{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:28:49Z","timestamp":1761596929446},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540283096"},{"type":"electronic","value":"9783540319344"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11539452_18","type":"book-chapter","created":{"date-parts":[[2005,9,27]],"date-time":"2005-09-27T13:54:50Z","timestamp":1127829290000},"page":"202-216","source":"Crossref","is-referenced-by-count":9,"title":["Timed Spi-Calculus with Types for Secrecy and Authenticity"],"prefix":"10.1007","author":[{"given":"Christian","family":"Haack","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alan","family":"Jeffrey","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"5","key":"18_CR1","doi-asserted-by":"publisher","first-page":"749","DOI":"10.1145\/324133.324266","volume":"46","author":"M. Abadi","year":"1999","unstructured":"Abadi, M.: Secrecy by typing in security protocols. Journal of the ACM\u00a046(5), 749\u2013786 (1999)","journal-title":"Journal of the ACM"},{"key":"18_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/3-540-45315-6_2","volume-title":"Foundations of Software Science and Computation Structures","author":"M. Abadi","year":"2001","unstructured":"Abadi, M., Blanchet, B.: Secrecy types for asymmetric communication. In: Honsell, F., Miculan, M. (eds.) FOSSACS 2001. LNCS, vol.\u00a02030, p. 25. Springer, Heidelberg (2001)"},{"key":"18_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1998.2740","volume":"148","author":"M. Abadi","year":"1999","unstructured":"Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: The spi calculus. Information and Computation\u00a0148, 1\u201370 (1999)","journal-title":"Information and Computation"},{"issue":"1","key":"18_CR4","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1109\/32.481513","volume":"22","author":"M. Abadi","year":"1996","unstructured":"Abadi, M., Needham, R.: Prudent engineering practice for cryptographic protocols. IEEE Transactions on Software Engineering\u00a022(1), 6\u201315 (1996)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"18_CR5","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.M.: A logic of authentication. Proceedings of the Royal Society of London A\u00a0426, 233\u2013271 (1989)","journal-title":"Proceedings of the Royal Society of London A"},{"key":"18_CR6","unstructured":"Clark, J., Jacob, J.: A survey of authentication protocol literature. Unpublished report. University of York (1997)"},{"key":"18_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/978-3-540-24730-2_27","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Delzanno","year":"2004","unstructured":"Delzanno, G., Ganty, P.: Automatic verification of time sensitive cryptographic protocols. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 342\u2013356. Springer, Heidelberg (2004)"},{"issue":"8","key":"18_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\u00a024(8), 533\u2013536 (1981)","journal-title":"Communications of the ACM"},{"key":"18_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1007\/10722599_14","volume-title":"Computer Security - ESORICS 2000","author":"N. Evans","year":"2000","unstructured":"Evans, N., Schneider, S.: Analysing time dependent security properties in CSP using PVS. In: Cuppens, F., Deswarte, Y., Gollmann, D., Waidner, M. (eds.) ESORICS 2000. LNCS, vol.\u00a01895, pp. 222\u2013237. Springer, Heidelberg (2000)"},{"key":"18_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1007\/3-540-36532-X_17","volume-title":"Proc. Int. Software Security Symp.","author":"A.D. Gordon","year":"2003","unstructured":"Gordon, A.D., Jeffrey, A.S.A.: Typing one-to-one and one-to-many correspondences in security protocols. In: Okada, M., Pierce, B.C., Scedrov, A., Tokuda, H., Yonezawa, A. (eds.) ISSS 2002. LNCS, vol.\u00a02609, pp. 263\u2013282. Springer, Heidelberg (2003)"},{"issue":"4","key":"18_CR11","doi-asserted-by":"crossref","first-page":"451","DOI":"10.3233\/JCS-2003-11402","volume":"11","author":"A.D. Gordon","year":"2003","unstructured":"Gordon, A.D., Jeffrey, A.S.A.: Authenticity by typing for security protocols. J. Computer Security\u00a011(4), 451\u2013521 (2003)","journal-title":"J. Computer Security"},{"issue":"3\/4","key":"18_CR12","first-page":"435","volume":"12","author":"A.D. Gordon","year":"2003","unstructured":"Gordon, A.D., Jeffrey, A.S.A.: Types and effects for asymmetric cryptographic protocols. J. Computer Security\u00a012(3\/4), 435\u2013484 (2003)","journal-title":"J. Computer Security"},{"key":"18_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"186","DOI":"10.1007\/11539452_17","volume-title":"CONCUR 2005 \u2013 Concurrency Theory","author":"A.D. Gordon","year":"2005","unstructured":"Gordon, A.D., Jeffrey, A.S.A.: Secrecy despite compromise: Types, cryptography and the pi-calculus. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol.\u00a03653, pp. 186\u2013201. Springer, Heidelberg (2005)"},{"key":"18_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"114","DOI":"10.1007\/3-540-36575-3_9","volume-title":"12th European Symposium on Programming","author":"R. Gorrieri","year":"2003","unstructured":"Gorrieri, R., Locatelli, E., Martinelli, F.: A simple language for realtime cryptographic protocol analysis. In: Degano, P. (ed.) ESOP 2003. LNCS, vol.\u00a02618, pp. 114\u2013128. Springer, Heidelberg (2003)"},{"key":"18_CR15","unstructured":"Guttman, J.D.: Key compromise, strand spaces, and the authentication tests. Electr. Notes Theor. Comput. Sci.\u00a045 (2001)"},{"key":"18_CR16","series-title":"IFIP","volume-title":"2nd IFIP Workshop on Formal Aspects in Security and Trust","author":"C. Haack","year":"2004","unstructured":"Haack, C., Jeffrey, A.S.A.: Pattern-matching spi-calculus. In: 2nd IFIP Workshop on Formal Aspects in Security and Trust. IFIP, vol.\u00a0173. Kluwer Academic Press, Dordrecht (2004)"},{"key":"18_CR17","first-page":"255","volume-title":"13th IEEE Computer Security Foundations Workshop","author":"J. Heather","year":"2000","unstructured":"Heather, J., Lowe, G., Schneider, S.: How to prevent type flaw attacks on security protocols. In: 13th IEEE Computer Security Foundations Workshop, pp. 255\u2013268. IEEE Computer Society Press, Los Alamitos (2000)"},{"issue":"2","key":"18_CR18","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1006\/inco.1995.1041","volume":"117","author":"M. Hennessy","year":"1995","unstructured":"Hennessy, M., Regan, T.: A process algebra for timed systems. Information and Computation\u00a0117(2), 221\u2013239 (1995)","journal-title":"Information and Computation"},{"key":"18_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/978-3-540-28644-8_12","volume-title":"CONCUR 2004 - Concurrency Theory","author":"L. Bozga","year":"2004","unstructured":"Bozga, L., Ene, C., Lakhnech, Y.: A symbolic decision procedure for cryptographic protocols with time stamps. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol.\u00a03170, pp. 177\u2013192. Springer, Heidelberg (2004)"},{"issue":"12","key":"18_CR20","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\u00a021(12), 993\u2013999 (1978)","journal-title":"Communications of the ACM"},{"key":"18_CR21","doi-asserted-by":"crossref","first-page":"85","DOI":"10.3233\/JCS-1998-61-205","volume":"6","author":"L.C. Paulson","year":"1998","unstructured":"Paulson, L.C.: The inductive approach to verifying cryptographic protocols. Journal of Computer Security\u00a06, 85\u2013128 (1998)","journal-title":"Journal of Computer Security"},{"key":"18_CR22","volume-title":"Modelling and Analysis of Security Protocols","author":"P. Ryan","year":"2001","unstructured":"Ryan, P., Schneider, S.: Modelling and Analysis of Security Protocols. Addison-Wesley, Reading (2001)"}],"container-title":["Lecture Notes in Computer Science","CONCUR 2005 \u2013 Concurrency Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11539452_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,17]],"date-time":"2019-03-17T09:16:28Z","timestamp":1552814188000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11539452_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540283096","9783540319344"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/11539452_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}