Calculus of Cryptographic Communication
2006 (English)Conference paper (Other academic)
We define C3, a model-based formalism that is one half of a framework for the modelling, specification and verification of cryptographic protocols. C3 consists of a design language of distributed processes and an associated (SOS) notion of concurrent execution. The other half of our framework is a property-based formalism, i.e., a logic for the specification and verification of cryptographic protocols, called CPL. The two primary features of the co-design of C3 and CPL are that reduction constraints of C3-processes are checkable via CPL-satisfaction, and that C3’s notion of observational equivalence and CPL’s notion of propositional knowledge have a common definitional basis, namely structurally indistinguishable protocol histories. Moreover, this co-design permits separation of the concerns of protocol and property description, within the same framework. Other important features of C3 are explicit notions of secure (out- of-band) communication and history-based key lookup, which together give a concrete foundation on which to base authentication and key establishment protocols.
Place, publisher, year, edition, pages
2006. , 17 p.
Research subject Computer Science with specialization in Computer Communication
IdentifiersURN: urn:nbn:se:uu:diva-162625OAI: oai:DiVA.org:uu-162625DiVA: diva2:461135
Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis, Seattle, August 15 - 16, 2006
Unpublished note accompanying a presentation at the Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis, Seattle, August 15 - 16, 20062011-12-052011-12-022011-12-07Bibliographically approved