The shadow knows: refinement and security in sequential programs

DOI10.1016/j.scico.2007.09.003zbMath1178.68166MaRDI QIDQ923889

Carroll Morgan

Publication date: 24 July 2009

Published in: Science of Computer Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.scico.2007.09.003

zbMATH Keywords

security; privacy; implementation; specification; Hoare logic; logic of knowledge

Mathematics Subject Classification ID

68P25: Data encryption (aspects in computer science)

68N99: Theory of software

Related Items

Hidden-Markov program algebra with iteration, Algebraic foundations for quantitative information flow, Preface, Compositional refinement in agent-based security protocols, Compositional noninterference from first principles, On integrating confidentiality and functionality in a formal method, Dynamic intransitive noninterference revisited, Architectural refinement and notions of intransitive noninterference, Security invariants in discrete transition systems, Abstractions of non-interference security: probabilistic versus possibilistic, How to Brew-up a Refinement Ordering, Program Synthesis Using Dual Interpretation

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• The dining cryptographers problem: Unconditional sender and recipient untraceability
• Power domains
• A semantic approach to secure information flow
• A Proof System for Information Flow Security
• Knowledge and common knowledge in a distributed environment
• The Shadow Knows: Refinement of Ignorance in Sequential Programs
• Abstraction, Refinement and Proof for Probabilistic Systems
• An axiomatic basis for computer programming
• Program development by stepwise refinement
• A per model of secure information flow in sequential programs