Title :
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
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;
Conference_Titel :
Information Security (Asia JCIS), 2013 Eighth Asia Joint Conference on
Conference_Location :
Seoul
DOI :
10.1109/ASIAJCIS.2013.25
