Sicherheitsanalyse von Authentifizierungsprotokollen - model checking mit dem SH-Verifikation Tool

Authentifizierungsprotokolle werden in verteilten Rechnersystemen verwendet, um die Identität eines Kommunikationspartners zu überprüfen, bevor mit diesem vertrauliche Daten ausgetauscht werden. Dieses Verfahren soll verhindern, daß ein unauthorisierter Dritter in die Kommunikation eingreifen kann. Zur Untersuchung, ob ein Authentifizierungsprotokoll dieses und weitere in der Diplomarbeit vorgestellte Protokollziele erreicht, wird eine Sicherheitsanalyse durchgeführt, durch die ausgeschlossen werden soll, daß Angriffe auf das betrachtete Protokoll möglich sind. Diese Untersuchung, die insbesondere klären soll, ob es für einen Angreifer möglich ist, in den Besitz von geheimen Daten zu gelangen, wurde bisher meistens durch "scharfes Hinsehen" und mit viel Intuition bezüglich der untersuchten Manipulationsmöglichkeiten durchgeführt. Zur Automatisierung dieses Vorgangs mit dem SH Verification Tool wird in der vorliegenden Diplomarbeit ein formales Modell eines Authentifizierungsprotokolls mit einem universellen Angreifer vorgestellt. Zur Durchführung einer umfassenden Sicherheitsanalyse ist es notwendig, daß der modellierte Angreifer jede Kommunikation zwischen den Protokollteilnehmern beliebig manipulieren kann. Dieser Ansatz führt allerdings sehr schnell zu einer beliebig großen Anzahl von zu untersuchenden Zuständen, was im praktischen Teil der Diplomarbeit an einem Beispiel vorgeführt wird. Daher wird im theoretischen Teil der Arbeit ein mathematischer Kalkül entwickelt, der es erlaubt, einen universellen Angreifer auf ein beliebiges Authentifizierungsprotokoll sinnvoll einzuschränken, ohne ihn in seinen Manipulationsmöglichkeiten zu beschränken.

In distributed computer systems, authentication protocols are used to check the communication partner's identity before exchanging confidential data with him. This procedure is supposed to stop unauthorised third parties from intervening in the communication. To analyse whether an authentication protocol achieves this and other goals presented in this research, a security analysis has to be performed to exclude an unauthorisied intervention. Previously, such studies investigated whether or not an attacker could gain access to confidential data by a combination of "taking a close look" and considerable intuition concerning the investigated possibilities for manipulation. In this research, a formal model of an authentication protocol with a universal attacker is presented for the automation of this procedure through the SH Verification Tool. For the purposes of a comprehensive security check, the model attacker is assumed to be able to manipulate any communication between the protocol participants. As demonstrated in an example in the practical part of the research, this assumption quickly leads to a vast number of states to be analysed. Therefore, as described in the theoretical part of the work, a mathematical calculus was developed which allows to limit the universal attacker in a sensible manner, without limiting his manipulation possibilities.