|
| | | |
Formal Security Analysis of Australian E-passport Implementation
Pasupathinathan, V., Pieprzyk, J. and Wang, H.
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 is-
sues 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 ra-
tional security analysis we identify and describe a
set of security goals for evaluation of e-passport pro-
tocols. Our analysis confirms existing security is-
sues that were previously informally identified and
presents weaknesses that exists in the current e-
passport implementation. |
Cite as: Pasupathinathan, V., Pieprzyk, J. and Wang, H. (2008). Formal Security Analysis of Australian E-passport Implementation. In Proc. Sixth Australasian Information Security Conference (AISC 2008), Wollongong, NSW, Australia. CRPIT, 81. Brankovic, L. and Miller, M., Eds. ACS. 75-82. |
(from crpit.com)
(local if available)
|
|