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

Automatic Analysis of the Security of XOR-Based Key Management Schemes. Véronique Cortier, Gavin Keighren, and Graham Steel. In Proceedings of the 13th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'07), pp. 538–552, Lecture Notes in Computer Science 4424, Springer, Braga, Portugal, March 2007.

Download

[PDF] [HTML]

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.

BibTeX

@inproceedings{CKSTacas07,
  address =       {Braga, Portugal},
  author =        {Cortier, V{\'e}ronique and Keighren, Gavin and
                   Steel, Graham},
  booktitle =     {{P}roceedings of the 13th {I}nternational
                   {C}onference on {T}ools and {A}lgorithms for
                   {C}onstruction and {A}nalysis of {S}ystems
                   ({TACAS}'07)},
  editor =        {Grumberg, Orna and Huth, Michael},
  month =         mar,
  pages =         {538-552},
  publisher =     {Springer},
  series =        {Lecture Notes in Computer Science},
  title =         {Automatic Analysis of the Security of {XOR}-Based Key
                   Management Schemes},
  volume =        {4424},
  year =          {2007},
  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.},
  doi =           {10.1007/978-3-540-71209-1_42},
}