2026-07-21T10:22:29Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:3136 2024-03-06T10:33:49Z ddc:004 open_access

FAST: An Efficient Decision Procedure for Deduction and Static Equivalence Conchinha, Bruno Basin, David A. Caleiro, Carlos Efficient algorithms Equational theories Deducibility Static equivalence Security protocols 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Bruno Conchinha and David A. Basin and Carlos Caleiro 2011 Is Part Of LIPIcs, Volume 10, 22nd International Conference on Rewriting Techniques and Applications (RTA'11) (2011) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.RTA.2011.11 urn:nbn:de:0030-drops-31369 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.11 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode