License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2015.497
URN: urn:nbn:de:0030-drops-53946
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5394/
Go to the corresponding LIPIcs Volume Portal

Baelde, David ; Delaune, Stéphanie ; Hirschi, Lucca

Partial Order Reduction for Security Protocols

pdf-format:
34.pdf (0.6 MB)

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 (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 eliminate 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 Apte, and demonstrated that it achieves the expected speedup on various protocols.

BibTeX - Entry

@InProceedings{baelde_et_al:LIPIcs:2015:5394,
  author =	{David Baelde and St{\'e}phanie Delaune and Lucca Hirschi},
  title =	{{Partial Order Reduction for Security Protocols}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{497--510},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Luca Aceto and David de Frutos Escrig},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5394},
  URN =		{urn:nbn:de:0030-drops-53946},
  doi =		{10.4230/LIPIcs.CONCUR.2015.497},
  annote =	{Keywords: Cryptographic protocols, verification, process algebra, trace equivalence}
}

Keywords: Cryptographic protocols, verification, process algebra, trace equivalence
Collection: 26th International Conference on Concurrency Theory (CONCUR 2015)
Issue Date: 2015
Date of publication: 26.08.2015

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI