{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,2]],"date-time":"2025-08-02T19:06:16Z","timestamp":1754161576043,"version":"3.41.2"},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[1996,1,1]],"date-time":"1996-01-01T00:00:00Z","timestamp":820454400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1996,1,1]],"date-time":"1996-01-01T00:00:00Z","timestamp":820454400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Designs, Codes and Cryptography"],"published-print":{"date-parts":[[1996,1]]},"DOI":"10.1023\/a:1018069220646","type":"journal-article","created":{"date-parts":[[2003,11,3]],"date-time":"2003-11-03T19:30:08Z","timestamp":1067887808000},"page":"27-59","source":"Crossref","is-referenced-by-count":5,"title":["A Formal Language for Cryptographic Protocol Requirements"],"prefix":"10.1007","volume":"7","author":[{"given":"Paul","family":"Syverson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Catherine","family":"Meadows","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"102719_CR1","unstructured":"Martin Abadi, An Axiomatization of Lamport's Temporal Logic of Action, Research Report 65, Digital Systems Research Center, (October 1990)."},{"key":"102719_CR2","doi-asserted-by":"crossref","unstructured":"Martin Abadi and Mark Tuttle, A semantics for a logic of authentication, Proceedings of the Tenth ACM Symposium on Principles of Distributed Computing, ACM Press (August 1991) pp. 201\u2013216.","DOI":"10.1145\/112600.112618"},{"issue":"1","key":"102719_CR3","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1109\/98.295357","volume":"1","author":"A. Aziz","year":"1994","unstructured":"A. Aziz and W. Diffle, Privacy and authentication for wireless local area networks, IEEE Personal Communications, Vol. 1, No. 1 (1994) pp 25\u201331.","journal-title":"IEEE Personal Communications"},{"key":"102719_CR4","unstructured":"M. Bellare and P. Rogaway, Entity authentication and key distribution, Advances in Cryptology\u2014CRYPTO '93, volume to appear, Springer-Verlag (1994)."},{"key":"102719_CR5","series-title":"Lecture Notes in Computer Science","volume-title":"Advances in Cryptology\u2014CRYPTO '91","author":"R. Bird","year":"1992","unstructured":"Ray Bird, lnder Gopal, Amir Herzberg, Phil Janson, Shay Kutten, Refik Molva, and Moti Yung, Systematic design of two-party authentication protocols, Advances in Cryptology\u2014CRYPTO '91, (Joan Feigenbaum, ed.), Lecture Notes in Computer Science, Springer-Verlag, Berlin, 572 (1992)."},{"key":"102719_CR6","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1016\/0167-4048(90)90159-Q","volume":"9","author":"J. Burns","year":"1990","unstructured":"J. Burns and C. J. Mitchell, A security scheme for resource sharing over a network, Computers and Security, Vol. 9 (1990) pp. 67\u201376.","journal-title":"Computers and Security"},{"issue":"1","key":"102719_CR7","first-page":"18","volume":"8","author":"M. Burrows","year":"1990","unstructured":"Michael Burrows, Martin Abadi, and Roger Needham, A Logic of Authentication, Research Report 39, Digital Systems Research Center February 1989. Parts and versions of this material have been presented in many places including ACM Transactions on Computer Systems, Vol. 8, No. 1 (1990) pp. 18\u201336, All references herein are to the SRC Research Report 39 as revised Feb. 22, 1990.","journal-title":"Digital Systems Research Center February 1989"},{"issue":"2","key":"102719_CR8","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1145\/382258.382790","volume":"24","author":"M. Burrows","year":"1990","unstructured":"Michael Burrows, Martin Abadi and Roger Needham, Rejoinder to Nessett, Operating Systems Review, Vol. 24, No. 2 (1990) pp. 39\u201340.","journal-title":"Operating Systems Review"},{"key":"102719_CR9","doi-asserted-by":"crossref","unstructured":"D. Chaum, A. Fial, and M. Naor, Untraceable electronic cash, Advances in Cryptology-CRYPTO '88, (S. Goldwasser, ed.) Springer-Verlag, LNCS 403 (1990) pp. 319\u2013327.","DOI":"10.1007\/0-387-34799-2_25"},{"issue":"6","key":"102719_CR10","doi-asserted-by":"crossref","first-page":"644","DOI":"10.1109\/TIT.1976.1055638","volume":"IT-22","author":"W. Diffle","year":"1976","unstructured":"Whitfield Diffle and Martin E. Hellman, New Directions in Cryptography, IEEE Transactions on Information Theory, Vol. IT-22, No. 6 (1976) pp. 644\u2013654.","journal-title":"IEEE Transactions on Information Theory"},{"key":"102719_CR11","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1007\/BF00124891","volume":"2","author":"W. Diffle","year":"1992","unstructured":"Whitfield Diffle, Pau1 C. van Oorschot, and Michael J Wiener, Authentication and authenticated key exchanges, Designs, Codes, and Cryptography, Vol. 2 (1992) pp. 107\u2013125.","journal-title":"Designs, Codes, and Cryptography"},{"issue":"2","key":"102719_CR12","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"29","author":"D. Dolev","year":"1983","unstructured":"D. Dolev and A. Yao, On the security of public Key protocols, IEEE Transactions on Information Theory, Vol. 29, No. 2 (1983) pp. 198\u2013208.","journal-title":"IEEE Transactions on Information Theory"},{"issue":"4","key":"102719_CR13","doi-asserted-by":"crossref","first-page":"469","DOI":"10.1109\/TIT.1985.1057074","volume":"IT-31","author":"T. El Gamal","year":"1985","unstructured":"Taher El Gamal, A public-key cryptosystem and a signature scheme based on discrete logarithms, IEEE Transactions on Information Theory, Vol. IT-31. No. 4 (1985) pp. 469\u2013472.","journal-title":"IEEE Transactions on Information Theory"},{"key":"102719_CR14","series-title":"CSLI Lecture Notes","volume-title":"Logic Of Time and Computation","author":"R. Goldblatt","year":"1992","unstructured":"Robert Goldblatt, Logic Of Time and Computation, 2nd edition CSLI Lecture Notes, CSLI Publications, Stanford, 7 (1992).","edition":"2nd edition"},{"key":"102719_CR15","unstructured":"Leslie Lamport, A Temporal Logic of Action, Research Report 57, Digirtal sustems research Center, (April 1990)."},{"key":"102719_CR16","first-page":"182","volume-title":"Proceedings of the 1991 IEEE Computer Society Symosium on Research in Security and Privacy","author":"C. Meadows","year":"1991","unstructured":"C. Meadows, A sytem for the specification and analysis of key management protocols, Proceedings of the 1991 IEEE Computer Society Symosium on Research in Security and Privacy, IEEE Computer Society Press, Los Alamilos, California, (1991) pp. 182\u2013195."},{"key":"102719_CR17","doi-asserted-by":"crossref","first-page":"5","DOI":"10.3233\/JCS-1992-1102","volume":"1","author":"C. Meadows","year":"1992","unstructured":"C. Meadows, Applying formal methods to the anslysis of a key management protocol, Journal of Computer Security, Vol. 1 (1992) pp. 5\u201353.","journal-title":"Journal of Computer Security"},{"key":"102719_CR18","unstructured":"M. L. Merntt, Cryptographic Protocols, Phd thesis, Georgia Institute of Technology (1983)."},{"key":"102719_CR19","volume-title":"Project Athena Technical Plan","author":"S. P. Miller","year":"1987","unstructured":"S. P. Miller, C. Neuman, J. I. Schiller and J. H. Saltzer, Kerberos authentication and <nt>authoriaalian<\/nt>Authorization system, in Project Athena Technical Plan, MIT. Cambridge, Mass. (Jaly 1987)."},{"issue":"2","key":"102719_CR20","doi-asserted-by":"crossref","first-page":"35\u201318","DOI":"10.1145\/382258.382789","volume":"24","author":"D. M. Nessett","year":"1990","unstructured":"D. M. Nessett, A critique of the Burrows, Abadi, and Needham logic, Operating Systems Review, VoI 24, No 2 (1990) pp. 35\u201318.","journal-title":"Operating Systems Review"},{"key":"102719_CR21","first-page":"85","volume-title":"Proceedings of the 1992","author":"S. G. Stubhiehino","year":"1992","unstructured":"S. G. Stubhiehino and V. D. Gligur, On message integrity in cryptographic protocols. Proceedings of the 1992, IEEE Computer Society Press, Lus Alamilos, California (1992) pp 85\u2013104."},{"key":"102719_CR22","first-page":"165","volume-title":"Proceedings of the 1993 IEE Computer Society Symposium on Research in Security and Privacy","author":"P. Syverson","year":"1993","unstructured":"Paul Syverson and Cathennc Meadows, A logical languqe lor spccifymg cryplographic protocol rcquire-ments, Proceedings of the 1993 IEE Computer Society Symposium on Research in Security and Privacy, IEEE Computer Society Press, Los Alaminos, California (1993) pp. 165\u2013177"},{"key":"102719_CR23","first-page":"325","volume-title":"Prep-proceedings of EUROCRYPT '94","author":"P. Syverson","year":"1994","unstructured":"Paul Syverson and Catherine Meadows, Formal requirements for key distributin protocols, Prep-proceedings of EUROCRYPT '94, University of Perugia, Italy, (1994) pp. 325\u2013337. Final proceedings forthcoming from Springer-Verlag."},{"key":"102719_CR24","first-page":"156","volume-title":"Proceedings orthc 1991 IEEE Computer Suciety Symposium on Research in Security and Privacy","author":"P. F. Syverson","year":"1991","unstructured":"Paul F. Syverson. The use of logic m thc analysis of cryptographic protocols, Proceedings orthc 1991 IEEE Computer Suciety Symposium on Research in Security and Privacy, IEEE Computcr Society Press, Los Alamitos, California (1991) pp. 156\u2013170."},{"key":"102719_CR25","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1145\/168588.168600","volume-title":"Proceedings of the Firs1 ACM Conference on Computer and Communications Security","author":"P. P. Syverson","year":"1993","unstructured":"Paul P. Syverson. Adding tmc to a logic of authentication. Proceedings of the Firs1 ACM Conference on Computer and Communications Security, ACM Press, New York (1993) pp. 97\u2013101"},{"issue":"4","key":"102719_CR26","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1145\/163640.163642","volume":"27","author":"P. F. Syverson","year":"1993","unstructured":"Paul F. Syverson, On key distribution protocols for repeated authentication, Operating Systems Review, Vol 27, No. 4 (1993) pp. 24\u201330.","journal-title":"Operating Systems Review"},{"key":"102719_CR27","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1007\/BFb0013893","volume":"638","author":"M.J. Toussaint","year":"1992","unstructured":"M.J. Toussaint, Separating the specification and Implementation phases in cryprology, Computer Security-ESORICS 92. Springer-Verlag LMCS 638 (1992) pp. 77\u2013102.","journal-title":"Computer Security-ESORICS 92"},{"key":"102719_CR28","series-title":"Synthese Library","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-015-7947-6","volume-title":"The Logic of Time","author":"J. van Bentham","year":"1991","unstructured":"Johan van Bentham, The Logic of Time, Synthese Library, Vol. 156, Kluwer Academic Publishers, Dordrecht, The Netherlands, second edition, (1991).","edition":"second edition"},{"key":"102719_CR29","unstructured":"T. Y. C. Woo and S. Lam, A Asemantic model for authentication protocols, Proceedings of the 1993 Syrnposium on Research in Security and Privacy. IEEE Computer Society Press (1993) pp. 178\u2013194."},{"issue":"2\u20133","key":"102719_CR30","first-page":"191","volume":"2","author":"R. Yahalom","year":"1994","unstructured":"R. Yahalom, Optinality of asynchronous two-party secure data-exchange protocols, Journal of Computer Security, Vol. 2, No. 2\u20133 (1994) pp. 191\u2013209.","journal-title":"Journal of Computer Security"}],"container-title":["Designs, Codes and Cryptography"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1018069220646.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1018069220646\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1018069220646.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,29]],"date-time":"2025-07-29T03:40:57Z","timestamp":1753760457000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1018069220646"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996,1]]},"references-count":30,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[1996,1]]}},"alternative-id":["102719"],"URL":"https:\/\/doi.org\/10.1023\/a:1018069220646","relation":{},"ISSN":["0925-1022","1573-7586"],"issn-type":[{"type":"print","value":"0925-1022"},{"type":"electronic","value":"1573-7586"}],"subject":[],"published":{"date-parts":[[1996,1]]}}}