Role based specification and security analysis of cryptographic protocols using asynchronous product automata

Sigrid Gürgens, Peter Ochsenschläger, Carsten Rudolph

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

12 Citations (Scopus)


Cryptographic protocols are formally specified as a system of protocol agents using asynchronous product automata (APA). APA are a universal and very flexible operational description concept for communicating automata. Their specification, analysis and verification is supported by the SH-verification tool (SHVT). The local state of each agent is structured in several components describing its knowledge of keys, its "view" of the protocol and the goals to be reached within the protocol. Communication is modeled by adding messages to and removing them from a shared state component network. Cryptography is modeled by symbolic functions with certain properties. In addition to the regular protocol agents an intruder is specified, which has no access to the agents' local states but to the network. The intruder may intercept messages and create new ones based on his initial knowledge and on what he can extract from intercepted messages. Violations of the security goals can be found by state space analysis performed by the SHVT. The method is demonstrated using the symmetric Needham-Schroeder protocol, and an attack is presented that does not involve compromised session keys. Our approach defers from others in that protocol specifications do not use implicit assumptions, thus protocol security does not depend on whether some implicit assumptions made are reasonable for a particular environment. Therefore, our protocol specifications explicitly provide relevant information for secure implementations.

Original languageEnglish
Title of host publicationProceedings - 13th International Workshop on Database and Expert Systems Applications, DEXA 2002
PublisherIEEE, Institute of Electrical and Electronics Engineers
Number of pages7
ISBN (Electronic)0769516688
Publication statusPublished - 1 Jan 2002
Externally publishedYes
EventInternational Workshop on Trust and Privacy in Digital Business 2002 - Aix-en-Provence, France
Duration: 2 Sep 20026 Sep 2002 (Proceedings)


ConferenceInternational Workshop on Trust and Privacy in Digital Business 2002
Abbreviated titleTrustBus 2002
OtherHeld within the "International Conference on Database and Expert Systems Applications 2002"
Internet address


  • Access protocols
  • Algorithm design and analysis
  • Authentication
  • Automata
  • Cryptographic protocols
  • Cryptography
  • Information security
  • Performance analysis
  • Power system modeling
  • State-space methods

Cite this