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

Abstract

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
PublisherSpringer
Pages86-106
Number of pages21
ISBN (Print)9783319271514
DOIs
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)
Volume9497
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other2nd International Conference on Security Standardisation Research, SSR 2015
Country/TerritoryJapan
CityTokyo
Period12/15/1512/16/15

Keywords

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

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

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