David Baelde, Stéphanie Delaune, and Lucca Hirschi. Partial Order Reduction for Security Protocols. In Proceedings of the 26th International Conference on Concurrency Theory (CONCUR'15), pp. 497–510, Leibniz International Proceedings in Informatics 42, Leibniz-Zentrum für Informatik, Madrid, Spain, September 2015.
Security protocols are concurrent processes that communicate using cryptography with the aim of achieving various security properties. Recent work on their formal verification has brought procedures and tools for deciding trace equivalence properties (e.g., anonymity, unlinkability, vote secrecy) for a bounded number of sessions. However, these procedures are based on a naive symbolic exploration of all traces of the considered processes which, unsurprisingly, greatly limits the scalability and practical impact of the verification tools.
In this paper, we mitigate this difficulty by developing partial order reduction techniques for the verification of security protocols. We provide reduced transition systems that optimally elim- inate redundant traces, and which are adequate for model-checking trace equivalence properties of protocols by means of symbolic execution. We have implemented our reductions in the tool \textsfApte, and demonstrated that it achieves the expected speedup on various protocols.
@inproceedings{BDH-concur15,
abstract = {Security protocols are concurrent processes that
communicate using cryptography with the aim of
achieving various security properties. Recent work on
their formal verification has brought procedures and
tools for deciding trace equivalence properties
(\textit{e.g.},~anonymity, unlinkability, vote
secrecy) for a bounded number of sessions. However,
these procedures are based on a naive symbolic
exploration of all traces of the considered processes
which, unsurprisingly, greatly limits the scalability
and practical impact of the verification tools.\par
In this paper, we mitigate this difficulty by
developing partial order reduction techniques for the
verification of security protocols. We provide
reduced transition systems that optimally elim- inate
redundant traces, and which are adequate for
model-checking trace equivalence properties of
protocols by means of symbolic execution. We have
implemented our reductions in the tool \textsf{Apte},
and demonstrated that it achieves the expected
speedup on various protocols.},
address = {Madrid, Spain},
author = {Baelde, David and Delaune, St{\'e}phanie and
Hirschi, Lucca},
booktitle = {{P}roceedings of the 26th {I}nternational
{C}onference on {C}oncurrency {T}heory ({CONCUR}'15)},
OPTDOI = {10.4230/LIPIcs.CONCUR.2015.497},
editor = {Aceto, Luca and de Frutos-Escrig, David},
month = sep,
pages = {497-510},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
title = {Partial Order Reduction for Security Protocols},
volume = {42},
year = {2015},
acceptrate = {33/93},
acronym = {{CONCUR}'15},
nmonth = {9},
lsv-category = {intc},
wwwpublic = {public and ccsb},
}