Preserving Secrecy Under Refinement

DOI10.1007/11787006_10MaRDI QIDQ3591420zbMATH OpenOpenAlexFDO

Authors Pavol Černý, Steve Zdancewic, Rajeev Alur

Publication date 11 September 2007

Published in Automata, Languages and Programming (Search for Journal in Brave)

Full work available at URL https://repository.upenn.edu/cis_papers/270

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Cryptography (94A60)

Recommendations

• scientific article; zbMATH DE number 1693541
• The Secret Art of Computer Programming
• The shadow knows: refinement and security in sequential programs
• The Shadow Knows: Refinement of Ignorance in Sequential Programs
• Relating Two Standard Notions of Secrecy

Cited in

(36)

• Constructing independently verifiable privacy-compliant type systems for message passing between black-box components
• Opacity for linear constraint Markov chains
• Comparing the notions of opacity for discrete-event systems
• Preservation of probabilistic information flow under refinement
• scientific article; zbMATH DE number 1693541 (Why is no real title available?)
• Keeping secrets in resource aware components
• Model Checking Information Flow in Reactive Systems
• Relating two standard notions of secrecy
• Secrecy via Sources and Channels
• scientific article; zbMATH DE number 2185759 (Why is no real title available?)
• Unifying theories of confidentiality
• Secure information flow by self-composition
• Modelling declassification policies using abstract domain completeness
• Relating Two Standard Notions of Secrecy
• Dynamic Observers for the Synthesis of Opaque Systems
• Comparative analysis of related notions of opacity in centralized and coordinated architectures
• Information flow in systems with schedulers. II: Refinement
• scientific article; zbMATH DE number 1330433 (Why is no real title available?)
• Compositional refinement in agent-based security protocols
• Compositional noninterference from first principles
• Synthesis of opaque systems with static and dynamic masks
• Interval vs. point temporal logic model checking. An expressiveness comparison
• On refinement-closed security properties and nondeterministic compositions
• What you lose is what you leak: information leakage in declassification policies
• Collaborative planning with confidentiality
• Relating two standard notions of secrecy
• Quantifying opacity
• Abstractions preserving parameter confidentiality
• To know or not to know: Epistemic approaches to security protocol verification
• Secretive birds: privacy in population protocols
• Gray-box runtime enforcement of hyperproperties
• Preserving hyperproperties of programs using primitives with consensus number 2
• Opacity of discrete event systems and its applications
• Non-interference through determinism
• Enforcement and validation (at runtime) of various notions of opacity
• The shadow knows: refinement and security in sequential programs

Describes a project that uses

Uses Software

• PVS

This page was built for publication: Preserving Secrecy Under Refinement

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3591420)