Formal security analysis of Australian e-passport implementation

P. Vijayakrishnan; Josef Pieprzyk; Huaxiong Wang

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 proceeding › Conference proceeding contribution › peer-review

9 Citations (Scopus)

Abstract

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 language	English
Title of host publication	Proceedings of the Sixth Australasian Information Security Conference, AISC 2008
Editors	Ljiljana Brankovic, Mirka Miller
Place of Publication	Sydney
Publisher	Australian Computer Society
Pages	75-82
Number of pages	8
Volume	81
ISBN (Print)	9781920682620
Publication status	Published - 2008
Event	6th Australasian Information Security Conference, AISC 2008 - Wollongong, NSW, Australia Duration: 22 Jan 2008 → 25 Jan 2008

Other

Other	6th Australasian Information Security Conference, AISC 2008
Country/Territory	Australia
City	Wollongong, NSW
Period	22/01/08 → 25/01/08

Cite this

@inproceedings{eebd2e496c1c45a8a82e4dd44f412f13,

title = "Formal security analysis of Australian e-passport implementation",

abstract = "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.",

author = "P. Vijayakrishnan and Josef Pieprzyk and Huaxiong Wang",

year = "2008",

language = "English",

isbn = "9781920682620",

volume = "81",

pages = "75--82",

editor = "Ljiljana Brankovic and Mirka Miller",

booktitle = "Proceedings of the Sixth Australasian Information Security Conference, AISC 2008",

publisher = "Australian Computer Society",

address = "Australia",

note = "6th Australasian Information Security Conference, AISC 2008 ; Conference date: 22-01-2008 Through 25-01-2008",

}

Vijayakrishnan, P, Pieprzyk, J & Wang, H 2008, Formal security analysis of Australian e-passport implementation. in L Brankovic & M Miller (eds), Proceedings of the Sixth Australasian Information Security Conference, AISC 2008. vol. 81, Australian Computer Society, Sydney, pp. 75-82, 6th Australasian Information Security Conference, AISC 2008, Wollongong, NSW, Australia, 22/01/08.

Formal security analysis of Australian e-passport implementation. / Vijayakrishnan, P.; Pieprzyk, Josef; Wang, Huaxiong.

Proceedings of the Sixth Australasian Information Security Conference, AISC 2008. ed. / Ljiljana Brankovic; Mirka Miller. Vol. 81 Sydney : Australian Computer Society, 2008. p. 75-82.

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding contribution › peer-review

TY - GEN

T1 - Formal security analysis of Australian e-passport implementation

AU - Vijayakrishnan, P.

AU - Pieprzyk, Josef

AU - Wang, Huaxiong

PY - 2008

Y1 - 2008

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84871181622&partnerID=8YFLogxK

M3 - Conference proceeding contribution

AN - SCOPUS:84871181622

SN - 9781920682620

VL - 81

SP - 75

EP - 82

BT - Proceedings of the Sixth Australasian Information Security Conference, AISC 2008

A2 - Brankovic, Ljiljana

A2 - Miller, Mirka

PB - Australian Computer Society

CY - Sydney

T2 - 6th Australasian Information Security Conference, AISC 2008

Y2 - 22 January 2008 through 25 January 2008

ER -

Formal security analysis of Australian e-passport implementation

Abstract

Other

Other files and links

Fingerprint

Cite this