{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,27]],"date-time":"2026-10-27T18:54:41Z","timestamp":1793127281744,"version":"4.5.0"},"reference-count":44,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[2005,2,1]],"date-time":"2005-02-01T00:00:00Z","timestamp":1107216000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IJIS"],"published-print":{"date-parts":[[2005,2]]},"DOI":"10.1007\/s10207-004-0047-7","type":"journal-article","created":{"date-parts":[[2005,1,24]],"date-time":"2005-01-24T13:26:31Z","timestamp":1106573191000},"page":"17-28","source":"Crossref","is-referenced-by-count":13,"title":["An overview of the verification of SET"],"prefix":"10.1007","volume":"4","author":[{"given":"Giampaolo","family":"Bella","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Fabio","family":"Massacci","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lawrence C.","family":"Paulson","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2005,2,1]]},"reference":[{"key":"47_CRAbadiBlanchetSAS03","doi-asserted-by":"crossref","unstructured":"Abadi M, Blanchet B (2003) Computer-assisted verification of a protocol for certified email. In: Cousot R (ed) Proc. 10th international symposium on static analysis (SAS\u201903), Lecture notes in computer science, vol 2694. Springer, Berlin Heidelberg New York, pp 316\u2013335","DOI":"10.1007\/3-540-44898-5_17"},{"key":"47_CRanderson-fail","doi-asserted-by":"crossref","first-page":"32","DOI":"10.1145\/188280.188291","volume":"37","author":"Anderson","year":"1994","unstructured":"Anderson R (1994) Why cryptosystems fail. Commun ACM 37(11):32\u201340","journal-title":"Commun ACM"},{"key":"47_CRAVISS","doi-asserted-by":"crossref","unstructured":"Armando A, Basin D, Bouallagui M, Chevalier Y, Compagna L, M\u00f6dersheim S, Rusinowitch M, Turuani M, Vigan\u00f2 L, Vigneron L (2002) The AVISS Security Protocol Analysis Tool. In: Proc. international conference on computer-aided verification (CAV-02). Lecture notes in computer science, vol 2404. Springer, Berlin Heidelberg New York","DOI":"10.1007\/3-540-45657-0_27"},{"key":"47_CRarm-comp-gant-03-FME","unstructured":"Armando A, Compagna L, Ganty P (2003) SAT-based model-checking of security protocols. In: Proc. 12th international FME symposium (FME03), Pisa, Italy, 8\u201314 September 2003"},{"key":"47_CRAsok-Schu-Waid-97","doi-asserted-by":"crossref","unstructured":"Asokan N, Schunter M, Waidner M (1997) Optimistic protocols for fair exchange. In: Proc. 4th ACM conference on computer and communication security (CCS-97). ACM Press\/Addison-Wesley, Reading, MA, pp 7\u201317","DOI":"10.1145\/266420.266426"},{"key":"47_CRgroup-protocols","doi-asserted-by":"crossref","unstructured":"Ateniese G, Steiner M, Tsudik G (1998) Authenticated group key agreement and friends. In: Proc. 5th ACM conference on computer and communication security. ACM Press, New York, pp 17\u201326","DOI":"10.1145\/288090.288097"},{"key":"47_CRbasi-99-CQRE","doi-asserted-by":"crossref","unstructured":"Basin D (1999) Lazy infinite-state analysis of security protocols. In: Baumgart R (ed) Secure networking \u2013 CQRE (Secure)\u201999, Lecture notes in computer science, vol 1740. Springer, Berlin Heidelberg New York, pp 30\u201342","DOI":"10.1007\/3-540-46701-7_3"},{"key":"47_CRbasi-denk-01-ENTCS","doi-asserted-by":"crossref","unstructured":"Basin D, Denker G (2001) Maude versus Haskell: an experimental comparison in security protocol analysis. In: Futatsugi K (ed) Electronic notes in theoretical computer science, vol 36. Elsevier (North-Holland), Amsterdam","DOI":"10.1016\/S1571-0661(05)80141-0"},{"key":"47_CRBella-03","doi-asserted-by":"crossref","first-page":"87","DOI":"10.3233\/JCS-2003-11103","volume":"11","author":"Bella","year":"2003","unstructured":"Bella G (2003) Inductive verification of smart card protocols. J Comput Secur 11(1):87\u2013132","journal-title":"J Comput Secur"},{"key":"47_CRset-specifications","unstructured":"Bella G, Massacci F, Paulson L, Tramontano P (2000) Making sense of specifications: the formalization of set (extended abstract). In: Christianson B, Crispo B, Malcolm JA, Roe M (eds) Proceedings of the 2000 workshop on security protocols. Lecture notes in computer science, vol 2133. Springer, Berlin Heidelberg New York, pp 74\u201381"},{"key":"47_CRset-purchase-ccs","doi-asserted-by":"crossref","unstructured":"Bella G, Massacci F, Paulson LC (2002) The verification of an industrial payment protocol: the SET purchase phase. In: Atluri V (ed) Proc. 9th ACM conference on computer and communications security. ACM Press, New York, pp 12\u201320","DOI":"10.1145\/586110.586113"},{"key":"47_CRset-registration","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1109\/JSAC.2002.806133","volume":"21","author":"Bella","year":"2003","unstructured":"Bella G, Massacci F, Paulson LC (2003) Verifying the SET registration protocols. IEEE J Select Areas Commun 21(1):77\u201387","journal-title":"IEEE J Select Areas Commun"},{"key":"47_CRset-esorics","doi-asserted-by":"crossref","unstructured":"Bella G, Massacci F, Paulson LC, Tramontano P (2000) Formal verification of cardholder registration in SET. In: Cuppens F, Deswarte Y, Gollman D, Waidner M (eds) Computer Security \u2013 ESORICS 2000. Lecture notes in computer science, vol 1895. Springer, Berlin Heidelberg New York, pp 159\u2013174","DOI":"10.1007\/10722599_10"},{"key":"47_CRBell-Paul-98","doi-asserted-by":"crossref","unstructured":"Bella G, Paulson LC (1998) Kerberos version IV: inductive analysis of the secrecy goals. In: Quisquater et al. [37], pp 361\u2013375","DOI":"10.1007\/BFb0055875"},{"key":"47_CRblanchet-verifier","unstructured":"Blanchet B (1998) An efficient cryptographic protocol verifier based on prolog rules. In: Proc. 14th IEEE workshop on computer security foundations. IEEE Press, New York"},{"key":"47_CRBrac-99","unstructured":"Brackin S (1999) Automatically detecting authentication limitations in commercial security protocols. In: Proc. 22nd national conference on information systems security, October 1999. http:\/\/www.arca.com\/proj_papers\/brackin\/Nissc99.pdf"},{"key":"47_CRBAN-89","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1098\/rspa.1989.0125","volume":"426","author":"Burrows","year":"1989","unstructured":"Burrows M, Abadi M, Needham RM (1989) A logic of authentication. Proc R Soc Lond 426:233\u2013271","journal-title":"Proc R Soc Lond"},{"key":"47_CRaiel-mass-01-TOCL","doi-asserted-by":"crossref","first-page":"542","DOI":"10.1145\/383779.383785","volume":"2","author":"Carlucci","year":"2001","unstructured":"Carlucci Aiello L, Massacci F (2001) Verifying security protocols as planning in logic programming. ACM Trans Comput Logic 2(4):542\u2013580","journal-title":"ACM Trans Comput Logic"},{"key":"47_CRchev-vign-02-CAV","doi-asserted-by":"crossref","unstructured":"Chevalier Y, Vigneron L (2002) Automated unbounded verification of security protocols. In: Proc. international conference on computer-aided verification (CAV-02). Lecture notes in computer science, vol 2404. Springer, Berlin Heidelberg New York","DOI":"10.1007\/3-540-45657-0_24"},{"key":"47_CRcohen-csfw","doi-asserted-by":"crossref","unstructured":"Cohen E (2000) TAPS: A first-order verifier for cryptographic protocols. In: Proc. 13th IEEE Computer Security Foundations Workshop. IEEE Press, New York, pp 144\u2013158","DOI":"10.1109\/CSFW.2000.856933"},{"key":"47_CRjacq-rusi-vign-00-LPAR","doi-asserted-by":"crossref","unstructured":"Jacquemard F, Rusinowitch M, Vigneron L (2000) Compiling and verifying security protocols. In: Parigot M, Voronkov A (eds) Proceedings of LPAR 2000. Lecture notes in computer science, vol 1955. Springer, Berlin Heidelberg New York, pp 131\u2013160","DOI":"10.1007\/3-540-44404-1_10"},{"key":"47_CRKess-Neum-98","doi-asserted-by":"crossref","unstructured":"Kessler V, Neumann H (1998) A sound logic for analysing electronic commerce protocols. In: Quisquater et al. [37]","DOI":"10.1007\/BFb0055874"},{"key":"47_CRLowe-96-b","unstructured":"Lowe G (1996) Breaking and fixing the Needham\u2013Schroeder public-key protocol using CSP and FDR. In: Margaria T, Steffen B (eds) Proc. 2nd international workshop on tools and algorithms for the construction and analysis of systems (TACAS \u201996). Lecture notes in computer science, vol 1055. Springer, Berlin Heidelberg New York, pp 147\u2013166"},{"key":"47_CRHui-Lowe-01","doi-asserted-by":"crossref","first-page":"3","DOI":"10.3233\/JCS-2001-91-202","volume":"9","author":"Lowe","year":"2001","unstructured":"Lowe G, Hui ML (2001) Fault-preserving simplifying transformations for security protocols. J Comput Secur 9:3\u201346","journal-title":"J Comput Secur"},{"key":"47_CRSET-external-97","unstructured":"Mastercard & VISA (1997) SET Secure Electronic Transaction: External Interface Guide, May 1997. http:\/\/www.setco.org\/set_specifications.html"},{"key":"47_CRSET-business-97","unstructured":"Mastercard & VISA (1997) SET Secure Electronic Transaction Specification: Business Description, May 1997. http:\/\/www.setco.org\/set_specifications.html"},{"key":"47_CRSET-protocol-97","unstructured":"Mastercard & VISA (1997) SET Secure Electronic Transaction Specification: Formal Protocol Definition, May 1997. http:\/\/www.setco.org\/set_specifications.html"},{"key":"47_CRSET-programmer-97","unstructured":"Mastercard & VISA (1997) SET Secure Electronic Transaction Specification: Programmer\u2019s Guide, May 1997. http:\/\/www.setco.org\/set_specifications.html"},{"key":"47_CRmeadows-ike","doi-asserted-by":"crossref","unstructured":"Meadows C (1999) Analysis of the Internet Key Exchange protocol using the NRL Protocol Analyzer. In: Proc. SSP-99. IEEE Press, New York, pp 216\u2013231","DOI":"10.1109\/SECPRI.1999.766916"},{"key":"47_CRmeadows-trends","doi-asserted-by":"crossref","first-page":"44","DOI":"10.1109\/JSAC.2002.806125","volume":"21","author":"Meadows","year":"2003","unstructured":"Meadows C (2003) Formal methods for cryptographic protocol analysis: emerging issues and trends. IEEE J Select Areas Commun 21(1):44\u201354","journal-title":"IEEE J Select Areas Commun"},{"key":"47_CRMead-Syve-98","doi-asserted-by":"crossref","unstructured":"Meadows C, Syverson P (1998) A formal specification of requirements for payment transactions in the SET protocol. In: Hirschfeld R (ed) Proc. Financial Cryptography \u201998, Lecture notes in computer science, vol 1465. Springer, Berlin Heidelberg New York","DOI":"10.1007\/BFb0055477"},{"key":"47_CRisa-tutorial","doi-asserted-by":"crossref","unstructured":"Nipkow T, Paulson LC, Wenzel M (2002) Isabelle\/HOL: A proof assistant for higher-order logic. Lecture notes in computer science tutorial, vol 2283. Springer, Berlin Heidelberg New York","DOI":"10.1007\/3-540-45949-9"},{"key":"47_CRPaul-98-b","doi-asserted-by":"crossref","first-page":"85","DOI":"10.3233\/JCS-1998-61-205","volume":"6","author":"Paulson","year":"1998","unstructured":"Paulson LC (1998) The inductive approach to verifying cryptographic protocols. J Comput Secur 6:85\u2013128","journal-title":"J Comput Secur"},{"key":"47_CRPaul-99","doi-asserted-by":"crossref","first-page":"332","DOI":"10.1145\/322510.322530","volume":"2","author":"Paulson","year":"1999","unstructured":"Paulson LC (1999) Inductive analysis of the internet protocol TLS. ACM Trans Inf Syst Secur 2(3):332\u2013351","journal-title":"ACM Trans Inf Syst Secur"},{"key":"47_CRpaulson-yahalom","doi-asserted-by":"crossref","first-page":"197","DOI":"10.3233\/JCS-2001-9302","volume":"9","author":"Paulson","year":"2001","unstructured":"Paulson LC (2001) Relations between secrets: two formal analyses of the Yahalom protocol. J Comput Secur 9(3):197\u2013216","journal-title":"J Comput Secur"},{"key":"47_CRpere-quis-01-SEC","doi-asserted-by":"crossref","unstructured":"Pereira O, Quisquater J-J (2001) Security analysis of the cliques protocols suites: first results. In: Dupuy M, Paradinas P (eds) Proc. IFIP TC11 16th annual working conference on information security (IFIP\/Sec\u201901), vol 193. Kluwer, Dordrecht","DOI":"10.1109\/CSFW.2001.930137"},{"key":"47_CResorics98","doi-asserted-by":"crossref","unstructured":"Quisquater J-J, Deswarte Y, Meadows C, Gollmann D (eds) (1998) Computer Security \u2013 ESORICS 98. Lecture notes in computer science, vol 1485. Springer, Berlin Heidelberg New York","DOI":"10.1007\/BFb0055851"},{"key":"47_CRFoca-Gorr-97","doi-asserted-by":"crossref","first-page":"550","DOI":"10.1109\/32.629493","volume":"23","author":"Focardi","year":"1997","unstructured":"Focardi R, Gorrieri R (1997) The compositional security checker: a tool for the verification of information flow security properties. IEEE Trans Softw Eng 23(9):550\u2013571","journal-title":"IEEE Trans Softw Eng"},{"key":"47_CRRyan-Schn-98","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1016\/S0020-0190(97)00180-4","volume":"65","author":"Ryan","year":"1998","unstructured":"Ryan P, Schneider S (1998) An attack on a recurive authentication protocol. A cautionary tale. Inf Process Lett 65(15):7\u201316","journal-title":"Inf Process Lett"},{"key":"47_CRRS-00","first-page":"the","volume":"protocols","author":"Ryan","year":"2000","unstructured":"Ryan PYA, Schneider SA (2000) The modelling and analysis of security protocols: the CSP approach. Addison-Wesley, Reading, MA","journal-title":"The modelling and analysis of security"},{"key":"47_CRSchn-98","doi-asserted-by":"crossref","first-page":"741","DOI":"10.1109\/32.713329","volume":"24","author":"Schneider","year":"1998","unstructured":"Schneider S (1998) Verifying authentication protocols in CSP. IEEE Trans Softw Eng 24(9):741\u2013758","journal-title":"IEEE Trans Softw Eng"},{"key":"47_CRshmati-fair","unstructured":"Shmatikov V, Mitchell JC (2000) Analysis of a fair exchange protocol. In: Proc. symposium on network and distributed system security (NDSS-00)"},{"key":"47_CRSong-99","doi-asserted-by":"crossref","unstructured":"Song D (1999) Athena: an automatic checker for security protocol analysis. In: Proc. 12th IEEE Computer Security Foundations Workshop. IEEE Press, New York","DOI":"10.1109\/CSFW.1999.779773"},{"key":"47_CRStol-01","doi-asserted-by":"crossref","unstructured":"Stoller SD (2001) 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":["International Journal of Information Security"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10207-004-0047-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10207-004-0047-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10207-004-0047-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,5]],"date-time":"2020-04-05T12:08:57Z","timestamp":1586088537000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10207-004-0047-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,2]]},"references-count":44,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2005,2]]}},"alternative-id":["47"],"URL":"https:\/\/doi.org\/10.1007\/s10207-004-0047-7","relation":{},"ISSN":["1615-5262","1615-5270"],"issn-type":[{"value":"1615-5262","type":"print"},{"value":"1615-5270","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,2]]}}}