@InProceedings{ conchinha.ea:efficient:2011, abstract = {We consider two standard notions in formal security protocol analysis: message deducibility and static equivalence under equational theories. We present new polynomial-time algorithms for deciding both notions under subterm convergent equational theories and under a theory representing symmetric encryption with the prefix property. For these equational theories, polynomial-time algorithms for the decision problems associated to both notions are well-known (although this has not been proven for static equivalence under the prefix theory). However, our algorithms have a significantly better asymptotic complexity than existing approaches.As an application, we use our algorithm for static equivalence to discover off-line guessing attacks on the Kerberos protocol when implemented using a symmetric encryption scheme for which the prefix property holds.}, author = {Bruno Conchinha and David Basin and Carlos Caleiro}, booktitle = {7th International Workshop on Formal Aspects of Security and Trust - FAST 2010}, editor = {Pierpaolo Degano and Sandro Etalle and Joshua D. Guttman}, filelabel = {DBLP:conf/ifip1-7/2010}, isbn = {978-3-642-19750-5}, language = {USenglish}, pages = {34--49}, pdf = {papers/2011/EfficientDecision.pdf}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {Efficient Decision Procedures for Message Deducibility and Static Equivalence}, url = {http://dx.doi.org/10.1007/978-3-642-19751-2}, volume = 6561, year = 2011, user = {bgeiser} }