On communication models when verifying equivalence properties

Kushal Babel, Vincent Cheval, and Steve Kremer. On communication models when verifying equivalence properties. In Proceedings of the 6th International Conference on Principles of Security and Trust (POST'17), pp. 141–163, Lecture Notes in Computer Science 10204, Springer, Uppsala, Sweden, April 2017. Best paper nominee.
doi:10.1007/978-3-662-54455-6

Download

[PDF] [PDF (long version)] [HTML] 

Abstract

Symbolic models for security protocol verification, following the sem-inal ideas of Dolev and Yao, come in many flavors, even though they share the same ideas. A common assumption is that the attacker has complete control over the network: he can therefore intercept any message. Depending on the precise model this may be reflected either by the fact that any protocol output is directly routed to the adversary, or communications may be among any two participants, including the attacker --- the scheduling between which exact parties the communication happens is left to the attacker. These two models may seem equivalent at first glance and, depending on the verification tools, either one or the other semantics is implemented. We show that, unsurprisingly, they indeed coincide for reachability properties. However, when we consider indistinguishability properties, we prove that these two semantics are incomparable. We also introduce a new semantics, where internal communications are allowed but messages are always eavesdropped by the attacker. We show that this new semantics yields strictly stronger equivalence relations. We also identify two subclasses of protocols for which the three semantics coincide. Finally, we implemented verification of trace equivalence for each of these semantics in the APTE tool and compare their performances on several classical examples.

BibTeX

@inproceedings{BCK-post17,
  abstract =	 {Symbolic models for security protocol verification,
                  following the sem-inal ideas of Dolev and Yao, come
                  in many flavors, even though they share the same
                  ideas. A common assumption is that the attacker has
                  complete control over the network: he can therefore
                  intercept any message. Depending on the precise
                  model this may be reflected either by the fact that
                  any protocol output is directly routed to the
                  adversary, or communications may be among any two
                  participants, including the attacker --- the
                  scheduling between which exact parties the
                  communication happens is left to the attacker. These
                  two models may seem equivalent at first glance and,
                  depending on the verification tools, either one or
                  the other semantics is implemented.  We show that,
                  unsurprisingly, they indeed coincide for
                  reachability properties. However, when we consider
                  indistinguishability properties, we prove that these
                  two semantics are incomparable. We also introduce a
                  new semantics, where internal communications are
                  allowed but messages are always eavesdropped by the
                  attacker. We show that this new semantics yields
                  strictly stronger equivalence relations. We also
                  identify two subclasses of protocols for which the
                  three semantics coincide. Finally, we implemented
                  verification of trace equivalence for each of these
                  semantics in the APTE tool and compare their
                  performances on several classical examples. },
  address =	 {Uppsala, Sweden},
  author =	 {Babel, Kushal and Cheval, Vincent and Kremer, Steve},
  booktitle =	 {{P}roceedings of the 6th International Conference on
                  Principles of Security and Trust (POST'17)},
  month =	 apr,
  series =	 {Lecture Notes in Computer Science},
  volume =	 10204,
  publisher =	 {Springer},
  doi =		 {10.1007/978-3-662-54455-6},
  pages =	 {141--163},
  title =	 {On communication models when verifying equivalence
                  properties},
  year =	 2017,
  acronym =	 {{POST}'17},
  nmonth =	 4,
  url =		 {https://hal.inria.fr/hal-01450898/},
  note =         {\textbf{\href{https://www.etaps.org/index.php/2017/best-papers}{Best paper nominee}}},
}