Formal Analysis of ISO/IEC 9798-2 Authentication Standard Using AVISPA

Author

Ziauddin, Sheikh ; Martin, Benoit

Author_Institution

Dept. of Comput. Sci., COMSATS Inst. of Inf. Technol., Islamabad, Pakistan

fYear

2013

fDate

25-26 July 2013

Firstpage

108

Lastpage

114

Abstract

Use of formal methods is considered as a useful and efficient technique for the validation of security properties of the protocols. In this paper, we analyze the protocols of ISO/IEC 9798-2 entity authentication standard using a state-of-the-art tool for automated analysis named AVISPA. Our analysis of the standard using AVISPA´s OFMC and CL-AtSe back-ends shows that the two party protocols are secure against the specified security properties while the back-ends are able to find attacks against unilateral and mutual authentication protocols involving a trusted third party.

Keywords

IEC standards; ISO standards; Internet; constraint handling; cryptographic protocols; formal verification; AVISPA; Automated Validation of Internet Security Protocols and Applications; CL-AtSe back-end; ISO/IEC 9798-2 entity authentication standard; OFMC back-end; automated analysis; constraint-logic-based attack searcher; formal analysis; mutual authentication protocols; on-the-fly model checker; party protocols; security properties; trusted third party; unilateral authentication protocols; Analytical models; Authentication; IEC standards; ISO standards; Protocols;

fLanguage

English

Publisher

ieee

Conference_Titel

Information Security (Asia JCIS), 2013 Eighth Asia Joint Conference on

Conference_Location

Seoul

Type

conf

DOI

10.1109/ASIAJCIS.2013.25

Filename

6621660