{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:44:06Z","timestamp":1725493446747},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540007081"},{"type":"electronic","value":"9783540365327"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-36532-x_17","type":"book-chapter","created":{"date-parts":[[2007,10,25]],"date-time":"2007-10-25T15:34:36Z","timestamp":1193326476000},"page":"263-282","source":"Crossref","is-referenced-by-count":10,"title":["Typing One-to-One and One-to-Many Correspondences in Security Protocols"],"prefix":"10.1007","author":[{"given":"Andrew D.","family":"Gordon","sequence":"first","affiliation":[]},{"given":"Alan","family":"Jefrey","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,6,25]]},"reference":[{"key":"17_CR1","series-title":"Lect Notes Comput Sci","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":"M. Abadi and B. Blanchet. Secrecy types for asymmetric communication. In Foundations of Software Science and Computation Structures, volume 2030 of Lecture Notes in Computer Science, pages 25\u201341. Springer, 2001."},{"issue":"5","key":"17_CR2","doi-asserted-by":"publisher","first-page":"749","DOI":"10.1145\/324133.324266","volume":"46","author":"M. Abadi","year":"1999","unstructured":"M. Abadi. Secrecy by typing in security protocols. Journal of the ACM, 46(5):749\u2013786, September 1999.","journal-title":"Journal of the ACM"},{"key":"17_CR3","unstructured":"M. Abadi, C. Fournet, and G. Gonthier. Secure communications implementation of channel abstractions. In 13th IEEE Symposium on Logic in Computer Science (LICS\u201998), pages 105\u2013116, 1998."},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"M. Abadi, C. Fournet, and G. Gonthier. Authentication primitives and their compilation. In 27th ACM Symposium on Principles of Programming Languages (POPL\u201900), pages 302\u2013315, 2000.","DOI":"10.1145\/325694.325734"},{"key":"17_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1998.2740","volume":"148","author":"M. Abadi","year":"1999","unstructured":"M. Abadi and A.D. Gordon. A calculus for cryptographic protocols: The spi calculus. Information and Computation, 148:1\u201370, 1999.","journal-title":"Information and Computation"},{"key":"17_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"426","DOI":"10.1007\/BFb0015258","volume-title":"Computer Science Today: Recent Trends and Developments","author":"R. Anderson","year":"1995","unstructured":"R. Anderson and R. Needham. Programming Satan\u2019s computer. In J. van Leeuwen, editor, Computer Science Today: Recent Trends and Developments, volume 1000 of Lecture Notes in Computer Science, pages 426\u2013440. Springer, 1995."},{"key":"17_CR7","doi-asserted-by":"crossref","unstructured":"M. Burrows, M. Abadi, and R.M. Needham. A logic of authentication. Proceedings of the Royal Society of London A, 426:233\u2013271, 1989.","DOI":"10.1145\/74850.74852"},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"F. Butler, I. Cervesato, A.D. Jaggard, and A. Scedrov. A formal analysis of some properties of Kerberos 5 using MSR. In 15th IEEE Computer Security Foundations Workshop, pages 175\u2013190. IEEE Computer Society Press, 2002.","DOI":"10.1109\/CSFW.2002.1021815"},{"key":"17_CR9","series-title":"Lect Notes Comput Sci","first-page":"242","volume-title":"From secrecy to authenticity in security protocols","author":"B. Blanchet","year":"2002","unstructured":"B. Blanchet. From secrecy to authenticity in security protocols. In 9th International Static Analysis Symposium (SAS\u201902), volume 2477 of Lecture Notes in Computer Science, pages 242\u2013259. Springer, 2002."},{"key":"17_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1007\/3-540-45116-1_18","volume-title":"Typed MSR: Syntax and examples","author":"I. Cervesato","year":"2001","unstructured":"I. Cervesato. Typed MSR: Syntax and examples. In First International Workshop on Mathematical Methods, Models and Architectures for Computer Network Security, volume 2052 of Lecture Notes in Computer Science, pages 159\u2013177. Springer, 2001."},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"D. Duggan. Cryptographic types. In 15th IEEE Computer Security Foundations Workshop, pages 238\u2013252. IEEE Computer Society Press, 2002.","DOI":"10.1109\/CSFW.2002.1021819"},{"issue":"2","key":"17_CR12","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"IT-29","author":"D. Dolev","year":"1983","unstructured":"D. Dolev and A.C. Yao. On the security of public key protocols. IEEE Transactions on Information Theory, IT-29(2):198\u2013208, 1983.","journal-title":"IEEE Transactions on Information Theory"},{"key":"17_CR13","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1016\/0304-3975(95)00118-2","volume":"153","author":"J. Engelfriet","year":"1996","unstructured":"J. Engelfriet. A multiset semantics for the pi-calculus with replication. Theoretical Computer Science, 153:65\u201394, 1996.","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"17_CR14","doi-asserted-by":"crossref","first-page":"5","DOI":"10.3233\/JCS-1994\/1995-3103","volume":"3","author":"R. Focardi","year":"1994","unstructured":"R. Focardi and R. Gorrieri. A classi.cation of security properties for process algebra. Journal of Computer Security, 3(1):5\u201333, 1994.","journal-title":"Journal of Computer Security"},{"key":"17_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"258","DOI":"10.1007\/3-540-45499-3_20","volume-title":"Message authentication through non-interference","author":"R. Focardi","year":"2000","unstructured":"R. Focardi, R. Gorrieri, and F. Martinelli. Message authentication through non-interference. In International Conference on Algebraic Methodology And Software Technology (AMAST2000), volume 1816 of Lecture Notes in Computer Science, pages 258\u2013272. Springer, 2000."},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"A.D. Gordon and A. Jeffrey. Authenticity by typing for security protocols. In 14th IEEE Computer Security Foundations Workshop, pages 145\u2013159. IEEE Computer Society Press, 2001.","DOI":"10.1109\/CSFW.2001.930143"},{"key":"17_CR17","doi-asserted-by":"crossref","unstructured":"A.D. Gordon and A. Jeffrey. Typing correspondence assertions for communication protocols. In Mathematical Foundations of Programming Semantics 17, volume 45 of Electronic Notes in Theoretical Computer Science. Elsevier, 2001.","DOI":"10.1016\/S1571-0661(04)80959-9"},{"key":"17_CR18","doi-asserted-by":"crossref","unstructured":"A.D. Gordon and A. Jeffrey. Types and e.ects for asymmetric cryptographic protocols. In 15th IEEE Computer Security Foundations Workshop, pages 77\u201391. IEEE Computer Society Press, 2002.","DOI":"10.1109\/CSFW.2002.1021808"},{"key":"17_CR19","doi-asserted-by":"crossref","unstructured":"D.K. Gifford and J.M. Lucassen. Integrating functional and imperative programming. In ACM Conference on Lisp and Functional Programming, pages 28\u201338, 1986.","DOI":"10.1145\/319838.319848"},{"key":"17_CR20","unstructured":"D. Gollmann. Authentication by correspondence. IEEE Journal on Selected Areas in Communication, 2002. To appear."},{"key":"17_CR21","doi-asserted-by":"crossref","unstructured":"A.D. Gordon and R. Pucella. Validating a web service security abstraction by typing. In ACM Workshop on XML Security, 2002. To appear.","DOI":"10.1145\/764792.764797"},{"issue":"2","key":"17_CR22","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/S0304-3975(01)00139-6","volume":"283","author":"J.D. Guttman","year":"2002","unstructured":"J.D. Guttman and F.J. Thayer. Authentication tests and the structure of bundles. Theoretical Computer Science, 283(2):333\u2013380, 2002.","journal-title":"Theoretical Computer Science"},{"key":"17_CR23","unstructured":"B.A. LaMacchia, S. Lange, M. Lyons, R. Martin, and K.T. Price..NET Framework Security. Addison Wesley Professional, 2002."},{"key":"17_CR24","doi-asserted-by":"crossref","unstructured":"G. Lowe. A hierarchy of authentication speci.cations. In 10th IEEE Computer Security Foundations Workshop, pages 31\u201343. IEEE Computer Society Press, 1997.","DOI":"10.1109\/CSFW.1997.596782"},{"key":"17_CR25","unstructured":"T. Lindholm and F. Yellin. The Java \u2122 Virtual Machine Speci.cation. Addison-Wesley, 1997."},{"issue":"2","key":"17_CR26","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/0743-1066(95)00095-X","volume":"26","author":"C. Meadows","year":"1996","unstructured":"C. Meadows. The NRL Protocol Analyzer: An overview. Journal of Logic Programming, 26(2):113\u2013131, 1996.","journal-title":"Journal of Logic Programming"},{"key":"17_CR27","doi-asserted-by":"crossref","first-page":"85","DOI":"10.3233\/JCS-1998-61-205","volume":"6","author":"L.C. Paulson","year":"1998","unstructured":"L.C. Paulson. The inductive approach to verifying cryptographic protocols. Journal of Computer Security, 6:85\u2013128, 1998.","journal-title":"Journal of Computer Security"},{"key":"17_CR28","unstructured":"B. Pierce and E. Sumii. Relating cryptography and polymorphism. Available from the authors, 2000."},{"key":"17_CR29","doi-asserted-by":"crossref","unstructured":"A.W. Roscoe. Intensional speci.cations of security protocols. In 8th IEEE Computer Security Foundations Workshop, pages 28\u201338. IEEE Computer Society Press, 1996.","DOI":"10.1109\/CSFW.1996.503688"},{"issue":"9","key":"17_CR30","doi-asserted-by":"publisher","first-page":"741","DOI":"10.1109\/32.713329","volume":"24","author":"S.A. Schneider","year":"1998","unstructured":"S.A. Schneider. Verifying authentication protocols in CSP. IEEE Transactions on Software Engineering, 24(9):741\u2013758, 1998.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"17_CR31","unstructured":"A. Sabelfeld and A.C. Myers. Language-based information-flow security.IEEE Journal on Selected Areas in Communication, 2002. To appear."},{"key":"17_CR32","doi-asserted-by":"crossref","unstructured":"T.Y.C. Woo and S.S. Lam. A semantic model for authentication protocols. In IEEE Computer Society Symposium on Research in Security and Privacy, pages 178\u2013194, 1993.","DOI":"10.1109\/RISP.1993.287633"}],"container-title":["Lecture Notes in Computer Science","Software Security \u2014 Theories and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36532-X_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T20:54:19Z","timestamp":1556916859000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36532-X_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540007081","9783540365327"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/3-540-36532-x_17","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}