A Structured Operational Modelling of the Dolev-Yao Threat Model

  • Wenbo Mao
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2845)


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.


Model Check Security Protocol Computer Security System Composition Threat Model 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 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. 2.
    CWB. The Edinburgh Concurrency Workbench, Available at
  3. 3.
    Denning, D., Sacco, G.: Timestamps in key distribution protocols. Communications of the ACM 24(8), 533–536 (1981)CrossRefGoogle Scholar
  4. 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
  5. 5.
    Hennessy, M.: Algebraic Theory of Processes. The MIT Press, Cambridge (1988)zbMATHGoogle Scholar
  6. 6.
    Hoare, C.A.R.: Communicating sequential processes. Communications of the ACM 21(8) (1978)Google Scholar
  7. 7.
    Hoare, C.A.R.: Communicating Sequential Processes. Series in Computer Science. Prentice Hall International, Englewood Cliffs (1985)zbMATHGoogle Scholar
  8. 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
  9. 9.
    Milner, R.: A Calculus of Communicating Systems. Springer, Heidelberg (1980)zbMATHGoogle Scholar
  10. 10.
    Milner, R.: Communication and Concurrency. Series in Computer Science. Prentice Hall International, Englewood Cliffs (1989)zbMATHGoogle Scholar
  11. 11.
    Needham, R., Schroeder, M.: Using encryption for authentication in large networks of computers. Communications of the ACM 21(12), 993–999 (1978)zbMATHCrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Wenbo Mao
    • 1
  1. 1.Hewlett-Packard LaboratoriesBristolUnited Kingdom

Personalised recommendations