CryptHOL: game-based proofs in higher-order logic
From MaRDI portal
Publication:2175214
DOI10.1007/s00145-019-09341-zzbMath1455.94121OpenAlexW2751465014WikidataQ113906162 ScholiaQ113906162MaRDI QIDQ2175214
Andreas Lochbihler, S. Reza Sefidgar, David A. 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
Game theory (91A99) Cryptography (94A60) Authentication, digital signatures and secret sharing (94A62) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (5)
Quotients of Bounded Natural Functors ⋮ Categorical composable cryptography: extended version ⋮ Unnamed Item ⋮ Formalising \(\varSigma\)-protocols and commitment schemes using crypthol ⋮ Verified analysis of random binary tree structures
Uses Software
Cites Work
- The coinductive resumption monad
- Another look at ``provable security
- Proofs of randomized algorithms in Coq
- Probabilistic encryption
- Bisimulation through probabilistic testing
- A theory of type polymorphism in programming
- Isabelle/HOL. A proof assistant for higher-order logic
- How to simulate it in Isabelle: towards formal proof for secure multi-party computation
- Cryptography made simple
- Probabilistic Functions and Cryptographic Oracles in Higher Order Logic
- Probabilistic Termination and Composability of Cryptographic Protocols
- Truly Modular (Co)datatypes for Isabelle/HOL
- A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving
- A General Framework for Probabilistic Characterizing Formulae
- Constructive Cryptography – A New Paradigm for Security Definitions and Proofs
- Concrete Semantics
- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
- A Formalized Hierarchy of Probabilistic System Types
- A Consistent Foundation for Isabelle/HOL
- An equational approach to secure multi-party computation
- Friends with Benefits
- Comprehending Isabelle/HOL’s Consistency
- What Is a Pure Functional?
- The Security of Triple Encryption and a Framework for Code-Based Game-Playing Proofs
- A public key cryptosystem and a signature scheme based on discrete logarithms
- Stochastic lambda calculus and monads of probability distributions
- Computer-Aided Security Proofs for the Working Cryptographer
- Formal certification of code-based cryptographic proofs
- Complete Characterization of Fairness in Secure Two-Party Computation of Boolean Functions
- Automatic Data Refinement
- Coupling proofs are probabilistic product programs
- Complete Fairness in Secure Two-Party Computation
- Secure distributed programming with value-dependent types
- Probabilistic relational verification for cryptographic implementations
- Logic-Free Reasoning in Isabelle/Isar
- A Formal Language for Cryptographic Pseudocode
- Formal Abstractions for Attested Execution Secure Processors
- How to protect DES against exhaustive key search (an analysis of DESX).
- A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: CryptHOL: game-based proofs in higher-order logic
