Constructive Cryptography in HOL: the Communication Modeling Aspect


Title: Constructive Cryptography in HOL: the Communication Modeling Aspect
Authors: Andreas Lochbihler and S. Reza Sefidgar
Submission date: 2021-03-17
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.
  author  = {Andreas Lochbihler and S. Reza Sefidgar},
  title   = {Constructive Cryptography in HOL: the Communication Modeling Aspect},
  journal = {Archive of Formal Proofs},
  month   = mar,
  year    = 2021,
  note    = {\url{},
            Formal proof development},
  ISSN    = {2150-914x},
License: BSD License
Depends on: Constructive_Cryptography, Game_Based_Crypto, Sigma_Commit_Crypto
Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.