Automatic Analysis of the Security of XOR-Based Key Management Schemes

Véronique Cortier; Gavin Keighren; Graham Steel

doi:10.1007/978-3-540-71209-1_42

Automatic Analysis of the Security of XOR-Based Key Management Schemes

Véronique Cortier, Gavin Keighren, Graham Steel

School of Informatics

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

Abstract

We describe a new algorithm for analysing security protocols that use XOR, such as key-management APIs. As a case study, we consider the IBM 4758 CCA API, which is widely used in the ATM (cash machine) network. Earlier versions of the CCA API were shown to have serious flaws, and the fixes introduced by IBM in version 2.41 had not previously been formally analysed. We first investigate IBM’s proposals using a model checker for security protocol analysis, uncovering some important issues about their implementation. Having identified configurations we believed to be safe, we describe the formal verification of their security. We first define a new class of protocols, containing in particular all the versions of the CCA API. We then show that secrecy after an unbounded number of sessions is decidable for this class. Implementing the decision procedure requires some improvements, since the procedure is exponential. We describe a change of representation that leads to an implementation able to verify a configuration of the API in a few seconds. As a consequence, we obtain the first security proof of the fixed IBM 4758 CCA API with unbounded sessions.

Original language	English
Title of host publication	Tools and Algorithms for the Construction and Analysis of Systems
Subtitle of host publication	13th International Conference, TACAS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24 - April 1, 2007. Proceedings
Editors	Orna Grumberg, Michael Huth
Publisher	Springer
Pages	538-552
Number of pages	15
ISBN (Electronic)	978-3-540-71209-1
ISBN (Print)	978-3-540-71208-4
DOIs	https://doi.org/10.1007/978-3-540-71209-1_42
Publication status	Published - 2007

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Berlin / Heidelberg
Volume	4424
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Access to Document

10.1007/978-3-540-71209-1_42

AUTOMATED ANALYSIS OF SECURITY CRITICAL SYSTEMS
Bundy, A. & Fleuriot, J.
EPSRC
1/10/04 → 30/09/07
Project: Research

Cite this

Cortier, V., Keighren, G., & Steel, G. (2007). Automatic Analysis of the Security of XOR-Based Key Management Schemes. In O. Grumberg, & M. Huth (Eds.), Tools and Algorithms for the Construction and Analysis of Systems: 13th International Conference, TACAS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24 - April 1, 2007. Proceedings (pp. 538-552). (Lecture Notes in Computer Science; Vol. 4424). Springer. https://doi.org/10.1007/978-3-540-71209-1_42

Cortier, Véronique ; Keighren, Gavin ; Steel, Graham. / Automatic Analysis of the Security of XOR-Based Key Management Schemes. Tools and Algorithms for the Construction and Analysis of Systems: 13th International Conference, TACAS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24 - April 1, 2007. Proceedings. editor / Orna Grumberg ; Michael Huth. Springer, 2007. pp. 538-552 (Lecture Notes in Computer Science).

@inproceedings{3a96ccfc3172499281a8e508fec5dbc1,

title = "Automatic Analysis of the Security of XOR-Based Key Management Schemes",

abstract = "We describe a new algorithm for analysing security protocols that use XOR, such as key-management APIs. As a case study, we consider the IBM 4758 CCA API, which is widely used in the ATM (cash machine) network. Earlier versions of the CCA API were shown to have serious flaws, and the fixes introduced by IBM in version 2.41 had not previously been formally analysed. We first investigate IBM{\textquoteright}s proposals using a model checker for security protocol analysis, uncovering some important issues about their implementation. Having identified configurations we believed to be safe, we describe the formal verification of their security. We first define a new class of protocols, containing in particular all the versions of the CCA API. We then show that secrecy after an unbounded number of sessions is decidable for this class. Implementing the decision procedure requires some improvements, since the procedure is exponential. We describe a change of representation that leads to an implementation able to verify a configuration of the API in a few seconds. As a consequence, we obtain the first security proof of the fixed IBM 4758 CCA API with unbounded sessions.",

author = "V{\'e}ronique Cortier and Gavin Keighren and Graham Steel",

year = "2007",

doi = "10.1007/978-3-540-71209-1_42",

language = "English",

isbn = "978-3-540-71208-4",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "538--552",

editor = "Orna Grumberg and Michael Huth",

booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",

address = "United Kingdom",

}

