### Abstract

CryptHOL provides a framework for formalising cryptographic arguments in Isabelle/HOL. It shallowly embeds a probabilistic functional programming language in higher order logic. The language features monadic sequencing, recursion, random sampling, failures and failure handling, and black-box access to oracles. Oracles are probabilistic functions which maintain hidden state between different invocations. All operators are defined in the new semantic domain of generative probabilistic values, a codatatype. We derive proof rules for the operators and establish a connection with the theory of relational parametricity. Thus, the resuting proofs are trustworthy and comprehensible, and the framework is extensible and widely applicable.

The framework is used in the accompanying AFP entry "Game-based Cryptography in HOL". There, we show-case our framework by formalizing different game-based proofs from the literature. This formalisation continues the work described in the author's ESOP 2016 paper.

### License

BSD License

### Topics

- Computer science/Security/Cryptography
- Computer science/Functional programming
- Mathematics/Probability theory

### Session CryptHOL

- Misc_CryptHOL
- Set_Applicative
- SPMF_Applicative
- List_Bits
- Environment_Functor
- Partial_Function_Set
- Negligible
- Resumption
- Generat
- Generative_Probabilistic_Value
- Computational_Model
- GPV_Expectation
- GPV_Bisim
- GPV_Applicative
- Cyclic_Group
- Cyclic_Group_SPMF
- CryptHOL

### Depends on

- Applicative Lifting
- Coinductive
- Landau Symbols
- Monad normalisation
- Effect polymorphism in higher-order logic
- Probabilistic while loop

### Used by

- CRYSTALS-Kyber_Security
- ABY3 Multiplication and Array Shuffling
- Sigma Protocols and Commitment Schemes
- Constructive Cryptography in HOL
- Game-based cryptography in HOL

### Auto-related entries

- Attack Trees in Isabelle for GDPR compliance of IoT healthcare systems

## Cite

×

CryptHOL-AFP

    @article{CryptHOL-AFP,
      author  = {Andreas Lochbihler},
      title   = {CryptHOL},
      journal = {Archive of Formal Proofs},
      month   = {May},
      year    = {2017},
      note    = {\url{https://isa-afp.org/entries/CryptHOL.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- May 11, 2017 : Isabelle2016-1