Skip to Main content Skip to Navigation
Journal articles

On the semantics of communications when verifying equivalence properties

Kushal Babel 1 Vincent Cheval 2, * Steve Kremer 2
* Corresponding author
2 PESTO - Proof techniques for security protocols
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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.
Document type :
Journal articles
Complete list of metadata

Cited literature [23 references]  Display  Hide  Download
Contributor : Steve Kremer <>
Submitted on : Tuesday, January 21, 2020 - 11:36:10 AM
Last modification on : Friday, June 11, 2021 - 5:12:08 PM
Long-term archiving on: : Wednesday, April 22, 2020 - 5:12:57 PM


Files produced by the author(s)




Kushal Babel, Vincent Cheval, Steve Kremer. On the semantics of communications when verifying equivalence properties. Journal of Computer Security, IOS Press, In press, 28 (1), pp.71-127. ⟨10.3233/JCS-191366⟩. ⟨hal-02446910⟩



Record views


Files downloads