{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,23]],"date-time":"2025-05-23T04:37:43Z","timestamp":1747975063180,"version":"3.41.0"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319174037"},{"type":"electronic","value":"9783319174044"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-17404-4_8","type":"book-chapter","created":{"date-parts":[[2015,4,16]],"date-time":"2015-04-16T08:45:59Z","timestamp":1429173959000},"page":"111-126","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Automatic Verification for Later-Correspondence of Security Protocols"],"prefix":"10.1007","author":[{"given":"Xiaofei","family":"Xie","sequence":"first","affiliation":[]},{"given":"Xiaohong","family":"Li","sequence":"additional","affiliation":[]},{"given":"Yang","family":"Liu","sequence":"additional","affiliation":[]},{"given":"Li","family":"Li","sequence":"additional","affiliation":[]},{"given":"Ruitao","family":"Feng","sequence":"additional","affiliation":[]},{"given":"Zhiyong","family":"Feng","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,4,17]]},"reference":[{"key":"8_CR1","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1098\/rspa.1989.0125","volume":"426","author":"M Burrows","year":"1989","unstructured":"Burrows, M., Abadi, M., Needham, R.: A logic of authentication. Proc. R. Soc. Lond. A 426, 233\u2013271 (1989)","journal-title":"Proc. R. Soc. Lond. A"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Lowe, G.: Breaking and fixing the needham-schroeder public-key protocol using FDR. In: Proceedings of the Second International Workshop on Tools and Algorithms for Construction and Analysis of Systems, pp. 147\u2013166 (1989)","DOI":"10.1007\/3-540-61042-1_43"},{"key":"8_CR3","first-page":"496","volume":"6","author":"XF Xie","year":"2012","unstructured":"Xie, X.F., Li, X.H., Cao, K.Y., Feng, Z.Y.: Security modeling based on CSP for network protocol. Int. J. Digit. Content Technol. Appl. 6, 496\u2013504 (2012)","journal-title":"Int. J. Digit. Content Technol. Appl."},{"key":"8_CR4","unstructured":"Thayer, F.J., Herzog, J.C., Guttman, J.D.: Strand spaces: why is a security protocol correct? In: Proceedings of the 1998 IEEE Symposium on Security and Privacy, pp. 160\u2013171 (1998)"},{"key":"8_CR5","doi-asserted-by":"crossref","first-page":"191","DOI":"10.3233\/JCS-1999-72-304","volume":"7","author":"FJ Thayer","year":"1999","unstructured":"Thayer, F.J., Herzog, J.C., Guttman, J.D.: Strand spaces: proving security protocols correct. J. Comput. Secur. 7, 191\u2013230 (1999)","journal-title":"J. Comput. Secur."},{"key":"8_CR6","unstructured":"Bella, G., Paulson, L.C.: Using Isabelle to prove properties of the Kerberos authentication system. In: DIMACS Workshop on Design and Formal Verification of Security Protocols (1997)"},{"key":"8_CR7","unstructured":"Athena, D.X.S.: A New efficient automatic checker for security protocol analysis.In: Computer Security Foundations Workshop, pp. 192\u2013202 (1999)"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In:Computer Security Foundations Workshop, pp. 82\u201396 (2001)","DOI":"10.1109\/CSFW.2001.930138"},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/11513988_27","volume-title":"Computer Aided Verification","author":"A Armando","year":"2005","unstructured":"Armando, A., Basin, D., Boichut, Y., Chevalier, Y., Compagna, L., Cuellar, J., Drielsma, P.H., He\u00e1m, P.C., Kouchnarenko, O., Mantovani, J., M\u00f6dersheim, S., von Oheimb, D., Rusinowitch, M., Santiago, J., Turuani, M., Vigan\u00f2, L., Vigneron, L.: The AVISPA tool for the automated validation of internet security protocols and applications. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 281\u2013285. Springer, Heidelberg (2005)"},{"key":"8_CR10","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/0743-1066(95)00095-X","volume":"26","author":"C Meadows","year":"1996","unstructured":"Meadows, C.: The NRL protocol analyzer: an overview. J. Logic Program. 26, 113\u2013131 (1996)","journal-title":"J. Logic Program."},{"key":"8_CR11","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-540-88479-8_22","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation","author":"J Sun","year":"2008","unstructured":"Sun, J., Liu, Y., Dong, J.S.: Model checking CSP revisited: introducing a process analysis toolkit. In: Margaria, T., Steffen, B. (eds.) ISoLA 2008. CCIS, vol. 17, pp. 307\u2013322. Springer, Heidelberg (2008)"},{"key":"8_CR12","unstructured":"Mitchell, J.C., Mitchell, M., Stern, U.: Automated analysis of cryptographic protocols using Murphi. In: Proceedings of IEEE Symposium on Security and Privacy, pp. 141\u2013151. IEEE Computer Society Press (1997)"},{"key":"8_CR13","series-title":"International Series in Computer Science","volume-title":"Communicating Sequential Processes","author":"C Hoare","year":"1985","unstructured":"Hoare, C.: Communicating Sequential Processes. International Series in Computer Science. Prentice-Hall, Upper Saddle River (1985)"},{"key":"8_CR14","doi-asserted-by":"crossref","first-page":"451","DOI":"10.3233\/JCS-2003-11402","volume":"11","author":"A Gordon","year":"2003","unstructured":"Gordon, A., Jeffrey, A.: Authenticity by typing for security protocols. J. Comput. Secur. 11, 451\u2013519 (2003)","journal-title":"J. Comput. Secur."},{"key":"8_CR15","doi-asserted-by":"crossref","first-page":"435","DOI":"10.3233\/JCS-2004-123-406","volume":"12","author":"A Gordon","year":"2004","unstructured":"Gordon, A., Jeffrey, A.: Types and effects for asymmetric cryptographic protocols. J. Comput. Secur. 12, 435\u2013484 (2004)","journal-title":"J. Comput. Secur."},{"key":"8_CR16","unstructured":"Gordon, A.D., H\u00fcttel, H., Hansen, R.R.: Type inference for correspondence types. In: 6th International Workshop on Security Issues in Concurrency (2008)"},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"Bugliesi, M., Focardi, R., Maffei, M.: Analysis of typed analyses of authentication protocols. In: Proceedings 18th IEEE Computer Security Foundations Workshop, pp. 112\u2013125 (2005)","DOI":"10.1109\/CSFW.2005.8"},{"key":"8_CR18","doi-asserted-by":"crossref","first-page":"563","DOI":"10.3233\/JCS-2007-15602","volume":"15","author":"M Bugliesi","year":"2007","unstructured":"Bugliesi, M., Focardi, R., Maffei, M.: Dynamic types for authentication. J. Comput. Secur. 15, 563\u2013617 (2007)","journal-title":"J. Comput. Secur."},{"key":"8_CR19","unstructured":"Cremers, C., Mauw, S., de Vink, E.: Defining authentication in a trace model. In: Proceedings of the First International Workshop on Formal Aspects in Security and Trust, pp. 131\u2013145 (2003)"},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"Corin, R., Saptawijaya, A., Etalle, S.: A logic for constraint based security protocol analysis. In: Proceedings of IEEE Symposium on Security and Privacy, pp. 155\u2013168 (2006)","DOI":"10.1109\/SP.2006.3"},{"key":"8_CR21","doi-asserted-by":"crossref","unstructured":"Schmidt, B., Meier, S., Cremers, C., Basin, D.: Automated analysis of Difie-Hellman protocols and advanced security properties. In: Computer Security Foundations Symposium (CSF), pp. 78\u201394 (2012)","DOI":"10.1109\/CSF.2012.25"},{"key":"8_CR22","first-page":"57","volume":"6","author":"LA Tuan","year":"2012","unstructured":"Tuan, L.A., Sun, J., Liu, Y., Dong, J.S., Li, X.H., Tho, Q.T.: SEVE: automatic tool for verification of security protocols. Front. Comput. Sci. Spec. Issue Form. Eng. Method 6, 57\u201375 (2012)","journal-title":"Front. Comput. Sci. Spec. Issue Form. Eng. Method"},{"key":"8_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1007\/978-3-642-15643-4_30","volume-title":"Automated Technology for Verification and Analysis","author":"Y Liu","year":"2010","unstructured":"Liu, Y., Sun, J., Dong, J.S.: Developing model checkers using PAT. In: Bouajjani, A., Chin, W.-N. (eds.) ATVA 2010. LNCS, vol. 6252, pp. 371\u2013377. Springer, Heidelberg (2010)"},{"key":"8_CR24","doi-asserted-by":"crossref","first-page":"363","DOI":"10.3233\/JCS-2009-0339","volume":"17","author":"B Blanchet","year":"2009","unstructured":"Blanchet, B.: Automatic verification of correspondences for security protocols. J. Comput. Secur. 17, 363\u2013434 (2009)","journal-title":"J. Comput. Secur."},{"key":"8_CR25","doi-asserted-by":"crossref","unstructured":"Woo, T.Y.C., Lam, S.S.: A semantic model for authentication protocols. In: IEEE Symposium on Security and Privacy, pp. 178\u2013194 (1993)","DOI":"10.1109\/RISP.1993.287633"},{"key":"8_CR26","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"2","author":"D Dolev","year":"1983","unstructured":"Dolev, D., Yao, A.C.: On the security of public-key protocols. IEEE Trans. Inf. Theory 2, 198\u2013208 (1983)","journal-title":"IEEE Trans. Inf. Theory"},{"key":"8_CR27","volume-title":"Formal Models and Techniques for Analyzing Security Protocols","author":"MD Ryan","year":"2011","unstructured":"Ryan, M.D., Smyth, B.: Applied pi calculus. In: Cortier, V., Kremer, S. (eds.) Formal Models and Techniques for Analyzing Security Protocols. IOS Press, Amsterdam (2011)"},{"key":"8_CR28","unstructured":"Clark, J.A., Jacob, J.L.: A survey of authentication protocol literature: version 1.0 (1997). http:\/\/www.cs.york.ac.uk\/jac\/papers\/drareview.ps.gz"},{"key":"8_CR29","first-page":"282","volume":"37","author":"Q Zhang","year":"2008","unstructured":"Zhang, Q., Zhang, L., et al.: A new certified E-mail protocol based on signcrytion. J. Univ. Electron. Sci. Technol. China 37, 282\u2013284 (2008)","journal-title":"J. Univ. Electron. Sci. Technol. China"},{"key":"8_CR30","unstructured":"Blanchet, B., Smyth, B.: ProVerif 1.86pl3: automatic cryptographic protocol verifier, user manual and tutorial (2011). http:\/\/prosecco.gforge.inria.fr\/personal\/bblanche\/proverif\/manual.pdf"}],"container-title":["Lecture Notes in Computer Science","Structured Object-Oriented Formal Language and Method"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-17404-4_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,22]],"date-time":"2025-05-22T16:44:08Z","timestamp":1747932248000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-17404-4_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319174037","9783319174044"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-17404-4_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"17 April 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}