A Structured Operational Modelling of the Dolev-Yao Threat Model
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.
KeywordsModel Check Security Protocol Computer Security System Composition Threat Model
Unable to display preview. Download preview PDF.
- 1.Clarke, E.M., Jha, S., Marrero, W.: Using state space exploration and a natural deduction style message derivation engine to verify security protocols. In: Proc. IFIP Working Conference on Programming Concepts, and Methods (PROCOMET) (June 1998)Google Scholar
- 2.CWB. The Edinburgh Concurrency Workbench, Available at http://www.dcs.ed.ac.uk/home/cwb/
- 4.Dolev, D., Yao, A.C.: On the security of public key protocols. In: Proceedings of the IEEE 22nd Annual Symposium on Foundations of Computer Science, pp. 350–357 (1981)Google Scholar
- 6.Hoare, C.A.R.: Communicating sequential processes. Communications of the ACM 21(8) (1978)Google Scholar
- 8.Marrero, W.: BRUTUS: A Model Checker for Security Protocols, Ph.D. Thesis, CMU-CS-01-170, School of Computer Science, Carnegie Mellon University (December 2001)Google Scholar