Options
2001
Report
Titel
Role based specification and security analysis of cryptographic protocols using asynchronous product automata
Abstract
Kryptographische Protokolle werden als ein System von Protokollagenten mittels asynchroner Produktautomaten (APA) formal spezifiziert. APA sind ein universelles und sehr flexibles formales Beschreibungsmittel für kommunizierende Automaten. Ihre Spezifikation, Analyse und Verifikation wird von einem Werkzeug, dem SH-verification tool (SHVT), unterstützt. Der lokale Zustand eines Agenten ist in mehrere Komponenten aufgeteilt, welche seine Kenntnis von Schlüsseln, seine "Sicht" des Protokolls sowie die Ziele, die das Protokoll erreichen soll, beschreiben. Kommunikation wird modelliert durch das Hineinlegen und Wegnehmen von Nachrichten in bzw. aus einer Komponente Network, auf die alle Agenten Zugriff haben. Kryptographie wird mittels symbolischer Funktionen mit bestimmten Eigenschaften modelliert. Zusätzlich zu den regulären Protokollagenten wird ein Angreifer spezifiziert, der Zugriff auf Network, aber nicht auf die lokalen Zustände der Agenten hat. Er kann Nachrichten abfangen und neue Nachrichten erzeugen basierend auf seinem Anfangswissen und dem, was er aus abgefangenen Nachrichten extrahieren kann. Die Verletzung von Sicherheitszielen wird automatisch (SHVT) mittels Erreichbarkeitsanalyse gefunden. Die Methode wird am Beispiel des symmetrischen Needham-Schroeder Protokolls demonstriert. Dabei wird eine Angriffsmöglichkeit aufgezeigt, die nicht auf kompromitierte Session Keys zurückgreift. Unser Ansatz unterscheidet sich von anderen darin, daß die Protokollspezifikationen keine impliziten Annahmen machen. Somit hängt die Sicherheit eines Protokolls nicht davon ab, ob solche impliziten Annahmen für bestimmten Protokollumgebungen sinnvoll sind oder nicht. Unsere Protokollspezifikationen enthalten daher explizit die Information, die für eine sichere Implementation relevant ist.
;
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 modelled by adding messages to and removing them from a shared state component Network. Cryptography is modelled 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 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.