Preserving Secrecy Under Refinement

DOI10.1007/11787006_10zbMath1133.94307OpenAlexW1492585812MaRDI QIDQ3591420

Steve Zdancewic, Pavol Černý, 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

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

Related Items (20)

Model Checking Information Flow in Reactive Systems ⋮ Constructing independently verifiable privacy-compliant type systems for message passing between black-box components ⋮ Comparative analysis of related notions of opacity in centralized and coordinated architectures ⋮ Information flow in systems with schedulers. II: Refinement ⋮ Enforcement and validation (at runtime) of various notions of opacity ⋮ To know or not to know: Epistemic approaches to security protocol verification ⋮ 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 ⋮ Opacity for linear constraint Markov chains ⋮ Collaborative planning with confidentiality ⋮ Quantifying opacity ⋮ On Refinement-Closed Security Properties and Nondeterministic Compositions ⋮ Opacity of discrete event systems and its applications ⋮ Comparing the notions of opacity for discrete-event systems ⋮ Dynamic Observers for the Synthesis of Opaque Systems ⋮ Secure information flow by self-composition ⋮ Modelling declassification policies using abstract domain completeness ⋮ What You Lose is What You Leak: Information Leakage in Declassification Policies

Uses Software

• PVS

This page was built for publication: Preserving Secrecy Under Refinement