A Formal Language for Cryptographic Pseudocode

DOI10.1007/978-3-540-89439-1_26MaRDI QIDQ5505567zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Michael Backes, Matthias Berg, Dominique Unruh

Publication date 27 January 2009

Published in Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-89439-1_26

Mathematics Subject Classification ID

Cryptography (94A60) Functional programming and lambda calculus (68N18)

Recommendations

• A Probabilistic Hoare-style Logic for Game-Based Cryptographic Proofs
• A Calculus for Game-Based Security Proofs
• The Computational SLR: A Logic for Reasoning about Computational Indistinguishability
• Formal certification of code-based cryptographic proofs
• CryptHOL: game-based proofs in higher-order logic

Cited in

(11)

• A formal language for cryptographic protocol requirements
• Certifying assembly with formal security proofs: the case of BBS
• The computational SLR: a logic for reasoning about computational indistinguishability
• CryptHOL: game-based proofs in higher-order logic
• A formalization of polytime functions
• A Calculus for Game-Based Security Proofs
• Formal security proofs with minimal fuss: implicit computational complexity at work
• Beyond provable security verifiable IND-CCA security of OAEP
• A Probabilistic Hoare-style Logic for Game-Based Cryptographic Proofs
• Probabilistic functions and cryptographic oracles in higher order logic
• The Computational SLR: A Logic for Reasoning about Computational Indistinguishability

Describes a project that uses

Uses Software

• Interrogator
• OFMC
• Isabelle/HOL
• Coq

This page was built for publication: A Formal Language for Cryptographic Pseudocode

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