@COMMENT This file was generated by bib2html.pl version 0.94
@COMMENT written by Patrick Riley
@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},
}