Constructive Cryptography in HOL: the Communication Modeling Aspect (Q7361367)

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 .