### Abstract

Inspired by Abstract Cryptography, we extend CryptHOL, a framework for formalizing game-based proofs, with an abstract model of Random Systems and provide proof rules about their composition and equality. This foundation facilitates the formalization of Constructive Cryptography proofs, where the security of a cryptographic scheme is realized as a special form of construction in which a complex random system is built from simpler ones. This is a first step towards a fully-featured compositional framework, similar to Universal Composability framework, that supports formalization of simulation-based proofs.

### License

BSD License

### Topics

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

### Session Constructive_Cryptography

- Resource
- Converter
- Converter_Rewrite
- Random_System
- Distinguisher
- Wiring
- Constructive_Cryptography
- System_Construction
- One_Time_Pad
- Message_Authentication_Code
- Secure_Channel
- Examples

### Depends on

- CryptHOL

### Used by

- Constructive Cryptography in HOL: the Communication Modeling Aspect

## Cite

×

Constructive_Cryptography-AFP

    @article{Constructive_Cryptography-AFP,
      author  = {Andreas Lochbihler and S. Reza Sefidgar},
      title   = {Constructive Cryptography in HOL},
      journal = {Archive of Formal Proofs},
      month   = {December},
      year    = {2018},
      note    = {\url{https://isa-afp.org/entries/Constructive_Cryptography.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
- Dec 20, 2018 : Isabelle2018
- Dec 19, 2018 : Isabelle2018