License
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.RTA.2011.11
URN: urn:nbn:de:0030-drops-31369
URL: http://drops.dagstuhl.de/opus/volltexte/2011/3136/
Go to the corresponding LIPIcs Volume Portal


Conchinha, Bruno ; Basin, David A. ; Caleiro, Carlos

FAST: An Efficient Decision Procedure for Deduction and Static Equivalence

pdf-format:
Document 1.pdf (539 KB)


Abstract

Message deducibility and static equivalence are central problems in symbolic security protocol analysis. We present FAST, an efficient decision procedure for these problems under subterm-convergent equational theories. FAST is a C++ implementation of an improved version of the algorithm presented in our previous work. This algorithm has a better asymptotic complexity than other algorithms implemented by existing tools for the same task, and FAST's optimizations further improve these complexity results. We describe here the main ideas of our implementation and compare its performance with competing tools. The results show that our implementation is significantly faster: for many examples, FAST terminates in under a second, whereas other tools take several minutes.

BibTeX - Entry

@InProceedings{conchinha_et_al:LIPIcs:2011:3136,
  author =	{Bruno Conchinha and David A. Basin and Carlos Caleiro},
  title =	{{FAST: An Efficient Decision Procedure for Deduction and Static Equivalence}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{11--20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9 },
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Manfred Schmidt-Schau{\ss}},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2011/3136},
  URN =		{urn:nbn:de:0030-drops-31369},
  doi =		{http://dx.doi.org/10.4230/LIPIcs.RTA.2011.11},
  annote =	{Keywords: Efficient algorithms, Equational theories, Deducibility, Static equivalence, Security protocols}
}

Keywords: Efficient algorithms, Equational theories, Deducibility, Static equivalence, Security protocols
Seminar: 22nd International Conference on Rewriting Techniques and Applications (RTA'11)
Issue Date: 2011
Date of publication: 26.04.2011


DROPS-Home | Fulltext Search | Imprint Published by LZI