{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:30:01Z","timestamp":1761597001072,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540410317"},{"type":"electronic","value":"9783540452997"}],"license":[{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10722599_14","type":"book-chapter","created":{"date-parts":[[2006,12,30]],"date-time":"2006-12-30T06:41:21Z","timestamp":1167460881000},"page":"222-237","source":"Crossref","is-referenced-by-count":37,"title":["Analysing Time Dependent Security Properties in CSP Using PVS"],"prefix":"10.1007","author":[{"given":"Neil","family":"Evans","sequence":"first","affiliation":[]},{"given":"Steve","family":"Schneider","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"14_CR1","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":"14_CR2","doi-asserted-by":"crossref","unstructured":"Burrows, M., Abadi, M., Needham, R.: A logic of authentication. ACM Transactions on Computer Systems\u00a08 (1989)","DOI":"10.1145\/74850.74852"},{"issue":"3","key":"14_CR3","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1016\/0020-0190(95)00136-Z","volume":"56","author":"J. Clark","year":"1995","unstructured":"Clark, J., Jacob, J.: On the security of recent protocols. Information Processing Letters\u00a056(3), 151\u2013155 (1995)","journal-title":"Information Processing Letters"},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Transactions on Information Theory\u00a029(2) (1983)","DOI":"10.1109\/TIT.1983.1056650"},{"key":"14_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028390","volume-title":"Theorem Proving in Higher Order Logics","author":"B. Dutertre","year":"1997","unstructured":"Dutertre, B., Schneider, S.: Embedding CSP in PVS. an application to authentication protocols. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol.\u00a01275. Springer, Heidelberg (1997)"},{"key":"14_CR6","unstructured":"Lowe, G.: Casper: A compiler for the analysis of security protocols. In: Proceedings of the 10th IEEE Computer Security Foundations Workshop (1997)"},{"key":"14_CR7","doi-asserted-by":"crossref","unstructured":"Meadows, C.: Language generation and verification in the NRL Protocol Analyzer. In: Proceedings of the 10th IEEE Computer Security Foundations Workshop (1996)","DOI":"10.21236\/ADA465477"},{"key":"14_CR8","unstructured":"Meadows, C.: Personal communication (2000)"},{"key":"14_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction - CADE-11","author":"S. Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607, pp. 748\u2013752. Springer, Heidelberg (1992)"},{"key":"14_CR10","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A Generic Theorem Prover","author":"L.C. Paulson","year":"1994","unstructured":"Paulson, L.C.: Isabelle: A Generic Theorem Prover. Springer, Heidelberg (1994)"},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"Schneider, S.A.: Verifying authentication protocols in CSP. IEEE Transactions on Software Engineering (1998)","DOI":"10.1109\/32.713329"},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"Schneider, S.A.: Timewise refinement for communicating processes. Science of Computer Programming 28 (1997)","DOI":"10.1016\/S0167-6423(96)00016-0"},{"key":"14_CR13","volume-title":"Concurrent and Real-time Systems","author":"S.A. Schneider","year":"1999","unstructured":"Schneider, S.A.: Concurrent and Real-time Systems. Wiley, Chichester (1999)"},{"key":"14_CR14","unstructured":"Thayer, J., Herzog, J.C., Guttman, J.D.: Strand spaces: Proving security protocols correct. Journal of Computer Security (1999)"}],"container-title":["Lecture Notes in Computer Science","Computer Security - ESORICS 2000"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10722599_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,2]],"date-time":"2019-06-02T20:32:41Z","timestamp":1559507561000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10722599_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540410317","9783540452997"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/10722599_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}