### Abstract

Constructive Cryptography (CC) [ICS 2011, TOSCA 2011, TCC 2016] introduces an abstract approach to composable security statements that allows one to focus on a particular aspect of security proofs at a time. Instead of proving the properties of concrete systems, CC studies system classes, i.e., the shared behavior of similar systems, and their transformations. Modeling of systems communication plays a crucial role in composability and reusability of security statements; yet, this aspect has not been studied in any of the existing CC results. We extend our previous CC formalization [Constructive_Cryptography, CSF 2019] with a new semantic domain called Fused Resource Templates (FRT) that abstracts over the systems communication patterns in CC proofs. This widens the scope of cryptography proof formalizations in the CryptHOL library [CryptHOL, ESOP 2016, J Cryptol 2020]. This formalization is described in Abstract Modeling of Systems Communication in Constructive Cryptography using CryptHOL.

### License

BSD License

### Topics

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

### Session Constructive_Cryptography_CM

- More_CC
- Observe_Failure
- Fold_Spmf
- Fused_Resource
- State_Isomorphism
- Construction_Utility
- Concrete_Security
- Asymptotic_Security
- Key
- Channel
- One_Time_Pad
- Diffie_Hellman_CC
- DH_OTP

### Depends on

- Constructive Cryptography in HOL
- Game-based cryptography in HOL
- Sigma Protocols and Commitment Schemes

## Cite

×

Constructive_Cryptography_CM-AFP

    @article{Constructive_Cryptography_CM-AFP,
      author  = {Andreas Lochbihler and S. Reza Sefidgar},
      title   = {Constructive Cryptography in HOL: the Communication Modeling Aspect},
      journal = {Archive of Formal Proofs},
      month   = {March},
      year    = {2021},
      note    = {\url{https://isa-afp.org/entries/Constructive_Cryptography_CM.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
- Mar 18, 2021 : Isabelle2021