Analysis of the ibm cca security api protocols in maude-npa

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

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


Standards for cryptographic protocols have long been attractive candidates for formal verification. It is important that such standards be correct, and cryptographic protocols are tricky to design and subject to non-intuitive attacks even when the underlying cryptosystems are secure. Thus a number of general-purpose cryptographic protocol analysis tools have been developed and applied to protocol standards. However, there is one class of standards, security application programming interfaces (security APIs), to which few of these tools have been applied. Instead, most work has concentrated on developing special-purpose tools and algorithms for specific classes of security APIs. However, there can be much advantage gained from having general-purpose tools that could be applied to a wide class of problems, including security APIs.

One particular class of APIs that has proven difficult to analyze using general-purpose tools is that involving exclusive-or. In this paper we analyze the IBM 4758 Common Cryptographic Architecture (CCA) protocol using an advanced automated protocol verification tool with full exclusive-or capabilities, the Maude-NPA tool. This is the first time that API protocols have been satisfactorily specified and analyzed in the Maude-NPA, and the first time XOR-based APIs have been specified and analyzed using a general-purpose unbounded session cryptographic protocol verification tool that provides direct support for AC theories. We describe our results and indicate what further research needs to be done to make such protocol analysis generally effective.

Original languageEnglish (US)
Title of host publicationSecurity Standardisation Research - 1st International Conference, SSR 2014, Proceedings
EditorsLiqun Chen, Chris Mitchell
Number of pages20
ISBN (Electronic)9783319140537
StatePublished - 2014
Event1st International Conference on Research in Security Standardisation Research, SSR 2014 - London, United Kingdom
Duration: Dec 16 2014Dec 17 2014

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


Other1st International Conference on Research in Security Standardisation Research, SSR 2014
Country/TerritoryUnited Kingdom


  • Automatic reasoning modulo XOR theory
  • IBM 4758 common cryptographic architecture
  • Security application programming interfaces (security APIs)
  • Symbolic cryptographic protocol analysis

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Analysis of the ibm cca security api protocols in maude-npa'. Together they form a unique fingerprint.

Cite this