Options
1998
Diploma Thesis
Titel
Analyse kryptographischer Protokolle mittels Produktnetzen basierend auf Modellannahmen der BAN-Logik
Abstract
In vielen Bereichen der Telekooperation ist es notwendig, daß zwischen verschiedenen Paaren von Teilnehmern (Menschen, Computern, Diensten, Chipkarten) Authentizität und Vertraulichkeit gesichert werden. Im allgemeinen begegnet man diesem Problem mit dem Einsatz kryptographischer Protokolle. Einige Protokolle dienen zum Beispiel zur Etablierung eines neuen Schlüssels zwischen zwei Partnern, die sich vorher jeweils von der Identität des anderenüberzeugen. Obwohl die verwendeten kryptographischen Verfahren große Sicherheit bieten, gibt es noch viele Möglichkeiten, solche Protokolle zu attackieren. Dazu zählen zum Beispiel replay-attacks (Wiederholung alter Nachrichten) oder parallel-session-attacks (Starten eines parallelen Protokollaufs mit Austausch von Nachrichten). Daher ist es wichtig, kryptographische Protokolle hinsichtlich ihrer Sicherheit zu analysieren. Ziel dieser Arbeit ist es, die Möglichkeiten zur Verwendung der Produktnetzmaschine als Analysewerkzeug für Authentifikationsprotokolle zu untersuchen. Um diese komplexe Problemstellung einzuschränken, wird die Wirkungsweise von Protokollen unter den Modellannahmen der BAN-Logik betrachtet. Diese von Burrows, Abadi und Needham eingeführte Logik bietet einen guten Ansatz zum Verständnis der Problematik und deckt einen Teil der möglichen Angriffe ab. Die als Produktnetze implementierten Methoden sollen mit geringem Aufwand an erweiterte Modelle angepaßt werden können. Es werden zwei Möglichkeiten vorgestellt, mit der Produktnetzmaschine Aussagen über Authentifikationsprotokolle zu treffen, erstens durch direkte Modellierung eines möglichen Angreifers und zweitens durch Implementation einer "Bottom-Up" Beweismethode für die BAN-Logik.
;
In telecooperating systems, it is often necessary to ensure authenticity and confidentiality between different pairs of principals (people, computers, services, smart cards, cellular phones). A common way to approach this problem is by using authentication protocols, using encryption and digital signatures. Although the encryption algorithms are good enough to prevent unauthorised decryption, it is often possible to attack protocols. The fundamental problem protocol designers have to deal with is the presence of a hostile opponent, who can control the complete communication between principals. For example, messages of ancient protocol runs can be repeated or parallel runs can be started, with exchange of messages between different runs. Also principals can be used as oracle to answer their own challenges. Since the variety of possible ways to attack protocols is enormous, formal methods are necessary to examine whether a protocol meets its security goals. This research work aims at supporting the verification of cryptographic protocols by applying formal methods used in the verification of distributed systems. The tool used for this purpose is the Product Net Machine (PNM), a tool developed by GMD - German National Research Center for Information Technology GmbH. Due to the complexity of the problem, it is useful to start with a restricted computational model which then can be be extended in a stepwise fashion in order to get a powerful method. In our research we use the restrictions used by Burrows, Abadi and Needham for their logic of authentication known as BAN logic [4]. Two different approaches to use product nets for the analysis of cryptographic protocols are presented. One approach is based on a product net model of a possible attacker. The second approach is the implementation of an automated "bottom-up" proof method for BAN-Logic.
ThesisNote
Zugl.: Frankfurt/Main, Univ., Dipl.-Arb., 1997
Tags