LIPIcs.RTA.2011.11.pdf
- Filesize: 0.52 MB
- 10 pages
Document
FAST: An Efficient Decision Procedure for Deduction and Static Equivalence
Authors
-
Part of:
Volume:
22nd International Conference on Rewriting Techniques and Applications (RTA'11) (RTA 2011)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Rewriting Techniques and Applications (RTA) - License:
Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
- Publication Date: 2011-04-26
Cite AsGet BibTex
Bruno Conchinha, David A. Basin, and Carlos Caleiro. FAST: An Efficient Decision Procedure for Deduction and Static Equivalence. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 11-20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
https://doi.org/10.4230/LIPIcs.RTA.2011.11
https://doi.org/10.4230/LIPIcs.RTA.2011.11
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.
Keywords
- Efficient algorithms
- Equational theories
- Deducibility
- Static equivalence
- Security protocols
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads