{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:26:34Z","timestamp":1774837594098,"version":"3.50.1"},"reference-count":42,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2013,2,1]],"date-time":"2013-02-01T00:00:00Z","timestamp":1359676800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["11-JS02-006-01"],"award-info":[{"award-number":["11-JS02-006-01"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004963","name":"Seventh Framework Programme","doi-asserted-by":"publisher","award":["FP7\/2007-2013"],"award-info":[{"award-number":["FP7\/2007-2013"]}],"id":[{"id":"10.13039\/501100004963","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["258865"],"award-info":[{"award-number":["258865"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2013,2]]},"abstract":"<jats:p>Reasoning about the knowledge of an attacker is a necessary step in many formal analyses of security protocols. In the framework of the applied pi-calculus, as in similar languages based on equational logics, knowledge is typically expressed by two relations: deducibility and static equivalence. Several decision procedures have been proposed for these relations under a variety of equational theories. However, each theory has its particular algorithm, and none has been implemented so far.<\/jats:p>\n          <jats:p>We provide a generic procedure for deducibility and static equivalence that takes as input any convergent rewrite system. We show that our algorithm covers most of the existing decision procedures for convergent theories. We also provide an efficient implementation and compare it briefly with the tools ProVerif and KiSs.<\/jats:p>","DOI":"10.1145\/2422085.2422089","type":"journal-article","created":{"date-parts":[[2013,2,22]],"date-time":"2013-02-22T19:25:04Z","timestamp":1361561104000},"page":"1-32","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["YAPA"],"prefix":"10.1145","volume":"14","author":[{"given":"Mathieu","family":"Baudet","sequence":"first","affiliation":[{"name":"MLstate"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"V\u00e9ronique","family":"Cortier","sequence":"additional","affiliation":[{"name":"LORIA - CNRS"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"St\u00e9phanie","family":"Delaune","sequence":"additional","affiliation":[{"name":"LSV, ENS Cachan &amp; CNRS &amp; INRIA Saclay Ile-de-France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2013,2]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/11690634_27"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.l016\/j.tcs.2006.08.032"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360213"},{"key":"e_1_2_1_4_1","volume-title":"Proceedings of the 18th Conference on Term Rewriting and Applications (RTA\u201907)","volume":"4533","author":"Anantharaman S.","unstructured":"Anantharaman , S. , Narendran , P. , and Rusinowitch , M . 2007. Intruders with caps . In Proceedings of the 18th Conference on Term Rewriting and Applications (RTA\u201907) . Lecture Notes in Computer Science , vol. 4533 . Springer, Berlin. Anantharaman, S., Narendran, P., and Rusinowitch, M. 2007. Intruders with caps. In Proceedings of the 18th Conference on Term Rewriting and Applications (RTA\u201907). Lecture Notes in Computer Science, vol. 4533. Springer, Berlin."},{"key":"e_1_2_1_5_1","volume-title":"Proceeding of the 1st International Workshop on RFID Security and Cryptography.","author":"Arapinis M.","unstructured":"Arapinis , M. , Chothia , T. , Ritter , E. , and Ryan , M . 2009. Untraceability in the applied pi calculus . In Proceeding of the 1st International Workshop on RFID Security and Cryptography. Arapinis, M., Chothia, T., Ritter, E., and Ryan, M. 2009. Untraceability in the applied pi calculus. In Proceeding of the 1st International Workshop on RFID Security and Cryptography."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_27"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74621-8_7"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1102120.1102125"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02348-4_11"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/11523468_53"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/872752.873511"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2007.06.002"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/11921240_11"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14203-1_35"},{"key":"e_1_2_1_16_1","volume-title":"Proceedings of the 23rd Conference on Foundations of Software Technology and Theoretical Computer Science (FST&TCS&rsquo;\u201903)","volume":"2914","author":"Chevalier Y.","unstructured":"Chevalier , Y. , K\u00fcsters , R. , Rusinowitch , M. , and Turuani , M . 2003a. Deciding the security of protocols with Diffie-Hellman exponentiation and product in exponents . In Proceedings of the 23rd Conference on Foundations of Software Technology and Theoretical Computer Science (FST&TCS&rsquo;\u201903) . Lecture Notes in Computer Science , vol. 2914 . Springer-Verlag, Berlin, 124--135. Chevalier, Y., K\u00fcsters, R., Rusinowitch, M., and Turuani, M. 2003a. Deciding the security of protocols with Diffie-Hellman exponentiation and product in exponents. In Proceedings of the 23rd Conference on Foundations of Software Technology and Theoretical Computer Science (FST&TCS&rsquo;\u201903). Lecture Notes in Computer Science, vol. 2914. Springer-Verlag, Berlin, 124--135."},{"key":"e_1_2_1_17_1","volume-title":"Proceedings of the 18th IEEE Symposium on Logic in Computer Science (LICS\u201903)","author":"Chevalier Y.","unstructured":"Chevalier , Y. , K\u00fcsters , R. , Rusinowitch , M. , and Turuani , M . 2003b. An NP decision procedure for protocol insecurity with XOR . In Proceedings of the 18th IEEE Symposium on Logic in Computer Science (LICS\u201903) . Chevalier, Y., K\u00fcsters, R., Rusinowitch, M., and Turuani, M. 2003b. An NP decision procedure for protocol insecurity with XOR. In Proceedings of the 18th IEEE Symposium on Logic in Computer Science (LICS\u201903)."},{"key":"e_1_2_1_18_1","doi-asserted-by":"crossref","unstructured":"Chevalier Y. and Rusinowitch M. 2010. Decidability of symbolic equivalence of derivations. J. Autom. Reason.  Chevalier Y. and Rusinowitch M. 2010. Decidability of symbolic equivalence of derivations. J. Autom. Reason .","DOI":"10.1007\/s10817-010-9199-5"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02959-2_27"},{"key":"e_1_2_1_20_1","first-page":"5","article-title":"Is it possible to decide whether a cryptographic protocol is secure or not","volume":"4","author":"Comon H.","year":"2002","unstructured":"Comon , H. and Shmatikov , V. 2002 . Is it possible to decide whether a cryptographic protocol is secure or not ? J. Telecomm. Inf. Technol. 4\/2002 , 5 -- 15 . Comon, H. and Shmatikov, V. 2002. Is it possible to decide whether a cryptographic protocol is secure or not? J. Telecomm. Inf. Technol. 4\/2002, 5--15.","journal-title":"J. Telecomm. Inf. Technol."},{"key":"e_1_2_1_21_1","volume-title":"Proceedings of the 14th International Conference on Rewriting Techniques and Applications (RTA\u201903)","volume":"2706","author":"Comon-Lundh H.","unstructured":"Comon-Lundh , H. and Cortier , V . 2003. New decidability results for fragments of first-order logic and application to cryptographic protocols . In Proceedings of the 14th International Conference on Rewriting Techniques and Applications (RTA\u201903) . Lecture Notes in Computer Science , vol. 2706 . Springer-Verlag, Berlin, 148--164. Comon-Lundh, H. and Cortier, V. 2003. New decidability results for fragments of first-order logic and application to cryptographic protocols. In Proceedings of the 14th International Conference on Rewriting Techniques and Applications (RTA\u201903). Lecture Notes in Computer Science, vol. 2706. Springer-Verlag, Berlin, 148--164."},{"key":"e_1_2_1_22_1","volume-title":"Proceedings of the 18th IEEE Symposium on Logic in Computer Science (LICS\u201903)","author":"Comon-Lundh H.","unstructured":"Comon-Lundh , H. and Shmatikov , V . 2003a. Intruder deductions, constraint solving and insecurity decision in presence of exclusive or . In Proceedings of the 18th IEEE Symposium on Logic in Computer Science (LICS\u201903) . Comon-Lundh, H. and Shmatikov, V. 2003a. Intruder deductions, constraint solving and insecurity decision in presence of exclusive or. In Proceedings of the 18th IEEE Symposium on Logic in Computer Science (LICS\u201903)."},{"key":"e_1_2_1_23_1","volume-title":"Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science (LICS\u201903)","author":"Comon-Lundh H.","unstructured":"Comon-Lundh , H. and Shmatikov , V . 2003b. Intruder deductions, constraint solving and insecurity decision in presence of exclusive or . In Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science (LICS\u201903) . 271--280. Comon-Lundh, H. and Shmatikov, V. 2003b. Intruder deductions, constraint solving and insecurity decision in presence of exclusive or. In Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science (LICS\u201903). 271--280."},{"key":"e_1_2_1_24_1","volume-title":"Proceedings of the 2nd International Workshop on Security Issues with Petri Nets and other Computational Models (WISP\u201904)","author":"Corin R.","unstructured":"Corin , R. , Doumen , J. , and Etalle , S . 2004. Analysing password protocol security against off-line dictionary attacks . In Proceedings of the 2nd International Workshop on Security Issues with Petri Nets and other Computational Models (WISP\u201904) . Corin, R., Doumen, J., and Etalle, S. 2004. Analysing password protocol security against off-line dictionary attacks. In Proceedings of the 2nd International Workshop on Security Issues with Petri Nets and other Computational Models (WISP\u201904)."},{"key":"e_1_2_1_25_1","volume-title":"Proceedings of the 14th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR\u201907)","author":"Cortier V.","unstructured":"Cortier , V. and Delaune , S . 2007. Deciding knowledge in security protocols for monoidal equational theories . In Proceedings of the 14th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR\u201907) . Lecture Notes in Artificial Intelligence. Springer, Berlin. Cortier, V. and Delaune, S. 2007. Deciding knowledge in security protocols for monoidal equational theories. In Proceedings of the 14th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR\u201907). Lecture Notes in Artificial Intelligence. Springer, Berlin."},{"key":"e_1_2_1_26_1","first-page":"2006","article-title":"A survey of algebraic properties used in cryptographic protocols","volume":"14","author":"Cortier V.","year":"2006","unstructured":"Cortier , V. , Delaune , S. , and Lafourcade , P. 2006 a. A survey of algebraic properties used in cryptographic protocols . J. Comput. Secur. 14 , 1\/ 2006 . Cortier, V., Delaune, S., and Lafourcade, P. 2006a. A survey of algebraic properties used in cryptographic protocols. J. Comput. Secur. 14, 1\/2006.","journal-title":"J. Comput. Secur."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/1239376.1239377"},{"key":"e_1_2_1_28_1","volume-title":"Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201907)","volume":"4424","author":"Cortier V.","unstructured":"Cortier , V. , Keighren , G. , and Steel , G . 2007. Automatic analysis of the security of xor-based key management schemes . In Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201907) . Lecture Notes in Computer Science , vol. 4424 . Springer, Berlin, 538--552. Cortier, V., Keighren, G., and Steel, G. 2007. Automatic analysis of the security of xor-based key management schemes. In Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201907). Lecture Notes in Computer Science, vol. 4424. Springer, Berlin, 538--552."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02002-5_5"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1030083.1030121"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/1576303.1576305"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-88313-5_35"},{"key":"e_1_2_1_33_1","volume-title":"Proceedings of the Advances in Cryptology (AUSCRYPT\u201992)","volume":"718","author":"Fujioka A.","unstructured":"Fujioka , A. , Okamoto , T. , and Ohta , K . 1992. A practical secret voting scheme for large scale elections . In Proceedings of the Advances in Cryptology (AUSCRYPT\u201992) . Lecture Notes in Computer Science , vol. 718 . Springer, Berlin, 244--251. Fujioka, A., Okamoto, T., and Ohta, K. 1992. A practical secret voting scheme for large scale elections. In Proceedings of the Advances in Cryptology (AUSCRYPT\u201992). Lecture Notes in Computer Science, vol. 718. Springer, Berlin, 244--251."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2004.09.004"},{"key":"e_1_2_1_35_1","doi-asserted-by":"crossref","unstructured":"K\u00fcsters R. and Truderung T. 2010. Reducing protocol analysis with XOR to the XOR-free case in the Horn theory based approach. J. Autom. Reason. To appear.  K\u00fcsters R. and Truderung T. 2010. Reducing protocol analysis with XOR to the XOR-free case in the Horn theory based approach. J. Autom. Reason . To appear.","DOI":"10.1007\/s10817-010-9188-8"},{"key":"e_1_2_1_36_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201996)","author":"Lowe G.","unstructured":"Lowe , G. 1996. Breaking and fixing the Needham-Schroeder public-key protocol using FDR . In Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201996) . Lecture Notes in Computer Science , vol. 1055 . Springer-Verlag , Berlin , 147--166. Lowe, G. 1996. Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201996). Lecture Notes in Computer Science, vol. 1055. Springer-Verlag, Berlin, 147--166."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/501983.502007"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03829-7_6"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02348-4_9"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24725-8_25"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2010.28"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/11805618_21"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.5555\/1759148.1759163"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2422085.2422089","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2422085.2422089","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T08:18:35Z","timestamp":1750234715000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2422085.2422089"}},"subtitle":["A Generic Tool for Computing Intruder Knowledge"],"short-title":[],"issued":{"date-parts":[[2013,2]]},"references-count":42,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2013,2]]}},"alternative-id":["10.1145\/2422085.2422089"],"URL":"https:\/\/doi.org\/10.1145\/2422085.2422089","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,2]]},"assertion":[{"value":"2010-05-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-01-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-02-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}