- 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.
(from crpit.com)
(local if available)
