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.

Proof outline
Proof document

Browse theories

Download this entry