zbMATH — the first resource for mathematics

FAST: an efficient decision procedure for deduction and static equivalence. (English) Zbl 1236.94073
Schmid-Schauß, Manfred (ed.), 22nd international conference on rewriting techniques and applications (RTA 2011), Novi Sad, Serbia, May 30 – June 1, 2011. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-939897-30-9). LIPIcs – Leibniz International Proceedings in Informatics 10, 11-20, electronic only (2011).
Summary: 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.
For the entire collection see [Zbl 1235.68033].

94A62 Authentication, digital signatures and secret sharing
68Q42 Grammars and rewriting systems
Full Text: DOI Link