{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:41:50Z","timestamp":1750308110024,"version":"3.41.0"},"reference-count":34,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2005,8,1]],"date-time":"2005-08-01T00:00:00Z","timestamp":1122854400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Inf. Syst. Secur."],"published-print":{"date-parts":[[2005,8]]},"abstract":"<jats:p>Security protocols are one of the most critical elements in enabling the secure communication and processing of information. The presence of flaws in published protocols highlights the complexity of security protocol design. Only formal verification can provide strong confidence in the correctness of security protocols and is considered an imperative step in their design. This paper presents a new theoretical concept, called Layered Proving Trees, for automatically applying logical postulates in logic-based security protocol verification.An algorithm for the new concept is introduced and the soundness and completeness of the technique is proved. Empirical results on the performance of the algorithm are presented. The presented proofs and empirical results demonstrate the feasibility and effectiveness of the Layered Proving Tree approach.<\/jats:p>","DOI":"10.1145\/1085126.1085128","type":"journal-article","created":{"date-parts":[[2005,11,7]],"date-time":"2005-11-07T16:00:45Z","timestamp":1131379245000},"page":"287-311","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":14,"title":["The concept of layered proving trees and its application to the automation of security protocol verification"],"prefix":"10.1145","volume":"8","author":[{"given":"Reiner","family":"Dojen","sequence":"first","affiliation":[{"name":"University of Limerick, Ireland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tom","family":"Coffey","sequence":"additional","affiliation":[{"name":"University of Limerick, Ireland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2005,8]]},"reference":[{"volume-title":"Proceedings of 2nd International Workshop on Discrete Algorithms and Methods for Mobility (DIAL M 98)","author":"Aydos M.","unstructured":"Aydos , M. , Sunar , B. , and Koc , C. K . 1998. An elliptic curve cryptography based authentication and key agreement protocol for wireless communication . In Proceedings of 2nd International Workshop on Discrete Algorithms and Methods for Mobility (DIAL M 98) , Dallas, TX October. 1--12. Aydos, M., Sunar, B., and Koc, C. K. 1998. An elliptic curve cryptography based authentication and key agreement protocol for wireless communication. In Proceedings of 2nd International Workshop on Discrete Algorithms and Methods for Mobility (DIAL M 98), Dallas, TX October. 1--12.","key":"e_1_2_1_1_1"},{"key":"e_1_2_1_2_1","doi-asserted-by":"crossref","first-page":"821","DOI":"10.1109\/49.232291","article-title":"Privacy and authentication on a portable communications system","volume":"11","author":"Beller M. J.","year":"1993","unstructured":"Beller , M. J. , Chang , L.-F. , and Yacobi , Y. 1993 . Privacy and authentication on a portable communications system . IEEE Journal on Selected Areas in Communications 11 , 6, 821 -- 829 . Beller, M. J., Chang, L.-F., and Yacobi, Y. 1993. Privacy and authentication on a portable communications system. IEEE Journal on Selected Areas in Communications 11, 6, 821--829.","journal-title":"IEEE Journal on Selected Areas in Communications"},{"key":"e_1_2_1_3_1","volume-title":"Proceedings of the 3rd Computer Security Foundation Workshop","author":"Bieber P.","year":"1990","unstructured":"Bieber , P. 1990 . A logic of communication in a hostile environment . In Proceedings of the 3rd Computer Security Foundation Workshop . Washington, USA. 14--22. Bieber, P. 1990. A logic of communication in a hostile environment. In Proceedings of the 3rd Computer Security Foundation Workshop. Washington, USA. 14--22."},{"key":"e_1_2_1_4_1","volume-title":"DARPA Information Survivability Conference and Exposition","volume":"1","author":"Brackin S.","year":"2000","unstructured":"Brackin , S. 2000 . Automatically detecting most vulnerabilities in Cryptographic protocols . In DARPA Information Survivability Conference and Exposition Vol. 1 , January. Hilton Head, South Carolina, 222--236. Brackin, S. 2000. Automatically detecting most vulnerabilities in Cryptographic protocols. In DARPA Information Survivability Conference and Exposition Vol.1, January. Hilton Head, South Carolina, 222--236."},{"doi-asserted-by":"publisher","key":"e_1_2_1_5_1","DOI":"10.1145\/77648.77649"},{"doi-asserted-by":"publisher","key":"e_1_2_1_6_1","DOI":"10.1145\/182110.182112"},{"key":"e_1_2_1_7_1","volume-title":"12th IEEE Computer Security Foundations Workshop","author":"Cervesato I.","year":"1999","unstructured":"Cervesato , I. , Durgin , N. , Lincoln , P. , Mitchell , J. , and Scedrov , A . 1999. A meta-notation for protocol analysis . In: 12th IEEE Computer Security Foundations Workshop , Mordano, Italy , June 1999 , 55--72. Cervesato, I., Durgin, N., Lincoln, P., Mitchell, J., and Scedrov, A. 1999. A meta-notation for protocol analysis. In: 12th IEEE Computer Security Foundations Workshop, Mordano, Italy, June 1999, 55--72."},{"key":"e_1_2_1_8_1","doi-asserted-by":"crossref","first-page":"28","DOI":"10.1049\/ip-cdt:19970838","article-title":"A logic for verifying public key cryptographic protocols","volume":"144","author":"Coffey T.","year":"1997","unstructured":"Coffey , T. and Saidha , P. 1997 . A logic for verifying public key cryptographic protocols . IEE Journal of Computers and Digital Techniques 144 , 1, 28 -- 32 . Coffey, T. and Saidha, P. 1997. A logic for verifying public key cryptographic protocols. IEE Journal of Computers and Digital Techniques 144, 1, 28--32.","journal-title":"IEE Journal of Computers and Digital Techniques"},{"doi-asserted-by":"publisher","key":"e_1_2_1_9_1","DOI":"10.1016\/S1389-1286(03)00292-5"},{"volume-title":"Proceedings of ISICT'03 (Invited Workshop on Network Security and Management at the International Symposium on Information and Communication Technologies). September","author":"Coffey T.","unstructured":"Coffey , T. , Dojen , R. , and Flanagan , T . 2003b. On the Automated implementation of modal logics used to verify security protocols . In Proceedings of ISICT'03 (Invited Workshop on Network Security and Management at the International Symposium on Information and Communication Technologies). September . Dublin, Ireland. 324--347. Coffey, T., Dojen, R., and Flanagan, T. 2003b. On the Automated implementation of modal logics used to verify security protocols. In Proceedings of ISICT'03 (Invited Workshop on Network Security and Management at the International Symposium on Information and Communication Technologies). September. Dublin, Ireland. 324--347.","key":"e_1_2_1_10_1"},{"volume-title":"Proceedings of SAM'03 (Conference on Security and Management)","author":"Coffey T.","unstructured":"Coffey , T. , Dojen , R. , and Flanagan , T . 2003c. On different approaches to establish the security of Cryptographic Protocols . In Proceedings of SAM'03 (Conference on Security and Management) , Vol. II , June. Las Vegas, NV, 637--643. Coffey, T., Dojen, R., and Flanagan, T. 2003c. On different approaches to establish the security of Cryptographic Protocols. In Proceedings of SAM'03 (Conference on Security and Management), Vol. II, June. Las Vegas, NV, 637--643.","key":"e_1_2_1_11_1"},{"volume-title":"Proceedings of IEEE International Conference on Intelligent Engineering Systems (INES2004)","author":"Coffey T.","unstructured":"Coffey , T. , Ventuneac , M. , Newe , T. , and Salomie , S . 2004. On investigating the security and fairness of a fair exchange protocol using logic-based verification . In Proceedings of IEEE International Conference on Intelligent Engineering Systems (INES2004) , September. Cluj-Napoca, Romania, 325--330. Coffey, T., Ventuneac, M., Newe, T., and Salomie, S. 2004. On investigating the security and fairness of a fair exchange protocol using logic-based verification. In Proceedings of IEEE International Conference on Intelligent Engineering Systems (INES2004), September. Cluj-Napoca, Romania, 325--330.","key":"e_1_2_1_12_1"},{"key":"e_1_2_1_13_1","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1007\/BF00196790","article-title":"Applying a formal analysis technique to the CCITT X.509 strong two-way authentication protocol","volume":"3","author":"Gaarder K.","year":"1991","unstructured":"Gaarder , K. and Snekkenes , E. 1991 . Applying a formal analysis technique to the CCITT X.509 strong two-way authentication protocol . Journal of Cryptology 3 , 81 -- 98 . Gaarder, K. and Snekkenes, E. 1991. Applying a formal analysis technique to the CCITT X.509 strong two-way authentication protocol. Journal of Cryptology 3, 81--98.","journal-title":"Journal of Cryptology"},{"volume-title":"Proceedings of the IEEE Computer Security Symposium on Security and Privacy, May","author":"Gong L.","unstructured":"Gong , L. , Needham , R. , and Yahalom , R . 1990. Reasoning about belief in cryptographic protocols . In Proceedings of the IEEE Computer Security Symposium on Security and Privacy, May . Oakland, CA, 234--248. Gong, L., Needham, R., and Yahalom, R. 1990. Reasoning about belief in cryptographic protocols. In Proceedings of the IEEE Computer Security Symposium on Security and Privacy, May. Oakland, CA, 234--248.","key":"e_1_2_1_14_1"},{"key":"e_1_2_1_15_1","volume-title":"HOL: A Theorem Proving Environment for Higher Order Logic","author":"Gordon M.","year":"1993","unstructured":"Gordon , M. and Melham , T. F . 1993 . Introduction to HOL: A Theorem Proving Environment for Higher Order Logic . Cambridge University Press , Cambridge . Gordon, M. and Melham, T. F. 1993. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge."},{"key":"e_1_2_1_16_1","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1007\/978-3-540-40981-6_10","article-title":"Security analysis of (Un-)fair Non-repudiation protocols. Formal Aspects of Security","volume":"2629","author":"G\u00fcrgens S.","year":"2002","unstructured":"G\u00fcrgens , S. and Rudolph , C. 2002 . Security analysis of (Un-)fair Non-repudiation protocols. Formal Aspects of Security , Lecture Notes in Computer Science 2629 , 97 -- 114 . G\u00fcrgens, S. and Rudolph, C. 2002. Security analysis of (Un-)fair Non-repudiation protocols. Formal Aspects of Security, Lecture Notes in Computer Science 2629, 97--114.","journal-title":"Lecture Notes in Computer Science"},{"key":"e_1_2_1_17_1","doi-asserted-by":"crossref","first-page":"383","DOI":"10.1109\/25.994813","article-title":"Authentication protocols for mobile network environment value-added services","volume":"51","author":"Horn G","year":"2002","unstructured":"Horn , G , Martin , K. and Mitchell , C. 2002 . Authentication protocols for mobile network environment value-added services . IEEE Transactions on Vehicular Technology 51 , 2, 383 -- 392 . Horn, G, Martin, K. and Mitchell, C. 2002. Authentication protocols for mobile network environment value-added services. IEEE Transactions on Vehicular Technology 51, 2, 383--392.","journal-title":"IEEE Transactions on Vehicular Technology"},{"key":"e_1_2_1_18_1","doi-asserted-by":"crossref","DOI":"10.3233\/JCS-2000-82-306","article-title":"Authentication and payment in future mobile systems","volume":"8","author":"Horn G.","year":"2000","unstructured":"Horn , G. and Preneel , H. 2000 . Authentication and payment in future mobile systems . Journal of Computer Security 8 , 2\/3, 183--207. Horn, G. and Preneel, H. 2000. Authentication and payment in future mobile systems. Journal of Computer Security 8, 2\/3, 183--207.","journal-title":"Journal of Computer Security"},{"volume-title":"Proceedings of the Second Workshop on Logical Frameworks, May","author":"Huet G.","unstructured":"Huet , G. , Felty , A. , Werner , B. , Herbelin , H. , and Dowek , H . 1991. Presenting the system Coq, version 5.6 . In Proceedings of the Second Workshop on Logical Frameworks, May . Edinburgh, UK. Huet, G., Felty, A., Werner, B., Herbelin, H., and Dowek, H. 1991. Presenting the system Coq, version 5.6. In Proceedings of the Second Workshop on Logical Frameworks, May. Edinburgh, UK.","key":"e_1_2_1_19_1"},{"key":"e_1_2_1_20_1","volume-title":"Proceedings of FLOC'99 Workshop on Formal Methods and Security Protocols, July.","author":"Huima A.","year":"1999","unstructured":"Huima A. 1999 . Efficient infinite-state analysis of security protocols . In Proceedings of FLOC'99 Workshop on Formal Methods and Security Protocols, July. Huima A. 1999. Efficient infinite-state analysis of security protocols. In Proceedings of FLOC'99 Workshop on Formal Methods and Security Protocols, July."},{"volume-title":"Proceedings of 7th IEEE Computer Security Foundations, August","author":"Kessler V.","unstructured":"Kessler , V. and Wendel , G . 1994. AUTLOG---An advanced logic of authentication . In Proceedings of 7th IEEE Computer Security Foundations, August . Menlo Park, California, 90--99. Kessler, V. and Wendel, G. 1994. AUTLOG---An advanced logic of authentication. In Proceedings of 7th IEEE Computer Security Foundations, August. Menlo Park, California, 90--99.","key":"e_1_2_1_21_1"},{"volume-title":"Proceedings of 1st Australasian Conference on Information Security and Privacy","author":"Mu Y.","unstructured":"Mu , Y. and Varadharajan , V . 1996. On the design of security protocols for mobile communications, Information security and Privacy . In Proceedings of 1st Australasian Conference on Information Security and Privacy , Wollongong, Australia, June. 134--145. Mu, Y. and Varadharajan, V. 1996. On the design of security protocols for mobile communications, Information security and Privacy. In Proceedings of 1st Australasian Conference on Information Security and Privacy, Wollongong, Australia, June. 134--145.","key":"e_1_2_1_22_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_23_1","DOI":"10.1145\/359657.359659"},{"doi-asserted-by":"publisher","key":"e_1_2_1_24_1","DOI":"10.1145\/24592.24593"},{"key":"e_1_2_1_25_1","first-page":"17","article-title":"Formal Verification logic for hybrid security protocols","volume":"18","author":"Newe T.","year":"2003","unstructured":"Newe T. and Coffey T. 2003 . Formal Verification logic for hybrid security protocols . International Journal of Computer Systems Science & Engineering 18 , 1, 17 -- 25 . Newe T. and Coffey T. 2003. Formal Verification logic for hybrid security protocols. International Journal of Computer Systems Science & Engineering 18, 1, 17--25.","journal-title":"International Journal of Computer Systems Science & Engineering"},{"volume-title":"Proceedings of Computer-Aided Verification, CAV '96","author":"Owre S.","unstructured":"Owre , S. , Rajan , S. , Rushby , J. M. , Shankar , N. , and Srivas , M. K . 1996. PVS: Combining specification, proof checking, and model checking . In Proceedings of Computer-Aided Verification, CAV '96 , July\/August. New Brunswick, NJ, 411--414. Owre, S., Rajan, S., Rushby, J. M., Shankar, N., and Srivas, M. K. 1996. PVS: Combining specification, proof checking, and model checking. In Proceedings of Computer-Aided Verification, CAV '96, July\/August. New Brunswick, NJ, 411--414.","key":"e_1_2_1_26_1"},{"key":"e_1_2_1_27_1","volume-title":"Isabelle: The next 700 therorem provers","author":"Paulson L. C.","year":"1991","unstructured":"Paulson , L. C. 1991 . Isabelle: The next 700 therorem provers . In Odifreddi, P. (Ed.), Logic and Computer Science, Academic Press , New York , 361--386. Paulson, L. C. 1991. Isabelle: The next 700 therorem provers. In Odifreddi, P. (Ed.), Logic and Computer Science, Academic Press, New York, 361--386."},{"key":"e_1_2_1_28_1","volume-title":"Proceedings of 8th IEEE Computer Security Foundations Workshop, June","author":"Roscoe A. W.","year":"1995","unstructured":"Roscoe A. W. 1995 . Modelling and verifying key-exchange protocols using CSP and FDR , In Proceedings of 8th IEEE Computer Security Foundations Workshop, June . Kenmare, Ireland, 98. Roscoe A. W. 1995. Modelling and verifying key-exchange protocols using CSP and FDR, In Proceedings of 8th IEEE Computer Security Foundations Workshop, June. Kenmare, Ireland, 98."},{"key":"e_1_2_1_29_1","volume-title":"Proceedings of the 11th IEEE Computer Security Foundations Workshop, June","author":"Schneider S.","year":"1998","unstructured":"Schneider , S. 1998 . Formal Analysis of a Non-Repudiation Protocol . In Proceedings of the 11th IEEE Computer Security Foundations Workshop, June . Rockport, IL, 54--65. Schneider, S. 1998. Formal Analysis of a Non-Repudiation Protocol. In Proceedings of the 11th IEEE Computer Security Foundations Workshop, June. Rockport, IL, 54--65."},{"key":"e_1_2_1_30_1","volume-title":"Proceedings of the 1991 IEEE Computer Society Symposium on Research in Security and Privacy, May","author":"Syverson P.","year":"1991","unstructured":"Syverson , P. 1991 . The use of logic in the analysis of cryptographic protocols . In Proceedings of the 1991 IEEE Computer Society Symposium on Research in Security and Privacy, May . Oakland, CA. 156--170. Syverson, P. 1991. The use of logic in the analysis of cryptographic protocols. In Proceedings of the 1991 IEEE Computer Society Symposium on Research in Security and Privacy, May. Oakland, CA. 156--170."},{"volume-title":"Proceedings of Advances in Cryptology---EUROCRYPT'94","author":"Syverson P.","unstructured":"Syverson P. and Meadows C . 1995. Formal requirements for key distribution protocols . In Proceedings of Advances in Cryptology---EUROCRYPT'94 , May. Perugia, Italy, 320--331. Syverson P. and Meadows C. 1995. Formal requirements for key distribution protocols. In Proceedings of Advances in Cryptology---EUROCRYPT'94, May. Perugia, Italy, 320--331.","key":"e_1_2_1_31_1"},{"volume-title":"Proceedings of the 13th IEEE Symposium on Security and Privacy. May","author":"Syverson P.F.","unstructured":"Syverson , P.F. and van Oorschot, P.C. 1994. On unifying some cryptographic protocols logics . In Proceedings of the 13th IEEE Symposium on Security and Privacy. May . Oakland, CA, 14--28. Syverson, P.F. and van Oorschot, P.C. 1994. On unifying some cryptographic protocols logics. In Proceedings of the 13th IEEE Symposium on Security and Privacy. May. Oakland, CA, 14--28.","key":"e_1_2_1_32_1"},{"volume-title":"Proceedings of 24th Australasian Computer Science Conference, January. Gold Coast","author":"Zhang Y.","unstructured":"Zhang , Y. and Varadharajan , V . 2001. A logic for modelling the dynamics of beliefs in cryptographic protocols . In Proceedings of 24th Australasian Computer Science Conference, January. Gold Coast , Queensland, Australia, 215--222 Zhang, Y. and Varadharajan, V. 2001. A logic for modelling the dynamics of beliefs in cryptographic protocols. In Proceedings of 24th Australasian Computer Science Conference, January. Gold Coast, Queensland, Australia, 215--222","key":"e_1_2_1_33_1"},{"volume-title":"Proceedings of 1996 IEEE Symposium on Security and Privacy, May","author":"Zhou J.","unstructured":"Zhou , J. and Gollmann , C . 1996. A fair non-repudiation protocol . In Proceedings of 1996 IEEE Symposium on Security and Privacy, May . Oakland, CA, 55--61. Zhou, J. and Gollmann, C. 1996. A fair non-repudiation protocol. In Proceedings of 1996 IEEE Symposium on Security and Privacy, May. Oakland, CA, 55--61.","key":"e_1_2_1_34_1"}],"container-title":["ACM Transactions on Information and System Security"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1085126.1085128","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1085126.1085128","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T16:08:10Z","timestamp":1750262890000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1085126.1085128"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,8]]},"references-count":34,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2005,8]]}},"alternative-id":["10.1145\/1085126.1085128"],"URL":"https:\/\/doi.org\/10.1145\/1085126.1085128","relation":{},"ISSN":["1094-9224","1557-7406"],"issn-type":[{"type":"print","value":"1094-9224"},{"type":"electronic","value":"1557-7406"}],"subject":[],"published":{"date-parts":[[2005,8]]},"assertion":[{"value":"2005-08-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}