Dresp, Wiebke (2005) Security Analysis of the Secure Authentication Protocol by Means of Coloured Petri Nets. In: Dittmann, Jana, (ed.) Communications and Multimedia Security. Lecture Notes in Computer Science, 3677. Springer, Berlin, pp. 230-239. ISBN 978-3-540-28791-9.
Download (946kB) - Repository staff only
Wireless communication demands for specialized protocols secure against attacks on the radio path while fitting the limited calculation and memory capabilities of mobile terminals. To ensure accessibility of mobile services beyond a user’s home network, signing on a foreign network should be possible. The latter must be able to authenticate a user without learning any secret registration data. Chouinard et al.[DBC01] introduce the Secure Authentication Protocol for this purpose.
In this paper, an exhaustive security analysis of the protocol is presented. First, it is mapped to a coloured petri net. Then, two different intruder models are developed and integrated separately into it. The state spaces of the two nets are calculated; they each contain a set of nodes representing all reachable states. Both are examined to detect states where any security objective is violated indicating a security flaw in the protocol. As there are no such states in both nets, the protocol is proven secure.
|Item Type:||Book Section|
|Institutions:||Business, Economics and Information Systems > Institut für Wirtschaftsinformatik > Professur für Wirtschaftsinformatik & Wirtschaftsmathematik (Prof. Dr. Peter Lory)|
|Keywords:||Secure Authentication Protocol; Coloured Petri Nets; Formal Protocol Verification; State Space Analysis; Security Analysis|
|Subjects:||300 Social sciences > 330 Economics|
|Created at the University of Regensburg:||Unknown|
|Deposited On:||12 Dec 2008 11:19|
|Last Modified:||20 Jul 2011 21:23|