{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,15]],"date-time":"2026-01-15T23:56:44Z","timestamp":1768521404466,"version":"3.49.0"},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[2006,2,25]],"date-time":"2006-02-25T00:00:00Z","timestamp":1140825600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2006,10,17]]},"DOI":"10.1007\/s10817-005-9018-6","type":"journal-article","created":{"date-parts":[[2006,2,24]],"date-time":"2006-02-24T13:04:13Z","timestamp":1140786253000},"page":"5-37","source":"Crossref","is-referenced-by-count":35,"title":["Verifying the SET Purchase Protocols"],"prefix":"10.1007","volume":"36","author":[{"given":"Giampaolo","family":"Bella","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fabio","family":"Massacci","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lawrence C.","family":"Paulson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,2,25]]},"reference":[{"key":"9018_CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M. and Gordon, A.: A calculus for cryptographic protocols: The spi calculus, in Proc. 4th ACM Conf. on Comm. and Comp. Sec. (CCS-97), ACM and Addison Wesley, 1997.","DOI":"10.1145\/266420.266432"},{"issue":"1","key":"9018_CR2","doi-asserted-by":"crossref","first-page":"6","DOI":"10.1109\/32.481513","volume":"22","author":"M. Abadi","year":"1996","unstructured":"Abadi, M. and Needham, R. M.: Prudent engineering practice for cryptographic protocols, IEEE Trans. Softw. Eng. 22(1) (January 1996), 6\u201315.","journal-title":"IEEE Trans. Softw. Eng."},{"key":"9018_CR3","doi-asserted-by":"crossref","unstructured":"Basin, D., M\u00f6dersheim, S. and Vigan\u00f2, L.: An on-the-fly model-checker for security protocol analysis, in E. Snekkenes and D. Gollmann (eds.), Proc. 8th Eur. Symp. on Res. in Comp. Sec., Volume 2000 of Lecture Notes in Comp. Sci., Springer, 2003, pp. 253\u2013270.","DOI":"10.1007\/978-3-540-39650-5_15"},{"issue":"1","key":"9018_CR4","doi-asserted-by":"crossref","first-page":"87","DOI":"10.3233\/JCS-2003-11103","volume":"11","author":"G. Bella","year":"2003","unstructured":"Bella, G.: Inductive verification of smart card protocols, J. Comput. Secur. 11(1) (2003), 87\u2013132.","journal-title":"J. Comput. Secur."},{"key":"9018_CR5","doi-asserted-by":"crossref","unstructured":"Bella, G., Massacci, F. and Paulson, L. C.: The verification of an industrial payment protocol: The SET purchase phase, in V. Atluri (ed.), 9th ACM Conf. on Comp. and Comm. Sec., ACM, 2002, pp. 12\u201320.","DOI":"10.1145\/586110.586113"},{"issue":"1","key":"9018_CR6","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1109\/JSAC.2002.806133","volume":"21","author":"G. Bella","year":"2003","unstructured":"Bella, G., Massacci, F. and Paulson, L. C.: Verifying the SET registration protocols, IEEE J. Sel. Areas Commun. 21(1) (2003), 77\u201387.","journal-title":"IEEE J. of Selected Areas in Communications"},{"issue":"1\u20132","key":"9018_CR7","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1007\/s10207-004-0047-7","volume":"4","author":"G. Bella","year":"2005","unstructured":"Bella, G., Massacci, F. and Paulson, L. C.: An overview of the verification of SET, Int. J. Inf. Secur. 4(1\u20132)(2005),17\u201328.","journal-title":"Int. J. Inf. Secur."},{"key":"9018_CR8","doi-asserted-by":"crossref","unstructured":"Bella, G., Massacci, F., Paulson, L. C. and Tramontano, P.: Formal verification of cardholder registration in SET, in F. Cuppens, Y. Deswarte, D. Gollman and M. Waidner (eds.), Computer Security \u2013 ESORICS 2000, volume 1895 of Lecture Notes in Comp. Sci., Springer, 2000, pp. 159\u2013174.","DOI":"10.1007\/10722599_10"},{"key":"9018_CR9","doi-asserted-by":"crossref","unstructured":"Bella, G. and Paulson, L. C.: Kerberos version IV: Inductive analysis of the secrecy goals, in Quisquater et al. [32], pp. 361\u2013375.","DOI":"10.1007\/BFb0055875"},{"key":"9018_CR10","doi-asserted-by":"crossref","unstructured":"Bozzano M. and Delzanno G.: Automated protocol verification in linear logic, in Proc. 4th ACM Conf. on Principles and Practice of Declarative Programming (ACM PPDP'02), ACM and Addison, Wesley 2002, pp. 38\u201349.","DOI":"10.1145\/571157.571162"},{"issue":"4","key":"9018_CR11","doi-asserted-by":"crossref","first-page":"677","DOI":"10.3233\/JCS-2003-11407","volume":"11","author":"N. Durgin","year":"2004","unstructured":"Durgin, N., Mitchell, J. and Pavlovic, D.: A compositional logic for proving security properties of protocols, J. Comput. Secur. 11(4) (2004), 677\u2013721.","journal-title":"J. Comput. Secur."},{"key":"9018_CR12","doi-asserted-by":"crossref","first-page":"191","DOI":"10.3233\/JCS-1999-72-304","volume":"7","author":"F. J. T. F\u00e1brega","year":"1999","unstructured":"F\u00e1brega, F. J. T., Herzog, J. C. and Guttman, J. D.: Strand spaces: Proving security protocols correct, J. Comp. Secur. 7 (1999), 191\u2013220.","journal-title":"J. Comput. Secur."},{"key":"9018_CR13","doi-asserted-by":"crossref","unstructured":"Gollmann, D.: What do we mean by entity authentication? in Proc. 15th IEEE Symp. on Security and Privacy, IEEE Comp. Society Press, 1996, pp. 46\u201354.","DOI":"10.1109\/SECPRI.1996.502668"},{"key":"9018_CR14","unstructured":"Gong, L. and Syverson, P.: Fail-stop protocols: An approach to designing secure protocols, in Proc. 5th IFIP Working Conference on Dependable Computing for Critical Applications (DCCA-5), September 1995."},{"key":"9018_CR15","doi-asserted-by":"crossref","unstructured":"Guttman, J.: Security goals: Packet trajectories and strand spaces, in R. Focardi and F. Gorrieri (eds.), Foundations of Security Analysis and Design \u2013 Tutorial Lectures, volume 2171 of Lecture Notes in Comp. Sci., Springer, 2001, pp. 197\u2013261.","DOI":"10.1007\/3-540-45608-2_4"},{"key":"9018_CR16","unstructured":"Kessler, V. and Neumann, H.: A sound logic for analysing electronic commerce protocols, in Quisquater et al. [32]."},{"key":"9018_CR17","doi-asserted-by":"crossref","unstructured":"Lowe, G.: A hierarchy of authentication specifications, in Proc. 10th IEEE Comp. Sec. Found. Workshop, IEEE Comp. Society Press, 1997, pp. 31\u201343.","DOI":"10.1109\/CSFW.1997.596782"},{"key":"9018_CR18","doi-asserted-by":"crossref","first-page":"3","DOI":"10.3233\/JCS-2001-91-202","volume":"9","author":"G. Lowe","year":"2001","unstructured":"Lowe, G. and Hui, M. L.: Fault-preserving simplifying transformations for security protocols, J. Comput. Secur. 9 (2001), 3\u201346.","journal-title":"J. Comput. Secur."},{"key":"9018_CR19","unstructured":"Mastercard & VISA: SET Secure Electronic Transaction: External Interface Guide, May 1997. On the Internet at http:\/\/www.setco.org\/set\\_specifications.html ."},{"key":"9018_CR20","unstructured":"Mastercard & VISA: SET Secure Electronic Transaction Specification: Business Description, May 1997. On the Internet at http:\/\/www.setco.org\/set\\_specifications.html ."},{"key":"9018_CR21","unstructured":"Mastercard & VISA: SET Secure Electronic Transaction Specification: Formal Protocol Definition, May 1997. On the Internet at http:\/\/www.setco.org\/set\\_specifications.html ."},{"key":"9018_CR22","unstructured":"Mastercard & VISA: SET Secure Electronic Transaction Specification: Programmer's Guide, May 1997. On the Internet at http:\/\/www.setco.org\/set\\_specifications.html ."},{"key":"9018_CR23","doi-asserted-by":"crossref","unstructured":"Meadows, C.: Analysis of the Internet Key Exchange protocol using the NRL Protocol Analyzer, in SSP-99, IEEE Comp. Society Press, 1999, pp. 216\u2013231.","DOI":"10.21236\/ADA465466"},{"issue":"1","key":"9018_CR24","doi-asserted-by":"crossref","first-page":"44","DOI":"10.1109\/JSAC.2002.806125","volume":"21","author":"C. Meadows","year":"2003","unstructured":"Meadows, C.: Formal methods for cryptographic protocol analysis: Emerging issues and trends, IEEE J. Sel. Areas Commun. 21(1) (2003), 44\u201354.","journal-title":"IEEE J. Sel. Areas Commun."},{"key":"9018_CR25","doi-asserted-by":"crossref","unstructured":"Meadows, C. and Syverson, P.: A formal specification of requirements for payment transactions in the SET protocol, in R. Hirschfeld, (ed.), Proc. Financial Cryptography 98, volume 1465 of Lecture Notes in Comp. Sci. Springer, 1998.","DOI":"10.1007\/BFb0055477"},{"key":"9018_CR26","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L. C. and Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Springer, 2002. LNCS Tutorial 2283.","DOI":"10.1007\/3-540-45949-9"},{"key":"9018_CR27","unstructured":"Paller, A.: Alert: Large criminal hacker attack on Windows NTE-banking and E-commerce sites. On the Internet at http:\/\/www.sans.org\/newlook\/alerts\/NTE-bank.htm , Mar. 2001. SANS Institute."},{"key":"9018_CR28","unstructured":"Paulson, L. C.: Generic automatic proof tools, in R. Veroff (ed.), Automated Reasoning and its Applications: Essays in Honor of Larry Wos, chapter 3. MIT Press, 1997."},{"key":"9018_CR29","doi-asserted-by":"crossref","first-page":"85","DOI":"10.3233\/JCS-1998-61-205","volume":"6","author":"L. C. Paulson","year":"1998","unstructured":"Paulson, L. C.: The inductive approach to verifying cryptographic protocols, J. Comput. Secur. 6 (1998), 85\u2013128.","journal-title":"J. Comput. Secur."},{"issue":"3","key":"9018_CR30","first-page":"73","volume":"5","author":"L. C. Paulson","year":"1999","unstructured":"Paulson, L. C.: A generic tableau prover and its integration with Isabelle, J. Univers. Comput. Sci. 5(3) (1999), 73\u201387.","journal-title":"J. Univers. Comput. Sci."},{"issue":"3","key":"9018_CR31","doi-asserted-by":"crossref","first-page":"332","DOI":"10.1145\/322510.322530","volume":"2","author":"L. C. Paulson","year":"1999","unstructured":"Paulson, L. C.: Inductive analysis of the internet protocol TLS, ACM Trans. Inf. Syst. Secur. 2(3) (1999), 332\u2013351.","journal-title":"ACM Trans. Inf. Syst. Secur."},{"key":"9018_CR32","doi-asserted-by":"crossref","unstructured":"Quisquater, J.-J., Deswarte, Y., Meadows, C. and Gollmann, D. (eds.), Computer Security \u2013 ESORICS 98, volume 1485 of Lecture Notes in Comp. Sci. Springer, 1998.","DOI":"10.1007\/BFb0055851"},{"key":"9018_CR33","unstructured":"RSA Laboratories. PKCS-7: Cryptographic Message Syntax Standard, 1993. On the Internet at http:\/\/www.rsasecurity.com\/rsalabs\/pkcs ."},{"key":"9018_CR34","doi-asserted-by":"crossref","unstructured":"Stoller, S. D.: A bound on attacks on payment protocols, in Proc. 16th Annual IEEE Symposium on Logic in Computer Science (LICS), June 2001.","DOI":"10.1109\/LICS.2001.932483"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-005-9018-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-005-9018-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-005-9018-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T21:34:40Z","timestamp":1736285680000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-005-9018-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,2,25]]},"references-count":34,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2006,10,17]]}},"alternative-id":["9018"],"URL":"https:\/\/doi.org\/10.1007\/s10817-005-9018-6","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,2,25]]}}}