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

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

doi:10.1007/978-3-319-14054-4_8

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 proceeding › Conference contribution

Abstract

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 language	English (US)
Title of host publication	Security Standardisation Research - 1st International Conference, SSR 2014, Proceedings
Editors	Liqun Chen, Chris Mitchell
Publisher	Springer
Pages	111-130
Number of pages	20
ISBN (Electronic)	9783319140537
DOIs	https://doi.org/10.1007/978-3-319-14054-4_8
State	Published - 2014
Event	1st International Conference on Research in Security Standardisation Research, SSR 2014 - London, United Kingdom Duration: Dec 16 2014 → Dec 17 2014

Publication series

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

Other

Other	1st International Conference on Research in Security Standardisation Research, SSR 2014
Country/Territory	United Kingdom
City	London
Period	12/16/14 → 12/17/14

Keywords

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)

Online availability

10.1007/978-3-319-14054-4_8

Library availability

Discover UIUC Full Text

Cite this

González-Burgueño, A., Santiago, S., Escobar, S., Meadows, C., & Meseguer, J. (2014). Analysis of the ibm cca security api protocols in maude-npa. In L. Chen, & C. Mitchell (Eds.), Security Standardisation Research - 1st International Conference, SSR 2014, Proceedings (pp. 111-130). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8893). Springer. https://doi.org/10.1007/978-3-319-14054-4_8

Analysis of the ibm cca security api protocols in maude-npa. / González-Burgueño, Antonio; Santiago, Sonia; Escobar, Santiago et al.

Security Standardisation Research - 1st International Conference, SSR 2014, Proceedings. ed. / Liqun Chen; Chris Mitchell. Springer, 2014. p. 111-130 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8893).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

González-Burgueño, A, Santiago, S, Escobar, S, Meadows, C & Meseguer, J 2014, Analysis of the ibm cca security api protocols in maude-npa. in L Chen & C Mitchell (eds), Security Standardisation Research - 1st International Conference, SSR 2014, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 8893, Springer, pp. 111-130, 1st International Conference on Research in Security Standardisation Research, SSR 2014, London, United Kingdom, 12/16/14. https://doi.org/10.1007/978-3-319-14054-4_8

González-Burgueño A, Santiago S, Escobar S, Meadows C, Meseguer J. Analysis of the ibm cca security api protocols in maude-npa. In Chen L, Mitchell C, editors, Security Standardisation Research - 1st International Conference, SSR 2014, Proceedings. Springer. 2014. p. 111-130. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-14054-4_8

González-Burgueño, Antonio ; Santiago, Sonia ; Escobar, Santiago et al. / Analysis of the ibm cca security api protocols in maude-npa. Security Standardisation Research - 1st International Conference, SSR 2014, Proceedings. editor / Liqun Chen ; Chris Mitchell. Springer, 2014. pp. 111-130 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{0ddb773bb5b04201a2dbba373525b797,

title = "Analysis of the ibm cca security api protocols in maude-npa",

abstract = "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.",

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

author = "Antonio Gonz{\'a}lez-Burgue{\~n}o and Sonia Santiago and Santiago Escobar and Catherine Meadows and Jos{\'e} Meseguer",

note = "Funding Information: Antonio Gonz{\'a}lez-Burgue{\~n}o, Sonia Santiago and Santiago Escobar have been partially supported by the EU (FEDER) and the Spanish MINECO under grants TIN 2010-21062-C02-02 and TIN 2013-45732-C4-1-P, and by Generalitat Valenciana PROMETEO2011/052. Jos{\'e} Meseguer has been partially supported by NSF Grant CNS 13-10109. Publisher Copyright: {\textcopyright} Springer International Publishing Switzerland 2014.; 1st International Conference on Research in Security Standardisation Research, SSR 2014 ; Conference date: 16-12-2014 Through 17-12-2014",

year = "2014",

doi = "10.1007/978-3-319-14054-4_8",

language = "English (US)",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "111--130",

editor = "Liqun Chen and Chris Mitchell",

booktitle = "Security Standardisation Research - 1st International Conference, SSR 2014, Proceedings",

address = "Germany",

}

TY - GEN

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

AU - González-Burgueño, Antonio

AU - Santiago, Sonia

AU - Escobar, Santiago

AU - Meadows, Catherine

AU - Meseguer, José

N1 - Funding Information: Antonio González-Burgueño, Sonia Santiago and Santiago Escobar have been partially supported by the EU (FEDER) and the Spanish MINECO under grants TIN 2010-21062-C02-02 and TIN 2013-45732-C4-1-P, and by Generalitat Valenciana PROMETEO2011/052. José Meseguer has been partially supported by NSF Grant CNS 13-10109. Publisher Copyright: © Springer International Publishing Switzerland 2014.

PY - 2014

Y1 - 2014

N2 - 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.

AB - 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.

KW - Automatic reasoning modulo XOR theory

KW - IBM 4758 common cryptographic architecture

KW - Security application programming interfaces (security APIs)

KW - Symbolic cryptographic protocol analysis

UR - http://www.scopus.com/inward/record.url?scp=84917730262&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84917730262&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-14054-4_8

DO - 10.1007/978-3-319-14054-4_8

M3 - Conference contribution

AN - SCOPUS:84917730262

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 111

EP - 130

BT - Security Standardisation Research - 1st International Conference, SSR 2014, Proceedings

A2 - Chen, Liqun

A2 - Mitchell, Chris

PB - Springer

T2 - 1st International Conference on Research in Security Standardisation Research, SSR 2014

Y2 - 16 December 2014 through 17 December 2014

ER -

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

Abstract

Publication series

Other

Keywords

ASJC Scopus subject areas

Online availability

Library availability

Related links

Fingerprint

Cite this