A Formal Language for Cryptographic Pseudocode

DOI10.1007/978-3-540-89439-1_26zbMATH Open1182.94035DBLPconf/lpar/BackesBU08OpenAlexW1911300459WikidataQ62038955 ScholiaQ62038955MaRDI QIDQ5505567FDOQ5505567

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

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

Mathematics Subject Classification ID

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

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

Uses Software

• Coq
• Isabelle/HOL
• OFMC
• Interrogator

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)