Click here for full text:
A Structured Operational Modelling of the Dolev-Yao Threat Model
Keyword(s): No keywords available.
Abstract: In the areas of computer security and cryptography a standard model for adversaries is the Dolev-Yao threat model. In the areas of formal analysis of complex, concurrent, communication and reactive systems, one of the foundations for formal analysis methodologies is a structured operational semantics (SOS) for Milner's process algebra Calculus of Communicating Systems (CCS). In this paper we provide a CCS-SOS modelling of the Dolev-Yao threat model. The intuitively appealing modelling indicates a suitability for the well studied formal analysis methodologies based on CCS- SOS being applied to computer security and cryptography.
Back to Index