{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,12]],"date-time":"2025-08-12T21:43:20Z","timestamp":1755035000740},"reference-count":31,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2013,7,1]],"date-time":"2013-07-01T00:00:00Z","timestamp":1372636800000},"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":[[2013,7]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>In this paper, we develop an inductive approach to strand spaces, by introducing an inductive definition for bundles. This definition provides us not only a constructive illustration for bundles, but also an effective and rigorous technique of rule induction to reason about properties of bundles. With this induction principle, we can prove that our bundle model is sound in the sense that a bundle is a causally well-founded graph. This approach also gives an alternative to rigorously prove a generalized version of authentication tests. To illustrate the applicability of our approach, we have performed case studies on verification of secrecy and authentication properties of the Needham\u2013Schroeder\u2013Lowe and Otway\u2013Rees protocols. Our approach has been mechanized using Isabelle\/HOL.<\/jats:p>","DOI":"10.1007\/s00165-011-0187-2","type":"journal-article","created":{"date-parts":[[2011,7,14]],"date-time":"2011-07-14T19:28:49Z","timestamp":1310671729000},"page":"465-501","source":"Crossref","is-referenced-by-count":7,"title":["An inductive approach to strand spaces"],"prefix":"10.1145","volume":"25","author":[{"given":"Yongjian","family":"Li","sequence":"first","affiliation":[{"name":"The State Key Laboratory of Computer Science &amp; The State Key Laboratory of Information Security, Institute of Software, Chinese Academy of Sciences, P.O. Box 8717, Beijing, China"}]},{"given":"Jun","family":"Pang","sequence":"additional","affiliation":[{"name":"Facult\u00e9 des Sciences de la Technologie et de la Communication, Computer Science and Communications, Universit\u00e9 du Luxembourg, Luxembourg, Belgium"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1145\/77648.77649"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"},{"key":"e_1_2_1_2_3_2","unstructured":"Furqan Z Muhammad S Guha RK (2006) Formal verification of 802.11i using strand space formalism. In: Proceedings conference on networking and conference on mobile communications and learning technologies. IEEE Computer Society p 140"},{"key":"e_1_2_1_2_4_2","unstructured":"Guttman JD Javier Thayer F (2001) Authentication tests. In: Proceedings of 12th IEEE symposium on security and privacy. IEEE Computer Society pp 96\u2013109"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00139-6"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Guttman JD (2002) Security protocol design via authentication tests. In: Proceedings of 15th IEEE computer security foundations workshop. IEEE Computer Society pp 92\u2013103","DOI":"10.1109\/CSFW.2002.1021809"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.5555\/1662641.1662645"},{"key":"e_1_2_1_2_8_2","unstructured":"Javier Thayer F Herzog F Guttman JD (1998) Strand spaces: why is a security protocol correct? In: Proceedings of 19th IEEE symposium on security and privacy. IEEE Computer Society pp 96\u2013109"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-1999-72-304"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Kamil A Lowe G (2010) Specifying and modelling secure channels in strand spaces. In: Proceedings of 6th workshop on formal aspects in security and trust. Lecture notes in computer science vol 5983. Springer Berlin pp 233\u2013247","DOI":"10.1007\/978-3-642-12459-4_17"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Li Y (2005) The inductive approach to strand space. In: Proceedings of 25th IFIP conference on formal techniques for networked and distributed systems. Lecture notes in computer science vol 3731. Springer Berlin pp 547\u2013552","DOI":"10.1007\/11562436_43"},{"key":"e_1_2_1_2_12_2","unstructured":"Li Y (2008) Strand spaces and security protocols. http:\/\/lcs.ios.ac.cn\/~lyj238\/strand.html."},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Lowe G (1996) Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: Proceedings of 2nd conference on tools and algorithms for the construction and analysis of systems. 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_14_2","doi-asserted-by":"crossref","unstructured":"Lowe G (1996) Some new attacks upon security protocols. In: Proceedings of 9th IEEE computer security foundations workshop. IEEE Computer Society pp 162\u2013169","DOI":"10.1109\/CSFW.1996.503701"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Li Y Pang J (2006) Generalized unsolicited tests for authentication protocol analysis. In: Proceedings of 7th conference on parallel and distributed computing applications and technologies. IEEE Computer Society pp 509\u2013514","DOI":"10.1109\/PDCAT.2006.65"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Li Y Pang J (2007) Extending the strand space method to verify Kerberos v. In: Proceedings of 8th conference on parallel and distributed computing applications and technologies. IEEE Computer Society pp 437\u2013444","DOI":"10.1109\/PDCAT.2007.22"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Meadows C (1999) Analysis of the internet key exchange protocol using the NRL protocol analyzer. In: Proceedings of 12th IEEE computer security foundations workshop. IEEE Computer Society pp 216\u2013231","DOI":"10.21236\/ADA465466"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Millen JK (1995) The interrogator model. In: Proceedings of 16th IEEE symposium on security and privacy. IEEE Computer Society pp 251\u2013260","DOI":"10.1109\/SECPRI.1995.398937"},{"key":"e_1_2_1_2_19_2","unstructured":"Mitchell JC Mitchell JC Stern U (1997) Automated analysis of cryptographic protocols using Murphi. In: Proceedings of 18th symposium on security and privacy. IEEE Computer Society pp 141\u2013153"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Nipkow T Paulson LC Wenzel M (2002) Isabelle\/HOL\u2014a proof assistant for higher-order logic. LNCS vol 2283. Springer Berlin","DOI":"10.1007\/3-540-45949-9"},{"issue":"2","key":"e_1_2_1_2_21_2","first-page":"10","article-title":"Efficient and timely mutual authentication","volume":"27","author":"Otway D","year":"1987","journal-title":"Oper Syst Rev"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Owre S Rushby JM Shankar N (1992) PVS: a prototype verification system. In: Proceedings of 11th conference on automated deduction. Lecture notes in artificial intelligence vol 607. Springer Berlin pp 748\u2013752","DOI":"10.1007\/3-540-55602-8_217"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Paulson LC (1996) ML for the working programmer. University of Cambridge Press","DOI":"10.1017\/CBO9780511811326"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Paulson LC (1997) Proving properties of security protocols by induction. In: Proceedings of 10th IEEE computer security foundations workshop. IEEE Computer Society pp 70\u201383","DOI":"10.1109\/CSFW.1997.596788"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.5555\/353677.353681"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Perrig A Song DX (2000) Looking for diamonds in the desert: extending automatic protocol generation to three-party authentication and key agreement protocols. In: Proceedings of 13th IEEE computer security foundations workshop. IEEE Computer Society pp 64\u201376","DOI":"10.1109\/CSFW.2000.856926"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Schneider S (1997) Verifying authentication protocols with CSP. In: Proceedings of 10th IEEE computer security foundations workshop. IEEE Computer Society pp 3\u201317","DOI":"10.1109\/CSFW.1997.596775"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Sharp R Hansen MR (2007) Timed traces and strand spaces. In: Proceedings of 2nd symposium on computer science in Russia. Lecture notes in computer science vol 4649. Springer Berlin pp 373\u2013386","DOI":"10.1007\/978-3-540-74510-5_38"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Song DX (1999) Athena: a new efficient automated checker for security protocol analysis. In: Proceedings of 12th IEEE computer security foundations workshop. IEEE Computer Society pp 192\u2013202","DOI":"10.1109\/CSFW.1999.779773"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Wenzel M (1999) Isar\u2014a generic interpretative approach to readable formal proof documents. In: Proceedings of 12th conference on theorem proving in higher order logics. Lecture notes in computer science vol 1690. Springer Berlin pp 167\u2013184","DOI":"10.1007\/3-540-48256-3_12"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Wang H Zhang Y Li Y (2005) Modeling for security verification of a cryptographic protocol with MAC payload. In: Proceedings of international conference on intelligent computing. Lecture notes in computer science vol 3645. Springer Berlin pp 538\u2013547","DOI":"10.1007\/11538356_56"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-011-0187-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-011-0187-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-011-0187-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:55:44Z","timestamp":1641484544000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-011-0187-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,7]]},"references-count":31,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2013,7]]}},"alternative-id":["10.1007\/s00165-011-0187-2"],"URL":"https:\/\/doi.org\/10.1007\/s00165-011-0187-2","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,7]]}}}