Deriving cryptographically sound implementations using composition and formally verified bisimulation

DOI10.1007/3-540-45614-7_18MaRDI QIDQ4808837zbMATH OpenFDO

Authors Michael Backes, Christian Jacobi, Birgit Pfitzmann

Publication date 12 August 2004

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2391/23910310.htm

zbMATH Keywords

cryptographyformal verificationPVSsecuritysimulatability

Mathematics Subject Classification ID

Data encryption (aspects in computer science) (68P25)

Recommendations

• Cryptographically sound and machine-assisted verification of security protocols
• scientific article; zbMATH DE number 1251177
• scientific article; zbMATH DE number 1497864
• Proved generation of implementations from computationally secure protocol specifications
• Formal verification of cryptographic protocols: A survey

Cited in

(9)

• How to simulate it in Isabelle: towards formal proof for secure multi-party computation
• A simple framework for real-time cryptographic protocol analysis with compositional proof rules
• The reactive simulatability (RSIM) framework for asynchronous systems
• Unifying simulatability definitions in cryptographic systems under different timing assumptions
• Cryptographically sound and machine-assisted verification of security protocols
• Computational probabilistic non-interference
• Proved generation of implementations from computationally secure protocol specifications
• A survey of symbolic methods in computational analysis of cryptographic systems
• Separating the specification and implementation phases in cryptology (extended abstract)

Describes a project that uses

Uses Software

• PVS

This page was built for publication: Deriving cryptographically sound implementations using composition and formally verified bisimulation

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