{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,12]],"date-time":"2026-01-12T23:45:26Z","timestamp":1768261526261,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540434771","type":"print"},{"value":"9783540460176","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-46017-9_14","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T21:12:13Z","timestamp":1269897133000},"page":"187-204","source":"Crossref","is-referenced-by-count":34,"title":["Using SPIN to Verify Security Properties of Cryptographic Protocols"],"prefix":"10.1007","author":[{"given":"Paolo","family":"Maggi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Riccardo","family":"Sisto","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,5,23]]},"reference":[{"key":"14_CR1","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1145\/363516.363528","volume":"9","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Jha, S., Marrero, W.: Verifying security protocols with Brutus. ACM Transactions on Software Engineering and Methodology 9 (2000) 443\u2013487","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"key":"14_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/3-540-61042-1_43","volume-title":"Breaking and fixing the Needham-Shroeder public-key protocol using FDR","author":"G. Lowe","year":"1996","unstructured":"Lowe, G.: Breaking and fixing the Needham-Shroeder public-key protocol using FDR. In: Proceeding of TACAS96, LNCS 1055, Springer-Verlag (1996) 147\u2013166"},{"key":"14_CR3","unstructured":"Mitchell, J.C., Mitchell, M., Stern, U.: Automated analysis of cryptographic protocols using murphi. In: Proceedings of the 1997 Conference on Security and Privacy (S&P-97), Los Alamitos, IEEE Press (1997) 141\u2013153"},{"key":"14_CR4","unstructured":"Josang, A.: Security protocol verification using SPIN. SPIN\u201995 Workshop (1995)"},{"key":"14_CR5","doi-asserted-by":"publisher","first-page":"993","DOI":"10.1145\/359657.359659","volume":"21","author":"R.M. Needham","year":"1978","unstructured":"Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. Communications of the ACM 21 (1978) 993\u2013999","journal-title":"Communications of the ACM"},{"key":"14_CR6","doi-asserted-by":"publisher","first-page":"644","DOI":"10.1109\/TIT.1976.1055638","volume":"IT-22","author":"W. Diffie","year":"1976","unstructured":"Diffie, W., Hellman, M.: New directions in cryptography. IEEE Transactions on Information Theory IT-22 (1976) 644\u2013654","journal-title":"IEEE Transactions on Information Theory"},{"key":"14_CR7","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1145\/359340.359342","volume":"21","author":"R.L. Rivest","year":"1978","unstructured":"Rivest, R.L., Shamir, A., Adleman, L.M.: A method for obtaining digital signatures and public-key cryptosystems. Communications of the ACM 21 (1978) 120\u2013126","journal-title":"Communications of the ACM"},{"key":"14_CR8","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1145\/358722.358740","volume":"24","author":"D.E. Denning","year":"1981","unstructured":"Denning, D.E., Sacco, G.M.: Timestamps in key distribution protocols. Communications of the ACM 24 (1981) 533\u2013536","journal-title":"Communications of the ACM"},{"key":"14_CR9","doi-asserted-by":"crossref","unstructured":"Durante, L., Sisto, R., Valenzano, A.: A state exploration technique for spi-calculus testing equivalence verification. In: Proceedings of FORTE\/PSTV 2000, Pisa, Italy, Kluver (2000) 155\u2013170","DOI":"10.1007\/978-0-387-35533-7_10"},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"Lowe, G.: Casper: A compiler for the analysis of security protocols. In: PCSFW: Proceedings of The 10th Computer Security Foundations Workshop, IEEE Computer Society Press (1997)","DOI":"10.1109\/CSFW.1997.596779"},{"key":"14_CR11","unstructured":"Ltd., F.S.E.: Failures-Divergence Refinement. FDR2 User Manual. Available at \n                    http:\/\/www.formal.demon.co.uk\/fdr2manual\/index.html\n                    \n                   (3 May 2000)"},{"key":"14_CR12","unstructured":"Lowe, G.: Casper: A compiler for the analysis of security protocols-user manual and tutorial. Available at \n                    http:\/\/www.mcs.le.ac.uk\/~glowe\/Security\/Casper\/manual.ps\n                    \n                   (1999)"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46017-9_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,24]],"date-time":"2019-02-24T13:56:52Z","timestamp":1551016612000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46017-9_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540434771","9783540460176"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/3-540-46017-9_14","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]}}}