Automated analysis of equivalence properties for security protocols using else branches
Ivan Gazeau and Steve Kremer. Automated analysis of equivalence properties for security protocols using else branches. In Proceedings of the 22nd European Symposium on Research in Computer Security (ESORICS'17), pp. 1–20, Lecture Notes in Computer Science 10493, Springer, Oslo, Norway, September 2017.
doi:10.1007/978-3-319-66399-9_1
Download
[PDF] [PDF (long version)] [HTML]
Abstract
In this paper we present an extension of the AKISS protocol verification tool which allows to verify equivalence properties for protocols with else branches, i.e., disequality tests. While many protocols are represented as linear sequences or inputs, outputs and equality tests, the reality is often more complex. When verifying equivalence properties one needs to model precisely the error messages sent out when equality tests fail. While ignoring these branches may often be safe when studying trace properties this is not the case for equivalence properties, as for instance witnessed by an attack on the European electronic passport. One appealing feature of our approach is that our extension re-uses the saturation procedure which is at the heart of the verification procedure of AKISS as a black box, without need to modify it. As a result we obtain the first tool that is able verify equivalence properties for protocols that may use xor and else branches.We demonstrate the tool’s effectiveness on several case studies, including the AKA protocol deployed in mobile telephony.
BibTeX
@inproceedings{GK-esorics17,
abstract = {In this paper we present an extension of the AKISS
protocol verification tool which allows to verify
equivalence properties for protocols with else
branches, i.e., disequality tests. While many
protocols are represented as linear sequences or
inputs, outputs and equality tests, the reality is
often more complex. When verifying equivalence
properties one needs to model precisely the error
messages sent out when equality tests fail. While
ignoring these branches may often be safe when
studying trace properties this is not the case for
equivalence properties, as for instance witnessed by
an attack on the European electronic passport. One
appealing feature of our approach is that our
extension re-uses the saturation procedure which is
at the heart of the verification procedure of AKISS
as a black box, without need to modify it. As a
result we obtain the first tool that is able verify
equivalence properties for protocols that may use
xor and else branches.We demonstrate the tool’s
effectiveness on several case studies, including the
AKA protocol deployed in mobile telephony.},
address = {Oslo, Norway},
author = {Gazeau, Ivan and Kremer, Steve},
booktitle = {{P}roceedings of the 22nd {E}uropean {S}ymposium on
{R}esearch in {C}omputer {S}ecurity ({ESORICS}'17)},
pages = {1--20},
month = sep,
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {10493},
title = {Automated analysis of equivalence properties for
security protocols using else branches},
year = 2017,
acronym = {{ESORICS}'17},
nmonth = 9,
doi = {10.1007/978-3-319-66399-9_1},
url = {https://hal.inria.fr/hal-01566035/document},
}