Analysis of the PKCS#11 API using the maude-NPA tool

Antonio González-Burgueño, Sonia Santiago, Santiago Escobar, Catherine Meadows, José Meseguer

Research output: Chapter in Book/Report/Conference proceedingConference contribution


Cryptographic Application Programmer Interfaces (Crypto APIs) are designed to allow a secure interoperation between applications and cryptographic devices such as smartcards and Hardware Security Modules (HSMs). However, several Crypto APIs have been shown to be subject to attacks in which sensitive information is disclosed to an attacker, such as the RSA Laboratories Public Key Standards PKCS#11, an API widely adopted in industry. Recently, there has been a growing interest on applying automated crypto protocol analysis methods to formally analyze APIs. However, the PKCS#11 has been proven difficult to analyze using such methods since it involves non-monotonic mutable global state. In this paper we specify and analyze the PKCS#11 in Maude-NPA, a general purpose crypto protocol analysis tool.

Original languageEnglish (US)
Title of host publicationSecurity Standardisation Research - 2nd International Conference, SSR 2015, Proceedings
EditorsLiqun Chen, Shin’ichiro Matsuo
Number of pages21
ISBN (Print)9783319271514
StatePublished - 2015
Event2nd International Conference on Security Standardisation Research, SSR 2015 - Tokyo, Japan
Duration: Dec 15 2015Dec 16 2015

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other2nd International Conference on Security Standardisation Research, SSR 2015


  • Cryptographic application programming interfaces (cryptographic APIs)
  • Maude-NPA
  • PKCS#11
  • Symbolic cryptographic protocol analysis

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Analysis of the PKCS#11 API using the maude-NPA tool'. Together they form a unique fingerprint.

Cite this