Skip to Main content Skip to Navigation
Conference papers

Formal Analysis of CWA 14890-1

Abstract : Formal analysis is of importance in order to increase confidence that the protocol satisfies its security requirements. In particular, the results obtained from the formal analysis of the smart card security protocols when smart cards are used as a specific type of Secure Signature Creation Devices (SSCDs) are presented. SSCDs are developed to support the EU-directive on electronic signatures. In this paper, we focus on security properties, called the authentication and secrecy. The device authentication protocols mentioned in CWA 14890-1 are modeled using the high-level protocol specification language HLPSL and verified with the help of AVISPA tool. Our formal analysis does not reveal any weaknesses of the CWA 14890-1 protocol suite.
Complete list of metadata

Cited literature [13 references]  Display  Hide  Download
Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Wednesday, September 27, 2017 - 2:46:04 PM
Last modification on : Tuesday, October 10, 2017 - 1:47:57 PM
Long-term archiving on: : Thursday, December 28, 2017 - 1:40:47 PM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License



Ashar Javed. Formal Analysis of CWA 14890-1. 10th Smart Card Research and Advanced Applications (CARDIS), Sep 2011, Leuven, Belgium. pp.314-335, ⟨10.1007/978-3-642-27257-8_20⟩. ⟨hal-01596294⟩



Record views


Files downloads