Formal Analysis of CWA 14890-1 - Smart Card Research and Advanced Applications Access content directly
Conference Papers Year : 2011

Formal Analysis of CWA 14890-1

Ashar Javed
  • Function : Author
  • PersonId : 1017793


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.
Fichier principal
Vignette du fichier
978-3-642-27257-8_20_Chapter.pdf (310.57 Ko) Télécharger le fichier
Origin Files produced by the author(s)

Dates and versions

hal-01596294 , version 1 (27-09-2017)




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⟩
111 View
294 Download



Gmail Mastodon Facebook X LinkedIn More