@COMMENT This file was generated by bib2html.pl version 0.94
@COMMENT written by Patrick Riley
@Article{BCK-jcs20,
abstract = {Symbolic models for security protocol verification
were pioneered by Dolev and Yao in their seminal
work. Since then, although inspired by the same
ideas, many variants of the original model were
developed. In particular, a common assumption is
that the attacker has complete control over the
network and can therefore intercept any
message. This assumption has been interpreted in
slightly different ways depending on the particular
models: either 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. This
difference may seem unimportant 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, for
indistinguishability properties, we prove that these
two interpretations lead to incomparable
semantics. We also introduce and study a new
semantics, where internal communications are allowed
but messages are always eavesdropped by the
attacker. This new semantics yields strictly
stronger equivalence relations. Moreover, we
identify two subclasses of protocols for which the
three semantics coincide. Finally, we implemented
verification of trace equivalence for each of the
three semantics in the DEEPSEC tool and compare
their performances on several classical examples.},
author = {Babel, Kushal and Cheval, Vincent and Kremer, Steve},
title = {On the semantics of communications when verifying
equivalence properties},
journal = {Journal of Computer Security},
volume = 28,
number = 1,
pages = {71-127},
year = 2020,
doi = {10.3233/JCS-191366},
url = {https://hal.inria.fr/hal-02446910/document},
}