Constructive Cryptography in HOL: the Communication Modeling Aspect

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.