{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T08:39:12Z","timestamp":1774946352528,"version":"3.50.1"},"reference-count":22,"publisher":"Association for Computing Machinery (ACM)","issue":"2","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Inf. Syst. Secur."],"published-print":{"date-parts":[[2006,5]]},"abstract":"<jats:p>\n            Classical security protocols aim to achieve authentication and confidentiality under the assumption that the peers behave honestly. Some recent protocols are required to achieve their goals even if the peer misbehaves.\n            <jats:italic>Accountability<\/jats:italic>\n            is a protocol design strategy that may help. It delivers to peers sufficient evidence of each other's participation in the protocol. Accountability underlies the nonrepudiation protocol of Zhou and Gollmann and the certified email protocol of Abadi et al. This paper provides a comparative, formal analysis of the two protocols, and confirms that they reach their goals under realistic conditions. The treatment, which is conducted with mechanized support from the proof assistant Isabelle, requires various extensions to the existing analysis method. A byproduct is an account of the concept of\n            <jats:italic>higher-level protocol<\/jats:italic>\n            .\n          <\/jats:p>","DOI":"10.1145\/1151414.1151416","type":"journal-article","created":{"date-parts":[[2006,10,18]],"date-time":"2006-10-18T18:11:32Z","timestamp":1161195092000},"page":"138-161","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":26,"title":["Accountability protocols"],"prefix":"10.1145","volume":"9","author":[{"given":"Giampaolo","family":"Bella","sequence":"first","affiliation":[{"name":"Universit\u00e0 di Catania, Catania, ITALY"}]},{"given":"Lawrence C.","family":"Paulson","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, UK"}]}],"member":"320","published-online":{"date-parts":[[2006,5]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"10th International Symposium (SAS'03)","volume":"2694","author":"Abadi M.","unstructured":"Abadi , M. and Blanchet , B . 2003. Computer-assisted verification of a protocol for certified email. In Static Analysis , 10th International Symposium (SAS'03) , R. Cousot, Ed. Lecture Notes in Comp. Sci. , vol. 2694 . Springer-Verlag, New York. 316--335.]] Abadi, M. and Blanchet, B. 2003. Computer-assisted verification of a protocol for certified email. In Static Analysis, 10th International Symposium (SAS'03), R. Cousot, Ed. Lecture Notes in Comp. Sci., vol. 2694. Springer-Verlag, New York. 316--335.]]"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/511446.511497"},{"key":"e_1_2_1_3_1","volume-title":"Proc. of the 17th IEEE Sym. on Sec. and Privacy. IEEE Comp","author":"Asokan N.","unstructured":"Asokan , N. , Shoup , V. , and Waidner , M . 1998a. Asynchronous protocols for optimistic fair exchange . In Proc. of the 17th IEEE Sym. on Sec. and Privacy. IEEE Comp . Society Press, New York. 86--99.]] Asokan, N., Shoup, V., and Waidner, M. 1998a. Asynchronous protocols for optimistic fair exchange. In Proc. of the 17th IEEE Sym. on Sec. and Privacy. IEEE Comp. Society Press, New York. 86--99.]]"},{"key":"e_1_2_1_4_1","volume-title":"Proc. of the 17th IEEE Sym. on Sec. and Privacy. IEEE Comp. Society Press.]]","author":"Asokan N.","unstructured":"Asokan , N. , Shoup , V. , and Waidner , M . 1998b. Asynchronous protocols for optimistic fair exchange . In Proc. of the 17th IEEE Sym. on Sec. and Privacy. IEEE Comp. Society Press.]] Asokan, N., Shoup, V., and Waidner, M. 1998b. Asynchronous protocols for optimistic fair exchange. In Proc. of the 17th IEEE Sym. on Sec. and Privacy. IEEE Comp. Society Press.]]"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/773065.773068"},{"key":"e_1_2_1_7_1","doi-asserted-by":"crossref","unstructured":"Bella G. Longo C. and Paulson L. C. 2003. Verifying second-level security protocols. In Theorem proving in higher order logics: TPHOLs 2003 D. Basin and B. Wolff Eds. LNCS 2758. Springer-Verlag New York. 352--366.]]  Bella G. Longo C. and Paulson L. C. 2003. Verifying second-level security protocols. In Theorem proving in higher order logics: TPHOLs 2003 D. Basin and B. Wolff Eds. LNCS 2758. Springer-Verlag New York. 352--366.]]","DOI":"10.1007\/10930755_23"},{"key":"e_1_2_1_8_1","volume-title":"Eds. Lecture Notes in Comp. Sci.","volume":"2152","author":"Bella G.","unstructured":"Bella , G. and Paulson , L. C . 2001. Mechanical proofs about a nonrepudiation protocol. In Theorem proving in higher order logics: TPHOLs 2001, R. J. Boulton and P. B. Jackson , Eds. Lecture Notes in Comp. Sci. , vol. 2152 . Springer-Verlag, New York. 91--104.]] Bella, G. and Paulson, L. C. 2001. Mechanical proofs about a nonrepudiation protocol. In Theorem proving in higher order logics: TPHOLs 2001, R. J. Boulton and P. B. Jackson, Eds. Lecture Notes in Comp. Sci., vol. 2152. Springer-Verlag, New York. 91--104.]]"},{"key":"e_1_2_1_9_1","volume-title":"Proc. of the 14th IEEE Comp. Sec. Found. Workshop. IEEE Comp. Society Press.]]","author":"Blanchet B.","year":"1998","unstructured":"Blanchet , B. 1998 . An efficient cryptographic protocol verifier based on Prolog rules . In Proc. of the 14th IEEE Comp. Sec. Found. Workshop. IEEE Comp. Society Press.]] Blanchet, B. 1998. An efficient cryptographic protocol verifier based on Prolog rules. In Proc. of the 14th IEEE Comp. Sec. Found. Workshop. IEEE Comp. Society Press.]]"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1098\/rspa.1989.0125"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/794200.795136"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02139147"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.21236\/ADA459060"},{"key":"e_1_2_1_14_1","volume-title":"Technical Report CSD-TR-02-13.]]","author":"G\u00fcrgens S.","year":"2002","unstructured":"G\u00fcrgens , S. and Rudolph , C . 2002 . Security analysis of (un-) fair non-repudiation protocols. In Formal Aspects of Security, A. Abdallah, P. Ryan, and S. Schneider, Eds . Technical Report CSD-TR-02-13.]] G\u00fcrgens, S. and Rudolph, C. 2002. Security analysis of (un-) fair non-repudiation protocols. In Formal Aspects of Security, A. Abdallah, P. Ryan, and S. Schneider, Eds. Technical Report CSD-TR-02-13.]]"},{"key":"e_1_2_1_15_1","volume-title":"VISA","author":"Mastercard","year":"1997","unstructured":"Mastercard & VISA 1997 . SET Secure Electronic Transaction Specification : Business Description. Mastercard & VISA. On the Internet at http:\/\/www.setco.org\/set_specifications.html.]] Mastercard & VISA 1997. SET Secure Electronic Transaction Specification: Business Description. Mastercard & VISA. On the Internet at http:\/\/www.setco.org\/set_specifications.html.]]"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/967900.967985"},{"key":"e_1_2_1_17_1","doi-asserted-by":"crossref","unstructured":"Nipkow T. Paulson L. C. and Wenzel M. 2002. Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Springer. LNCS Tutorial 2283.]]  Nipkow T. Paulson L. C. and Wenzel M. 2002. Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Springer. LNCS Tutorial 2283.]]","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_2_1_18_1","first-page":"85","article-title":"The inductive approach to verifying cryptographic protocols","volume":"6","author":"Paulson L. C.","year":"1998","unstructured":"Paulson , L. C. 1998 . The inductive approach to verifying cryptographic protocols . J. Comp. Sec. 6 , 85 -- 128 .]] Paulson, L. C. 1998. The inductive approach to verifying cryptographic protocols. J. Comp. Sec. 6, 85--128.]]","journal-title":"J. Comp. Sec."},{"key":"e_1_2_1_19_1","unstructured":"Ryan P. Y. A. and Schneider S. A. 2000. The Modelling and Analysis of Security Protocols: the CSP Approach. Addison Wesley Reading MA.]]  Ryan P. Y. A. and Schneider S. A. 2000. The Modelling and Analysis of Security Protocols: the CSP Approach. Addison Wesley Reading MA.]]"},{"key":"e_1_2_1_20_1","volume-title":"11th Computer Security Foundations Workshop. IEEE Computer Society Press. 54--65","author":"Schneider S.","year":"1998","unstructured":"Schneider , S. 1998 . Formal analysis of a nonrepudiation protocol . In 11th Computer Security Foundations Workshop. IEEE Computer Society Press. 54--65 .]] Schneider, S. 1998. Formal analysis of a nonrepudiation protocol. In 11th Computer Security Foundations Workshop. IEEE Computer Society Press. 54--65.]]"},{"key":"e_1_2_1_21_1","unstructured":"VISA 2002. 3-D Secure Introduction. VISA. On the Internet at http:\/\/international.visa.com\/fb\/paytech\/secure\/pdfs\/3DS_70001-01_Intro%duction_v1.0.2.pdf.]]  VISA 2002. 3-D Secure Introduction. VISA. On the Internet at http:\/\/international.visa.com\/fb\/paytech\/secure\/pdfs\/3DS_70001-01_Intro%duction_v1.0.2.pdf.]]"},{"key":"e_1_2_1_22_1","volume-title":"Symposium on Security and Privacy. IEEE Computer Society.]]","author":"Zhou J.","unstructured":"Zhou , J. and Gollmann , D . 1996. A fair nonrepudiation protocol . In Symposium on Security and Privacy. IEEE Computer Society.]] Zhou, J. and Gollmann, D. 1996. A fair nonrepudiation protocol. In Symposium on Security and Privacy. IEEE Computer Society.]]"},{"key":"e_1_2_1_23_1","volume-title":"International Refinement Workshop and Formal Methods Pacific, J. Grundy, M. Schwenke, and T. Vickers, Eds. Springer-Verlag","author":"Zhou G.","unstructured":"Zhou , G. and Gollmann , D . 1998. Towards verification of nonrepudiation protocols . In International Refinement Workshop and Formal Methods Pacific, J. Grundy, M. Schwenke, and T. Vickers, Eds. Springer-Verlag , New York. 370--380.]] Zhou, G. and Gollmann, D. 1998. Towards verification of nonrepudiation protocols. In International Refinement Workshop and Formal Methods Pacific, J. Grundy, M. Schwenke, and T. Vickers, Eds. Springer-Verlag, New York. 370--380.]]"}],"container-title":["ACM Transactions on Information and System Security"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1151414.1151416","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,28]],"date-time":"2022-12-28T18:37:06Z","timestamp":1672252626000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1151414.1151416"}},"subtitle":["Formalized and verified"],"short-title":[],"issued":{"date-parts":[[2006,5]]},"references-count":22,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2006,5]]}},"alternative-id":["10.1145\/1151414.1151416"],"URL":"https:\/\/doi.org\/10.1145\/1151414.1151416","relation":{},"ISSN":["1094-9224","1557-7406"],"issn-type":[{"value":"1094-9224","type":"print"},{"value":"1557-7406","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,5]]},"assertion":[{"value":"2006-05-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}