The hitchhiker's guide to decidability and complexity of equivalence properties in security protocols
Vincent Cheval, Steve Kremer, and Itsaka Rakotonirina. The hitchhiker's guide to decidability and complexity of equivalence properties in security protocols. In Logic, Language, and Security. Essays Dedicated to Andre Scedrov on the Occasion of His 65th Birthday, Lecture Notes in Computer Science 12300, Springer, 2020.
doi:10.1007/978-3-030-62077-6_10
Download
[PDF] [PDF (long version)] [HTML]
Abstract
Privacy-preserving security properties in cryptographic protocols are typically modelled by observational equivalences in process calculi such as the applied pi-calulus. We survey decidability and complexity results for the automated verification of such equivalences, casting existing results in a common framework which allows for a precise comparison. This unified view, beyond providing a clearer insight on the current state of the art, allowed us to identify some variations in the statements of the decision problems---sometimes resulting in different complexity results. Additionally, we prove a couple of novel or strengthened results.
BibTeX
@InProceedings{CKR-scedrovfest20,
author = {Cheval, Vincent and Kremer, Steve and Rakotonirina,
Itsaka},
abstract = { Privacy-preserving security properties in
cryptographic protocols are typically modelled by
observational equivalences in process calculi such
as the applied pi-calulus. We survey decidability
and complexity results for the automated
verification of such equivalences, casting existing
results in a common framework which allows for a
precise comparison. This unified view, beyond
providing a clearer insight on the current state of
the art, allowed us to identify some variations in
the statements of the decision problems---sometimes
resulting in different complexity results.
Additionally, we prove a couple of novel or
strengthened results. },
title = {The hitchhiker's guide to decidability and
complexity of equivalence properties in security
protocols},
booktitle = {Logic, Language, and Security. Essays Dedicated to
Andre Scedrov on the Occasion of His 65th Birthday},
editor = {Nigam, V. and Talcott, C. and Guttman, J. and Ban
Kirigan, T. and Kuznetsov, S. and Okada, M. and Thau
Loo, B.},
year = 2020,
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = 12300,
acronym = {{ScedrovFest65}},
doi = {10.1007/978-3-030-62077-6_10},
={https://hal.archives-ouvertes.fr/hal-02501577v4/document},
={https://members.loria.fr/IRakotonirina/files/public_html/publications/scedrov20.pdf},
}