CryptHOL: game-based proofs in higher-order logic

DOI10.1007/S00145-019-09341-ZMaRDI QIDQ2175214zbMATH OpenOpenAlexWikidataFDO

Authors Andreas Lochbihler, S. Reza Sefidgar, David Basin

Publication date 28 April 2020

Published in Journal of Cryptology (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s00145-019-09341-z

zbMATH Keywords

game-based proofshigher-order logicIsabelle/HOLprovable securitytheorem proving

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Game theory (91A99) Cryptography (94A60) Authentication, digital signatures and secret sharing (94A62)

Recommendations

• A Probabilistic Hoare-style Logic for Game-Based Cryptographic Proofs
• A Calculus for Game-Based Security Proofs
• Formal Proof of Provable Security by Game-Playing in a Proof Assistant
• Formal certification of code-based cryptographic proofs
• Automated Security Proofs with Sequences of Games

Cites work

• A consistent foundation for Isabelle/HOL
• A Formal Language for Cryptographic Pseudocode
• A formalized hierarchy of probabilistic system types. Proof pearl
• A general framework for probabilistic characterizing formulae
• A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks
• A public key cryptosystem and a signature scheme based on discrete logarithms
• A synthesis of the procedural and declarative styles of interactive theorem proving
• A theory of type polymorphism in programming
• An equational approach to secure multi-party computation
• Another look at ``provable security
• Automatic Data Refinement
• Bisimulation through probabilistic testing
• Complete Characterization of Fairness in Secure Two-Party Computation of Boolean Functions
• Complete fairness in secure two-party computation
• Comprehending Isabelle/HOL’s Consistency
• Computer-Aided Security Proofs for the Working Cryptographer
• Concrete semantics. With Isabelle/HOL
• Constructive cryptography -- a new paradigm for security definitions and proofs
• Coupling proofs are probabilistic product programs
• Cryptography made simple
• Formal abstractions for attested execution secure processors
• Formal certification of code-based cryptographic proofs
• Friends with benefits. Implementing corecursion in foundational proof assistants
• How to protect DES against exhaustive key search (an analysis of DESX).
• How to simulate it in Isabelle: towards formal proof for secure multi-party computation
• scientific article; zbMATH DE number 5009203 (Why is no real title available?)
• scientific article; zbMATH DE number 65529 (Why is no real title available?)
• scientific article; zbMATH DE number 3495581 (Why is no real title available?)
• scientific article; zbMATH DE number 3614066 (Why is no real title available?)
• scientific article; zbMATH DE number 1088907 (Why is no real title available?)
• scientific article; zbMATH DE number 1942415 (Why is no real title available?)
• scientific article; zbMATH DE number 1927425 (Why is no real title available?)
• scientific article; zbMATH DE number 1834589 (Why is no real title available?)
• scientific article; zbMATH DE number 1842495 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• Isabelle/HOL. A proof assistant for higher-order logic
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• Logic-Free Reasoning in Isabelle/Isar
• Probabilistic encryption
• Probabilistic functions and cryptographic oracles in higher order logic
• Probabilistic relational verification for cryptographic implementations
• Probabilistic Termination and Composability of Cryptographic Protocols
• Proofs of randomized algorithms in Coq
• Secure distributed programming with value-dependent types
• Stochastic lambda calculus and monads of probability distributions
• The coinductive resumption monad
• The Security of Triple Encryption and a Framework for Code-Based Game-Playing Proofs
• Truly modular (co)datatypes for Isabelle/HOL
• What is a pure functional?

Cited in

(13)

• Formalising \(\varSigma\)-protocols and commitment schemes using crypthol
• Formal Proof of Provable Security by Game-Playing in a Proof Assistant
• A Probabilistic Hoare-style Logic for Game-Based Cryptographic Proofs
• A Calculus for Game-Based Security Proofs
• Quotients of bounded natural functors
• Quotients of Bounded Natural Functors
• The Layered Games Framework for Specifications and Analysis of Security Protocols
• A Formal Language for Cryptographic Pseudocode
• Verified analysis of random binary tree structures
• Categorical composable cryptography: extended version
• Formalizing Coppersmith's method in Isabelle/HOL
• Propositional logics of overwhelming truth
• Formalizing the hidden number problem in Isabelle/HOL

Describes a project that uses

Uses Software

• Isabelle/HOL
• EasyCrypt
• Zoo Probabilistic Systems
• Archive Formal Proofs
• Probabilistic_While
• MFMC_Countable
• Game_Based_Crypto
• ML
• HOL
• AmiCo
• Nuprl
• Autoref
• miz3
• Transfer
• Lifting
• F*
• CryptHOL

This page was built for publication: CryptHOL: game-based proofs in higher-order logic

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