A structured operational semantic modelling of the Dolev-Yao threat environment and its composition with cryptographic protocols

摘要

In the areas of computer security and cryptographic protocols a standard model for describing the malicious behaviour of adversaries is the Dolev-Yao threat model. In formal analysis of complex, reactive and concurrent communication systems, a well-researched algebraic process approach is Milner's Calculus of Communicating Systems (CCS) which has the semantic foundation underpinned by Plotkin's structured operational semantics (SOS). In this article we provide a CCS-SOS modelling of the Dolev-Yao threat environment and its composition with the CCS description of a cryptographic protocol. For a given protocol, we attempt to discover security flaws by examining whether there is any difference between the SOS transition behaviours of the protocol descriptions which has and has not been composed with the malicious environment. The intuitively appealing modelling shows a suitability for the well-researched CCS-SOS-based algebraic process approach being applied to formal analysis of cryptographic protocols.