{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T19:10:32Z","timestamp":1694632232538},"reference-count":32,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2008,5,1]],"date-time":"2008-05-01T00:00:00Z","timestamp":1209600000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2008,5]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>This paper addresses the problem of representing the intruder\u2019s knowledge in the formal verification of cryptographic protocols, whose main challenges are to represent the intruder\u2019s knowledge efficiently and without artificial limitations on the structure and size of messages. The new knowledge representation strategy proposed in this paper achieves both goals and leads to practical implementation because it is incrementally computable and is easily amenable to work with various term representation languages. In addition, it handles associative and commutative term composition operators, thus going beyond the free term algebra framework. An extensive computational complexity analysis of the proposed representation strategy is included in the paper.<\/jats:p>","DOI":"10.1007\/s00165-008-0078-3","type":"journal-article","created":{"date-parts":[[2008,4,28]],"date-time":"2008-04-28T13:09:35Z","timestamp":1209388175000},"page":"303-348","source":"Crossref","is-referenced-by-count":1,"title":["Efficient representation of the attacker\u2019s knowledge in cryptographic protocols analysis"],"prefix":"10.1145","volume":"20","author":[{"given":"Ivan Cibrario","family":"Bertolotti","sequence":"first","affiliation":[{"name":"IEIIT-CNR, C.so Duca degli Abruzzi 24, 10129, Torino, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luca","family":"Durante","sequence":"additional","affiliation":[{"name":"IEIIT-CNR, C.so Duca degli Abruzzi 24, 10129, Torino, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Riccardo","family":"Sisto","sequence":"additional","affiliation":[{"name":"Politecnico di Torino, C.so Duca degli Abruzzi 24, 10129, Torino, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adriano","family":"Valenzano","sequence":"additional","affiliation":[{"name":"IEIIT-CNR, C.so Duca degli Abruzzi 24, 10129, Torino, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1998.2740"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Amadio RM Lugiez D (2000) On the reachability problem in cryptographic protocols. In: Proceedings of the 11th international conference on concurrency theory (CONCUR 2000) vol 1877 of Lecture Notes in Computer Science pp 380\u2013394 Springer Berlin","DOI":"10.1007\/3-540-44618-4_28"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Boreale M Buscemi MG (2002) A framework for the analysis of security protocols. In: Proceedings of the 13th International Conference on Concurrency Theory (CONCUR 2002). Lecture Notes in Computer Science vol 2421. Springer Berlin pp 483\u2013498","DOI":"10.1007\/3-540-45694-5_32"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539700377864"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Blanchet B (2001) An efficient cryptographic protocol verifier based on prolog rules. In: Proceedings of the 14th IEEE computer security foundations workshop (CSFW-14) Cape Breton. IEEE Computer Society Washington pp 82\u201396","DOI":"10.1109\/CSFW.2001.930138"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10207-004-0055-7"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Boreale M (2001) Symbolic trace analysis of cryptographic protocols. In: Proceedings of the 28th international colloquium on automata languages and programming (ICALP 2001). Lecture Notes in Computer Science vol 2076. Springer Berlin pp 667\u2013681","DOI":"10.1007\/3-540-48224-5_55"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Cibrario Bertolotti I Durante L Sisto R Valenzano A (2003) Introducing commutative and associative operators in cryptographic protocol analysis. In: Proceedings of the 23rd IFIP international conference on formal techniques for networked and distributed systems (FORTE 2003). Lecture Notes in Computer Science vol 2767. Springer Berlin pp 224\u2013239","DOI":"10.1007\/978-3-540-39979-7_15"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Cibrario Bertolotti I Durante L Sisto R Valenzano A (2003) A new knowledge representation strategy for cryptographic protocol analysis. In: Proceedings of tools and algoritms for the construction and analysis of systems (TACAS 2003). Lecture Notes in Computer Science vol 2619. Springer Berlin pp 284\u2013298","DOI":"10.1007\/3-540-36577-X_21"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Clarke EM Jha S Marrero W (1998) Using state space exploration and a natural deduction style message derivation engine to verify security protocols. In: Proceedings of the IFIP working conference on programming concepts and methods (PROCOMET 1998). Chapman & Hall London pp 87\u2013106","DOI":"10.1007\/978-0-387-35358-6_10"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/363516.363528"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Chevalier Y K\u00fcsters R Rusinowitch M Turuani M (2003) An NP decision procedure for protocol insecurity with XOR. In: Proceedings of the 18th IEEE symposium on logic in computer science (LICS 2003). IEEE Computer Society Press Washington pp 261\u2013170. doi:10.1109\/LICS.2003.1210066","DOI":"10.1109\/LICS.2003.1210066"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Comon-Lundh H Shmatikov V (2003) 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 2003). IEEE Computer Society Press Washington pp 271\u2013280. doi:10.1109\/LICS.2003.1210067","DOI":"10.1109\/LICS.2003.1210067"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1976.1055638"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/941566.941570"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Fiore M Abadi M (2001) Computing symbolic models for verifying cryptographic protocols. In: Proceedings of the 14th IEEE computer security foundations workshop (CSFW 2001). IEEE Computer Society Press Washington pp 160\u2013173. doi:10.1109\/CSFW.2001.930144","DOI":"10.1109\/CSFW.2001.930144"},{"key":"e_1_2_1_2_18_2","unstructured":"Huima A (1999) Efficient infinite-state analysis of security protocols. In: Proceedings of the FLOC workshop on formal methods and security protocols"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Lowe G (1996) Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: Proceedings of tools and algoritms for the construction and analysis of systems (TACAS 1996). Lecture Notes in Computer Science vol 1055. Springer Berlin pp 147\u2013166","DOI":"10.1007\/3-540-61042-1_43"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Lowe G (1997) Casper: a compiler for the analysis of security protocols. In: Proceedings of the 10th IEEE computer security foundations workshop (CSFW 1997). IEEE Computer Society Press Washington pp 18\u201330. doi:10.1109\/CSFW.1997.596779","DOI":"10.1109\/CSFW.1997.596779"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.5555\/353594.353597"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/151261.151265"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Marrero W Clarke EM Jha S (1997) A model checker for authentication protocols. In: Proceedings of the DIMACS workshop on design and formal verification of security protocols","DOI":"10.21236\/ADA327281"},{"key":"e_1_2_1_2_24_2","unstructured":"Meadows C Narendran P (2002) A unification algorithm for the group Diffie\u2013Hellman protocol. In: Proceedings of WITS\u201902"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Monniaux D (1999) Abstracting cryptographic protocols with tree automata. In: Proceedings of the 6th international static analysis symposium (SAS 1999). Lecture Notes in Computer Science vol 1694. Springer Berlin pp 149\u2013163","DOI":"10.1007\/3-540-48294-6_10"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90008-4"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Millen JK Shmatikov V (2001) Constraint solving for bounded-process cryptographic protocol analysis. In: Proceedings of the 8th ACM conference on computer and communications security (CCS 2001). ACM Press New York pp 166\u2013175. doi:10.1145\/501983.502007","DOI":"10.1145\/501983.502007"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Millen JK Shmatikov V (2003) Symbolic protocol analysis with products and Diffie\u2013Hellman exponentiation. In: Proceedings of the 16th IEEE computer security foundations workshop (CSFW 2003). IEEE Computer Society Press Washington pp 47\u201361. doi:10.1109\/CSFW.2003.1212704","DOI":"10.1109\/CSFW.2003.1212704"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"publisher","DOI":"10.5555\/353677.353681"},{"key":"e_1_2_1_2_30_2","volume-title":"Natural deduction: a proof-theoretical study","author":"Prawitz D","year":"1965"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Rusinowitch M Turuani M (2001) Protocol insecurity with finite number of sessions is NP-complete. In: Proceedings of the 14th IEEE computer security foundations workshop (CSFW 2001). IEEE Computer Society Press Washington pp 174\u2013187. doi:10.1109\/CSFW.2001.930145","DOI":"10.1109\/CSFW.2001.930145"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.713329"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-008-0078-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-008-0078-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-008-0078-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:45:39Z","timestamp":1641483939000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-008-0078-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,5]]},"references-count":32,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2008,5]]}},"alternative-id":["10.1007\/s00165-008-0078-3"],"URL":"https:\/\/doi.org\/10.1007\/s00165-008-0078-3","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,5]]}}}