Fraunhofer-Gesellschaft

Publica

Hier finden Sie wissenschaftliche Publikationen aus den Fraunhofer-Instituten.

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

 
: Gürgens, S.; Ochsenschläger, P.; Rudolph, C.

:
Volltext (PDF; )

Tjoa, A.M.:
13th International Workshop on Database and Expert Systems Applications 2002. Proceedings : 2 - 6 September 2002, Aix-en-Provence, France
Los Alamitos, Calif.: IEEE Computer Society, 2002
ISBN: 0-7695-1668-8
ISBN: 0-7695-1669-6
ISBN: 0-7695-1670-X
S.473-479
International Conference on Database and Expert Systems Applications (DEXA) <13, 2002, Aix-en-Provence>
Englisch
Konferenzbeitrag, Elektronische Publikation
Fraunhofer SIT ()
role based specification; security analysis; cryptography; Needham-Schroeder protocol; security protocol; protocol specification; SH verification tool; SHVT; state space analysis; protocol view; symbolic function; cryptographic protocol; asynchronous product automata; protocol agent; communicating automata

Abstract
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.

: http://publica.fraunhofer.de/dokumente/N-16745.html