# 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. BibTeX: @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 = mar, year = 2021, note = {\url{https://isa-afp.org/entries/Constructive_Cryptography_CM.html}, 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.