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},
}