Formal security analysis of Australian e-passport implementation

P. Vijayakrishnan*, Josef Pieprzyk, Huaxiong Wang

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contributionpeer-review

9 Citations (Scopus)


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.

Original languageEnglish
Title of host publicationProceedings of the Sixth Australasian Information Security Conference, AISC 2008
EditorsLjiljana Brankovic, Mirka Miller
Place of PublicationSydney
PublisherAustralian Computer Society
Number of pages8
ISBN (Print)9781920682620
Publication statusPublished - 2008
Event6th Australasian Information Security Conference, AISC 2008 - Wollongong, NSW, Australia
Duration: 22 Jan 200825 Jan 2008


Other6th Australasian Information Security Conference, AISC 2008
CityWollongong, NSW


Dive into the research topics of 'Formal security analysis of Australian e-passport implementation'. Together they form a unique fingerprint.

Cite this