Formal security analysis of Australian e-passport implementation
Contribuinte(s) |
Brankovic, Ljiljana Miller, Mirka |
---|---|
Data(s) |
2008
|
Resumo |
This paper provides a detailed description of the current Australian e-passport implementation and makes a formal verification using model checking tools CASPER/CSP/FDR. We highlight security issues present in the current e-passport implementation and identify new threats when an e-passport system is integrated with an automated processing systems like SmartGate. Because the current e-passport specification does not provide adequate security goals, to perform a rational security analysis we identify and describe a set of security goals for evaluation of e-passport protocols. Our analysis confirms existing security issues that were previously informally identified and presents weaknesses that exists in the current e-passport implementation. |
Identificador | |
Publicador |
Australian Computer Society, Inc |
Relação |
http://crpit.com/confpapers/CRPITV81Vijayakrishnan.pdf Pasupathinathan, Vijayakrishnan, Pieprzyk, Josef, & Wang, Huaxiong (2008) Formal security analysis of Australian e-passport implementation. In Brankovic, Ljiljana & Miller, Mirka (Eds.) AISC '08 Proceedings of the Sixth Australasian Conference on Information Security - (CRPIT Volume 81 - Information Security 2008), Australian Computer Society, Inc, Wollongong, NSW, Australia, pp. 75-82. |
Direitos |
Copyright 2008 Australian Computer Society, Inc. |
Fonte |
School of Electrical Engineering & Computer Science; Science & Engineering Faculty |
Palavras-Chave | #Electronic passport #Formal methods #Model checking |
Tipo |
Conference Paper |