Exploiting Symmetries When Proving Equivalence Properties for Security Protocols
Vincent Cheval, Steve Kremer, and Itsaka Rakotonirina. Exploiting Symmetries When Proving Equivalence Properties for Security Protocols. In Proceedings of the 26th ACM Conference on Computer and Communications Security (CCS'19), pp. 905–922, ACM, London, UK, November 2019.
doi:10.1145/3319535.3354260
Download
[PDF] [PDF (long version)] [HTML]
Abstract
Verification of privacy-type properties for cryptographic protocols in an active adversarial environment, modelled as a behavioural equivalence in concurrent-process calculi, exhibits a high computational complexity. While undecidable in general, for some classes of common cryptographic primitives the problem is coNEXP-complete when the number of honest participants is bounded.
In this paper we develop optimisation techniques for verifying equivalences, exploiting symmetries between the two processes under study. We demonstrate that they provide a significant (several orders of magnitude) speed-up in practice, thus increasing the size of the protocols that can be analysed fully automatically.
BibTeX
@InProceedings{CKR-ccs19,
abstract = {Verification of privacy-type properties for
cryptographic protocols in an active adversarial
environment, modelled as a behavioural equivalence
in concurrent-process calculi, exhibits a high
computational complexity. While undecidable in
general, for some classes of common cryptographic
primitives the problem is coNEXP-complete when the
number of honest participants is bounded. \par In
this paper we develop optimisation techniques for
verifying equivalences, exploiting symmetries
between the two processes under study. We
demonstrate that they provide a significant (several
orders of magnitude) speed-up in practice, thus
increasing the size of the protocols that can be
analysed fully automatically. },
address = {London, UK},
author = {Cheval, Vincent and Kremer, Steve and Rakotonirina,
Itsaka},
booktitle = {{P}roceedings of the 26th ACM Conference on Computer
and Communications Security (CCS'19)},
month = nov,
pages = {905--922},
publisher = {ACM},
title = {Exploiting Symmetries When Proving Equivalence
Properties for Security Protocols},
year = 2019,
acronym = {{CCS}'19},
nmonth = 11,
doi = {10.1145/3319535.3354260},
url =
{https://hal.archives-ouvertes.fr/hal-02269043/document},
{https://hal.archives-ouvertes.fr/hal-02269043/document},
{https://hal.archives-ouvertes.fr/hal-02267866/document},
}