Automatic Analysis of the Security of XOR-based Key Management Schemes.

Véronique Cortier 1 Keighren Gavin 2 Graham Steel 2
1 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
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 IBM4758 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.
Type de document :
Communication dans un congrès
Orna Grumberg et Michael Huth. 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'07),, Mar 2007, Braga, Portugal. Springer-Verlag, 4424, pp.538-552, 2007, Lecture Notes in Computer Science
Liste complète des métadonnées

https://hal.inria.fr/inria-00181616
Contributeur : Véronique Cortier <>
Soumis le : mercredi 24 octobre 2007 - 10:44:09
Dernière modification le : vendredi 6 juillet 2018 - 15:06:10

Identifiants

  • HAL Id : inria-00181616, version 1

Citation

Véronique Cortier, Keighren Gavin, Graham Steel. Automatic Analysis of the Security of XOR-based Key Management Schemes.. Orna Grumberg et Michael Huth. 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'07),, Mar 2007, Braga, Portugal. Springer-Verlag, 4424, pp.538-552, 2007, Lecture Notes in Computer Science. 〈inria-00181616〉

Partager

Métriques

Consultations de la notice

172