Cortier, V, Keighren, G & Steel, G 2007, Automatic Analysis of the Security of XOR-Based Key Management Schemes. in O Grumberg & M Huth (eds), Tools and Algorithms for the Construction and Analysis of Systems: 13th International Conference, TACAS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24 - April 1, 2007. Proceedings. Lecture Notes in Computer Science, vol. 4424, Springer, pp. 538-552. https://doi.org/10.1007/978-3-540-71209-1_42

Automatic Analysis of the Security of XOR-Based Key Management Schemes. / Cortier, Véronique; Keighren, Gavin; Steel, Graham.
Tools and Algorithms for the Construction and Analysis of Systems: 13th International Conference, TACAS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24 - April 1, 2007. Proceedings. ed. / Orna Grumberg; Michael Huth. Springer, 2007. p. 538-552 (Lecture Notes in Computer Science; Vol. 4424).

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

TY - GEN

T1 - Automatic Analysis of the Security of XOR-Based Key Management Schemes

AU - Cortier, Véronique

AU - Keighren, Gavin

AU - Steel, Graham

PY - 2007

Y1 - 2007

N2 - We describe a new algorithm for analysing security protocols that use XOR, such as key-management APIs. As a case study, we consider the IBM 4758 CCA API, which is widely used in the ATM (cash machine) network. Earlier versions of the CCA API were shown to have serious flaws, and the fixes introduced by IBM in version 2.41 had not previously been formally analysed. We first investigate IBM’s proposals using a model checker for security protocol analysis, uncovering some important issues about their implementation. Having identified configurations we believed to be safe, we describe the formal verification of their security. We first define a new class of protocols, containing in particular all the versions of the CCA API. We then show that secrecy after an unbounded number of sessions is decidable for this class. Implementing the decision procedure requires some improvements, since the procedure is exponential. We describe a change of representation that leads to an implementation able to verify a configuration of the API in a few seconds. As a consequence, we obtain the first security proof of the fixed IBM 4758 CCA API with unbounded sessions.

AB - We describe a new algorithm for analysing security protocols that use XOR, such as key-management APIs. As a case study, we consider the IBM 4758 CCA API, which is widely used in the ATM (cash machine) network. Earlier versions of the CCA API were shown to have serious flaws, and the fixes introduced by IBM in version 2.41 had not previously been formally analysed. We first investigate IBM’s proposals using a model checker for security protocol analysis, uncovering some important issues about their implementation. Having identified configurations we believed to be safe, we describe the formal verification of their security. We first define a new class of protocols, containing in particular all the versions of the CCA API. We then show that secrecy after an unbounded number of sessions is decidable for this class. Implementing the decision procedure requires some improvements, since the procedure is exponential. We describe a change of representation that leads to an implementation able to verify a configuration of the API in a few seconds. As a consequence, we obtain the first security proof of the fixed IBM 4758 CCA API with unbounded sessions.

U2 - 10.1007/978-3-540-71209-1_42

DO - 10.1007/978-3-540-71209-1_42

M3 - Conference contribution

SN - 978-3-540-71208-4

T3 - Lecture Notes in Computer Science

SP - 538

EP - 552

BT - Tools and Algorithms for the Construction and Analysis of Systems

A2 - Grumberg, Orna

A2 - Huth, Michael

PB - Springer

ER -

Cortier V, Keighren G, Steel G. Automatic Analysis of the Security of XOR-Based Key Management Schemes. In Grumberg O, Huth M, editors, Tools and Algorithms for the Construction and Analysis of Systems: 13th International Conference, TACAS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24 - April 1, 2007. Proceedings. Springer. 2007. p. 538-552. (Lecture Notes in Computer Science). doi: 10.1007/978-3-540-71209-1_42

Automatic Analysis of the Security of XOR-Based Key Management Schemes

Abstract

Publication series

Access to Document

Fingerprint

Projects

AUTOMATED ANALYSIS OF SECURITY CRITICAL SYSTEMS

Cite this