{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:11Z","timestamp":1761611171683},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540633792"},{"type":"electronic","value":"9783540695264"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/bfb0028390","type":"book-chapter","created":{"date-parts":[[2005,11,22]],"date-time":"2005-11-22T06:50:11Z","timestamp":1132642211000},"page":"121-136","source":"Crossref","is-referenced-by-count":33,"title":["Using a PVS embedding of CSP to verify authentication protocols"],"prefix":"10.1007","author":[{"given":"Bruno","family":"Dutertre","sequence":"first","affiliation":[]},{"given":"Steve","family":"Schneider","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,17]]},"reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"S. H. Brackin. Deciding Cryptographic Protocol Adequacy with HOL: The Implementation. In TPHOLs'96. Springer-Verlag, LNCS 1125, 1996.","DOI":"10.1007\/BFb0105397"},{"key":"9_CR2","unstructured":"J. Bryans and S. Schneider. Mechanical Verification of the full Needham-Schroeder public key protocol. Technical report, Royal Holloway, University of London, 1997."},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"M. Burrows, M, Abadi, and R. Needham. A Logic of Authentication. Technical Report 39, Digital Equipment Corporation, System Research Center, 1989.","DOI":"10.1145\/74850.74852"},{"issue":"9","key":"9_CR4","doi-asserted-by":"crossref","first-page":"993","DOI":"10.1109\/32.58786","volume":"16","author":"A. J. Camilleri","year":"1990","unstructured":"A. J. Camilleri. Mechanizing CSP trace theory in higher order logic. IEEE Transactions on Software Engineering, 16(9):993\u20131004, 1990.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"9_CR5","unstructured":"J. Crow, S. Owre, 1 Rushby, N. Shankar, and M. Srivas. A tutorial introduction to PVS. In Workshop on Industrial-Strength Formal Specification Techniques, 1995."},{"key":"9_CR6","unstructured":"B. Dutertre and S. Schneider. Embedding CSP in PVS. An Application to Authentication Protocols. Technical report, Royal Holloway, CSD-TR-97-12."},{"key":"9_CR7","unstructured":"C. A R. Hoare. Communicating Sequential Processes. Prentice-Hall International, 1985."},{"key":"9_CR8","doi-asserted-by":"crossref","unstructured":"R. Kemmerer, C. Meadows, and Millen J. Three systems for cryptographic analysis. Journal of Cryptology, 7(2), 1994.","DOI":"10.1007\/BF00197942"},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"G. Lowe. Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR. In Proc. of TACAS'96. Springer-Verlag, LNCS 1055, 1996.","DOI":"10.1007\/3-540-61042-1_43"},{"issue":"12","key":"9_CR10","doi-asserted-by":"crossref","first-page":"990","DOI":"10.1145\/359657.359659","volume":"21","author":"R. M. Needham","year":"1978","unstructured":"R. M. Needham and M. D. Schroeder. Using Encryption for Authentication in Large Networks of Computers. Comm. of the ACM, 21(12):990\u2013999, 1978.","journal-title":"Comm. of the ACM"},{"key":"9_CR11","unstructured":"S. Owre, N. Shankar, and J. M. Rushby. The PVS Specification Language. Computer Science Lab., SRI International, 1993."},{"key":"9_CR12","unstructured":"L. Paulson. Proving Properties of Security Protocols by Induction. Technical Report TR409, Computer Laboratory, University of Cambridge, 1996."},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"S. Schneider. Security Properties and CSP. In IEEE Symposium on Security and Privacy, 1996.","DOI":"10.1109\/SECPRI.1996.502680"},{"key":"9_CR14","unstructured":"S. Schneider. Using CSP for protocol analysis: the Needham-Schroeder Public Key Protocol. Technical Report CSD-TR-96-14, Royal Holloway, 1996.."},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"J. U. Skakkebask and N. Shankar. Towards a duration calculus proof assistant in PVS. In Formal Techniques in Real-Time and Fault-Tolerant Systems. Springer-Verlag, LNCS 863, September 1994.","DOI":"10.1007\/3-540-58468-4_189"},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"P. Syverson and P. van Oorschot. On Unifying Some Cryptographic Protocol Logics. In Proc. of the 19N IEEE 4M. on Research in Security and Privacy, 1994.","DOI":"10.21236\/ADA465512"},{"key":"9_CR17","unstructured":"F. J. Thayer. An approach to process algebra using mWs. Technical Report MP-94B193, The mitre Corporation, 1994."}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0028390","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,20]],"date-time":"2021-07-20T03:43:42Z","timestamp":1626752622000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0028390"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540633792","9783540695264"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/bfb0028390","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}