Proved generation of implementations from computationally secure protocol specifications

DOI10.1007/978-3-642-36830-1_4MaRDI QIDQ5326754zbMATH OpenOpenAlexFDO

Authors David Cadé, Bruno Blanchet

Publication date 6 August 2013

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

Full work available at URL https://doi.org/10.1007/978-3-642-36830-1_4

Mathematics Subject Classification ID

Data encryption (aspects in computer science) (68P25) Cryptography (94A60)

Recommendations

• Verified interoperable implementations of security protocols
• scientific article; zbMATH DE number 2090144
• Compiling and securing cryptographic protocols
• Cryptographically Sound Implementations for Communicating Processes
• G2C: cryptographic protocols from goal-driven specifications

Cited in

(8)

• scientific article; zbMATH DE number 2090144 (Why is no real title available?)
• System-level non-interference of constant-time cryptography. II: Verified static analysis and stealth memory
• Programming Languages and Systems
• Automatic Generation of Sources Lemmas in Tamarin: Towards Automatic Proofs of Security Protocols
• Formally sound implementations of security protocols with JavaSPI
• G2C: cryptographic protocols from goal-driven specifications
• Verified interoperable implementations of security protocols
• scientific article; zbMATH DE number 1583798 (Why is no real title available?)

Describes a project that uses

Uses Software

• CryptoVerif
• ASPIER
• OCaml

This page was built for publication: Proved generation of implementations from computationally secure protocol specifications

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