Analyzing security protocols with secrecy types and logic programs
Tóm tắt
Từ khóa
Tài liệu tham khảo
Abadi , M. 2000. Security protocols and their properties . In Foundations of Secure Computation , F. Bauer and R. Steinbrueggen, Eds. NATO Science Series. IOS Press , Amsterdam, The Netherlands, 39--60. (Volume for the 20th International Summer School on Foundations of Secure Computation, held in Marktoberdorf, Germany (1999).)]] Abadi, M. 2000. Security protocols and their properties. In Foundations of Secure Computation, F. Bauer and R. Steinbrueggen, Eds. NATO Science Series. IOS Press, Amsterdam, The Netherlands, 39--60. (Volume for the 20th International Summer School on Foundations of Secure Computation, held in Marktoberdorf, Germany (1999).)]]
Abadi , M. , and Blanchet , B . 2003a. Computer-assisted verification of a protocol for certified email. In Static Analysis , 10th International Symposium (SAS'03) (San Diego, Calif.), R. Cousot, Ed. Lecture Notes in Computer Science , vol. 2694 . Springer-Verlag, Berlin, Germany, 316--335.]] Abadi, M., and Blanchet, B. 2003a. Computer-assisted verification of a protocol for certified email. In Static Analysis, 10th International Symposium (SAS'03) (San Diego, Calif.), R. Cousot, Ed. Lecture Notes in Computer Science, vol. 2694. Springer-Verlag, Berlin, Germany, 316--335.]]
Abadi , M. , Blanchet , B. , and Fournet , C . 2004. Just fast keying in the pi calculus . In Programming Languages and Systems: 13th European Symposium on Programming (ESOP 2004) (Barcelona, Spain), D. Schmidt, Ed. Lecture Notes in Computer Science , vol. 2986 . Springer-Verlag, Berlin, Germany, 340--354.]] Abadi, M., Blanchet, B., and Fournet, C. 2004. Just fast keying in the pi calculus. In Programming Languages and Systems: 13th European Symposium on Programming (ESOP 2004) (Barcelona, Spain), D. Schmidt, Ed. Lecture Notes in Computer Science, vol. 2986. Springer-Verlag, Berlin, Germany, 340--354.]]
Bachmair , L. , and Ganzinger , H. 1998 . Equational reasoning in saturation-based theorem proving. In Automated Deduction---A Basis for Applications, W. Bibel and P. Schmitt, Eds. Vol. I. Kluwer, Dordrecht, The Netherlands , Chapter 11 , 353 -- 397 .]] Bachmair, L., and Ganzinger, H. 1998. Equational reasoning in saturation-based theorem proving. In Automated Deduction---A Basis for Applications, W. Bibel and P. Schmitt, Eds. Vol. I. Kluwer, Dordrecht, The Netherlands, Chapter 11, 353--397.]]
Blanchet , B. , and Podelski , A . 2003. Verification of cryptographic protocols: Tagging enforces termination. Foundations of Software Science and Computation Structures , 6th International Conference. (FoSSaCS'03) (Warsaw, Poland). A. Gordon, Ed. Lecture Notes in Computer Science , vol. 2620 . Springer-Verlag, Berlin, Germany, 136--152.]] Blanchet, B., and Podelski, A. 2003. Verification of cryptographic protocols: Tagging enforces termination. Foundations of Software Science and Computation Structures, 6th International Conference. (FoSSaCS'03) (Warsaw, Poland). A. Gordon, Ed. Lecture Notes in Computer Science, vol. 2620. Springer-Verlag, Berlin, Germany, 136--152.]]
Bodei , C. , Degano , P. , Nielson , F. , and Nielson , H . 1998. Control flow analysis for the π-calculus . CONCUR'98: Concurrency Theory, 9th International Conference. Lecture Notes in Computer Science , vol. 1466 . Springer Verlag, Berlin, Germany, 84--98.]] Bodei, C., Degano, P., Nielson, F., and Nielson, H. 1998. Control flow analysis for the π-calculus. CONCUR'98: Concurrency Theory, 9th International Conference. Lecture Notes in Computer Science, vol. 1466. Springer Verlag, Berlin, Germany, 84--98.]]
Cardelli , L. 1997 . Type systems. In The Computer Science and Engineering Handbook, A. B. Tucker, Ed. CRC Press, Boca Raton, Fla . Chap. 103 , 2208 -- 2236 .]] Cardelli, L. 1997. Type systems. In The Computer Science and Engineering Handbook, A. B. Tucker, Ed. CRC Press, Boca Raton, Fla. Chap. 103, 2208--2236.]]
Cervesato , I. , Durgin , N. A. , Lincoln , P. D. , Mitchell , J. C. , and Scedrov , A . 1999. A meta-notation for protocol analysis . In Proceedings of the 12th IEEE Computer Security Foundations Workshop (CSFW'99) . IEEE Computer Society, Los Alamitos, Calif., 55--69.]] Cervesato, I., Durgin, N. A., Lincoln, P. D., Mitchell, J. C., and Scedrov, A. 1999. A meta-notation for protocol analysis. In Proceedings of the 12th IEEE Computer Security Foundations Workshop (CSFW'99). IEEE Computer Society, Los Alamitos, Calif., 55--69.]]
Comon-Lundh , H. , and Cortier , V . 2003. New decidability results for fragments of first-order logic and application to cryptographic protocols . In Proceedings of the 14th International Conference Rewriting Techniques and Applications (RTA'2003) (Valencia, Spain), R. Nieuwenhuis, Ed. Lecture Notes in Computer Science , vol. 2706 . Springer-Verlag, Berlin, Germany, 148--164.]] Comon-Lundh, H., and Cortier, V. 2003. New decidability results for fragments of first-order logic and application to cryptographic protocols. In Proceedings of the 14th International Conference Rewriting Techniques and Applications (RTA'2003) (Valencia, Spain), R. Nieuwenhuis, Ed. Lecture Notes in Computer Science, vol. 2706. Springer-Verlag, Berlin, Germany, 148--164.]]
Compton , K. J. , and Dexter , S . 1999. Proof techniques for cryptographic protocols. In Automata, Languages and Programming , 26th International Colloquium, ICALP'99 (Prague, Czech Republic), J. Wiedermann, P. van Emde Boas, and M. Nielsen, Eds. Lecture Notes in Computer Science , vol. 1644 . Springer-Verlag, Berlin, Germany, 25--39.]] Compton, K. J., and Dexter, S. 1999. Proof techniques for cryptographic protocols. In Automata, Languages and Programming, 26th International Colloquium, ICALP'99 (Prague, Czech Republic), J. Wiedermann, P. van Emde Boas, and M. Nielsen, Eds. Lecture Notes in Computer Science, vol. 1644. Springer-Verlag, Berlin, Germany, 25--39.]]
Debbabi , M. , Mejri , M. , Tawbi , N. , and Yahmadi , I . 1997. A new algorithm for the automatic verification of authentication protocols: From specifications to flaws and attack scenarios . In Proceedings of the DIMACS Workshop on Design and Formal Verification of Security Protocols . Rutgers University, New Jersey.]] Debbabi, M., Mejri, M., Tawbi, N., and Yahmadi, I. 1997. A new algorithm for the automatic verification of authentication protocols: From specifications to flaws and attack scenarios. In Proceedings of the DIMACS Workshop on Design and Formal Verification of Security Protocols. Rutgers University, New Jersey.]]
Denker , G. , Meseguer , J. , and Talcott , C . 1998. Protocol specification and analysis in Maude . In Proceedings of Workshop on Formal Methods and Security Protocols ( Indianapolis, Indiana), N. Heintze and J. Wing, Eds.]] Denker, G., Meseguer, J., and Talcott, C. 1998. Protocol specification and analysis in Maude. In Proceedings of Workshop on Formal Methods and Security Protocols (Indianapolis, Indiana), N. Heintze and J. Wing, Eds.]]
Denning , D. E. 1982. Cryptography and Data Security . Addison-Wesley , Reading, Mass .]] Denning, D. E. 1982. Cryptography and Data Security. Addison-Wesley, Reading, Mass.]]
Durante , A. , Focardi , R. , and Gorrieri , R . 1999. CVS: A compiler for the analysis of cryptographic protocols . In Proceedings of the 12th IEEE Computer Security Foundations Workshop (CSFW'99) . IEEE Computer Society, Los Alamitos, Calif., 203--212.]] Durante, A., Focardi, R., and Gorrieri, R. 1999. CVS: A compiler for the analysis of cryptographic protocols. In Proceedings of the 12th IEEE Computer Security Foundations Workshop (CSFW'99). IEEE Computer Society, Los Alamitos, Calif., 203--212.]]
Durgin , N. , Mitchell , J. , and Pavlovic , D . 2001. A compositional logic for protocol correctness . In Proceedings of the 14th IEEE Computer Security Foundations Workshop (CSFW-14) . IEEE Computer Society, Los Alamitos, Calif., 241--255.]] Durgin, N., Mitchell, J., and Pavlovic, D. 2001. A compositional logic for protocol correctness. In Proceedings of the 14th IEEE Computer Security Foundations Workshop (CSFW-14). IEEE Computer Society, Los Alamitos, Calif., 241--255.]]
Durgin N. A. and Mitchell J. C. 1999. Analysis of security protocols. In Calculational System Design M. Broy and R. Steinbruggen Eds. IOS Press Amsterdam The Netherlands 369--395.]] Durgin N. A. and Mitchell J. C. 1999. Analysis of security protocols. In Calculational System Design M. Broy and R. Steinbruggen Eds. IOS Press Amsterdam The Netherlands 369--395.]]
Gordon , A. , and Jeffrey , A . 2001. Authenticity by typing for security protocols . In Proceedings of the 14th IEEE Computer Security Foundations Workshop (CSFW-14) . IEEE Computer Society, Los Alamitos, Calif., 145--159.]] Gordon, A., and Jeffrey, A. 2001. Authenticity by typing for security protocols. In Proceedings of the 14th IEEE Computer Security Foundations Workshop (CSFW-14). IEEE Computer Society, Los Alamitos, Calif., 145--159.]]
Gordon , A. , and Jeffrey , A . 2002. Types and effects for asymmetric cryptographic protocols . In Proceedings of the 15th IEEE Computer Security Foundations Workshop (CSFW-15) . IEEE Computer Society, Los Alamitos, Calif., 77--91.]] Gordon, A., and Jeffrey, A. 2002. Types and effects for asymmetric cryptographic protocols. In Proceedings of the 15th IEEE Computer Security Foundations Workshop (CSFW-15). IEEE Computer Society, Los Alamitos, Calif., 77--91.]]
Goubault-Larrecq J. 2002. Protocoles cryptographiques: la logique à la rescousse! In Atelier SEcurité des Communications sur Internet (SECI'02) (Tunis Tunisie).]] Goubault-Larrecq J. 2002. Protocoles cryptographiques: la logique à la rescousse! In Atelier SEcurité des Communications sur Internet (SECI'02) (Tunis Tunisie).]]
Goubault-Larrecq , J. 2004. Une fois qu'on n'a pas trouvé de preuve, comment le faire comprendre à un assistant de preuve ? In Actes 15èmes journées francophones sur les langages applicatifs (JFLA'04) (Sainte-Marie-de-Ré , France). INRIA , Rocquencourt, France .]] Goubault-Larrecq, J. 2004. Une fois qu'on n'a pas trouvé de preuve, comment le faire comprendre à un assistant de preuve ? In Actes 15èmes journées francophones sur les langages applicatifs (JFLA'04) (Sainte-Marie-de-Ré, France). INRIA, Rocquencourt, France.]]
Goubault-Larrecq , J. , Roger , M. , and Verma , K. N . 2005 . Abstraction and resolution modulo AC: How to verify Diffie-Hellman-like protocols automatically. J. Logic Algeb. Prog. To appear.]] Goubault-Larrecq, J., Roger, M., and Verma, K. N. 2005. Abstraction and resolution modulo AC: How to verify Diffie-Hellman-like protocols automatically. J. Logic Algeb. Prog. To appear.]]
Hennessy , M. , and Riely , J . 2000. Information flow vs. resource access in the asynchronous pi-calculus . In Proceedings of the 27th International Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science. Springer-Verlag , Berlin, Germany, 415--427.]] Hennessy, M., and Riely, J. 2000. Information flow vs. resource access in the asynchronous pi-calculus. In Proceedings of the 27th International Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany, 415--427.]]
Lowe , G. 1996. Breaking and fixing the Needham-Schroeder public-key protocol using FDR . In Tools and Algorithms for the Construction and Analysis of Systems . Lecture Notes in Computer Science , vol. 1055 . Springer Verlag , Berlin, Germany , 147--166.]] Lowe, G. 1996. Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 1055. Springer Verlag, Berlin, Germany, 147--166.]]
Meadows , C. , and Narendran , P . 2002. A unification algorithm for the group Diffie-Hellman protocol . In Workshop on Issues in the Theory of Security (WITS'02) (Portland, Ore.).]] Meadows, C., and Narendran, P. 2002. A unification algorithm for the group Diffie-Hellman protocol. In Workshop on Issues in the Theory of Security (WITS'02) (Portland, Ore.).]]
Milner , R. 1999. Communicating and Mobile Systems: The Pi-Calculus . Cambridge University Press , Cambridge, United Kingdom.]] Milner, R. 1999. Communicating and Mobile Systems: The Pi-Calculus. Cambridge University Press, Cambridge, United Kingdom.]]
Selinger , P. 2001 . Models for an adversary-centric protocol logic . In Proceedings of the 1st Workshop on Logical Aspects of Cryptographic Protocol Verification ( Paris, France), J. Goubault-Larrecq, Ed. Electronic Notes in Theoretical Computer Science , vol. 55(1). Elsevier, Amsterdam, The Netherlands, 73-- 88 .]] Selinger, P. 2001. Models for an adversary-centric protocol logic. In Proceedings of the 1st Workshop on Logical Aspects of Cryptographic Protocol Verification (Paris, France), J. Goubault-Larrecq, Ed. Electronic Notes in Theoretical Computer Science, vol. 55(1). Elsevier, Amsterdam, The Netherlands, 73--88.]]
Sumii , E. , and Pierce , B. C . 2001. Logical relations and encryption (Extended abstract) . In Proceedings of the 14th IEEE Computer Security Foundations Workshop (CSFW-14) . IEEE Computer Society, Los Alamitos, Calif., 256--269.]] Sumii, E., and Pierce, B. C. 2001. Logical relations and encryption (Extended abstract). In Proceedings of the 14th IEEE Computer Security Foundations Workshop (CSFW-14). IEEE Computer Society, Los Alamitos, Calif., 256--269.]]