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 | |
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)