Верификация протоколов безопасности на основе комбинированного использования существующих методов и средств
Ключевые слова:
протоколы безопасности, формальные методы, верификация, проверка на модели, доказательство теоремАннотация
В настоящей статье анализируются существующие подходы к верификации протоколов безопасности и демонстрируется невозможность полноценной верификации протоколов безопасности в рамках только одного из подходов. Для решения данной задачи предлагается комбинированный подход к верификации, основанный на объединении сильных сторон существующих методов и средств.Литература
Десницкий В. А., Котенко И. В., Резник С. А. Разработка и верификация протокола обмена сообщениями для защиты программ на основе механизма удаленного доверия” // Защита информации. Инсайд. 2008. № 4. С. 59–63; № 5, 2008. С. 68–74.
Котенко И. В., Десницкий В. А. Аспектно-ориентированный подход к реализации мобильного модуля в модели защиты, основанной на механизме удаленного доверия” // Информационные технологии и вычислительные системы. 2008. № 5.
Косачев А. С., Пономаренко В. Н. Анализ подходов к верификации функций безопасности и мобильности. М.: Триумф, 2004. 101 с.
Abadi M., Blanchet B., Fournet C. Just Fast Keying in the Pi Calculus // ACM Transactions on Information and System Security. TISSEC. July 2007. Vol. 10, № 3. P. 1–59.
Bella G. Inductive Verification of Cryptographic Protocols. PhD Thesis, University of Cambridge, 2000. 189 p.
Blanchet B. An Efficient Cryptographic Protocol Verifier Based on Prolog Rules // Proc. of 14th IEEE Computer Security Foundations Workshop (CSFW–14). Cape Breton, Nova Scotia, Canada, IEEE Computer Society, June 2001. P. 82–96.
Basin D., Mödersheim S., Viganò L. An On-The-Fly Model-Checker for Security Protocol Analysis // Proc. of ESORICS'03, Lecture Notes in Computer Science. 2003. Vol. 2808. P. 253–270.
Bella G., Paulson L. C. Using Isabelle to Prove Properties of the Kerberos Authentication System // Proc. of DIMACS Workshop on Design and Formal Verification of Security Protocols, 1997.11p.
Clark J., Jacob J. A Survey of Authentication Protocol Literature: Version 1. 0. http://www.cs.york.ac.uk/jac/papers/drareview.ps.gz, 1997. 109 p.
Compagna L. SAT-based Model-Checking of Security Protocols. PhD Thesis, Universitа degli Studi di Genova and the University of Edinburgh, September 2005. 216 p.
Cremers C. J. F. Unbounded Verification, Falsification, and Characterization of Security Protocols by Pattern Refinement // Proc. of the 15th ACM conference on Computer and communications security, 2008. P. 119–128.
Durgin N., Lincoln P., Mitchell J., Scedrov A. Undecidability of bounced security protocols // Proc. of the FLOC’99 Workshop on Formal Methods and Security Protocols (FMSP’99), 1999.
Denker G., Millen J. CAPSL integrated protocol environment // Proc. of DARPA Information Survivability Conference, DISCEX 2000. IEEE Computer Society, 2000. P. 207–221.
Gritzalis S., Spinellis D., Georgiadis P. Security protocols over open networks and distributed systems: Formal methods for their analysis, design, and verification // Computer Communications. May 1999. Vol. 22, № 8. P. 695–707.
Hoare C. A. R. Communicating sequential processes // Communications of the ACM, 1978. Vol. 21, № 8. P. 666–677.
Josang A. Security Protocol Verification Using SPIN // Proc. of SPIN'95 Workshop, 1995. 9 p.
Lowe G. An attack on the Needham-Schroeder public key authentication protocol // Information Processing Letters, November 1995. Vol. 56, № 3. P. 131–136.
Lowe G. Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR Tools and Algorithms for Construction and Analysis of Systems // Proc. of the Second International Workshop, TACAS 96, Passau, Germany, March 27–29, 1996. Lecture Notes in Computer Science. 1996. Vol. 1055. P. 147–166.
Lowe G. Casper: A Compiler for the Analysis of Security Protocols // J. of Computer Security. 1998. Vol. 6, № 1–2. P. 53–84.
Meadows C. Formal Verification of Cryptographic Protocols: A Survey // Proc. of ASIACRYPT. 1994. P. 135–150.
Meadows C. Formal methods for cryptographic protocol analysis: emerging issues and trends // IEEE J. on Selected Areas in Communications. January 2003. Vol. 21, Issue 1. P. 44–54.
Mitchell J. C., Mitchell M., Stern U. Automated analysis of cryptographic protocols using Murphi // IEEE Symposium on Security and Privacy, 1997. P. 141–151.
Millen J., Shmatikov V. Constraint Solving for Bounded-Process Cryptographic Protocol Analysis // Proc. of the ACM Conference on Computer and Communications Security, 2001. P. 166–175.
Mitchell J. C., Shmatikov V., Stern U. Finite-State Analysis of SSL 3. 0 // 7th USENIX Security Symposium, 1998. 15 p.
Nieh B. and Tavares S. Modeling and analyzing cryptographic protocols using Petri nets. // Proc. of the Workshop on the Theory and Application of Cryptographic Techniques: Advances in Cryptology, 1992. Vol. 718. P. 275–295.
Norman G., Shmatikov V. Analysis of Probabilistic Contract Signing // J. of Computer Security, 2006, Volume 14 , Issue 6. P. 561–589.
Oehl F., Cece G., Kouchnarenko O., Sinclair D. Automatic Approximation for the Verication of Cryptographic Protocols // Proc. of the International Conference on Formal Aspects of Security (FASec), London, UK. Lecture Notes in Computer Science. November 2003. Vol. 2629. P. 33–48.
Paulson L. C. The foundation of a generic theorem prover // J. of Automated Reasoning, September 1989. Vol. 5, Issue 3. P. 363–397.
Rusinowitch M. Automated Analysis of Security Protocols // Proc. of the 12th Intern. Workshop on Functional and (Constraint) Logic Programming (WFLP'03). Electronic Notes in Theoretical Computer Science. 2003. Vol. 86, № 3. 4 p.
Shmatikov V. Probabilistic Model Checking of an Anonymity System // J. of Computer Security, 2004. Vol. 12, № 3. P. 355–377.
Viganò L. Automated Security Protocol Analysis with the AVISPA Tool // Proc. of the XXI Mathematical Foundations of Programming Semantics (MFPS'05), ENTCS, Elsevier, 2005. № 155. P. 61–86.
Десницкий В. А., Котенко И. В. Защита программного обеспечения на основе механизма удаленного доверия” // Изв. вузов. Приборостроение, Т. 51, № 11. 2008, С. 26–30.
Котенко И. В., Десницкий В. А. Аспектно-ориентированный подход к реализации мобильного модуля в модели защиты, основанной на механизме удаленного доверия” // Информационные технологии и вычислительные системы. 2008. № 5.
Косачев А. С., Пономаренко В. Н. Анализ подходов к верификации функций безопасности и мобильности. М.: Триумф, 2004. 101 с.
Abadi M., Blanchet B., Fournet C. Just Fast Keying in the Pi Calculus // ACM Transactions on Information and System Security. TISSEC. July 2007. Vol. 10, № 3. P. 1–59.
Bella G. Inductive Verification of Cryptographic Protocols. PhD Thesis, University of Cambridge, 2000. 189 p.
Blanchet B. An Efficient Cryptographic Protocol Verifier Based on Prolog Rules // Proc. of 14th IEEE Computer Security Foundations Workshop (CSFW–14). Cape Breton, Nova Scotia, Canada, IEEE Computer Society, June 2001. P. 82–96.
Basin D., Mödersheim S., Viganò L. An On-The-Fly Model-Checker for Security Protocol Analysis // Proc. of ESORICS'03, Lecture Notes in Computer Science. 2003. Vol. 2808. P. 253–270.
Bella G., Paulson L. C. Using Isabelle to Prove Properties of the Kerberos Authentication System // Proc. of DIMACS Workshop on Design and Formal Verification of Security Protocols, 1997.11p.
Clark J., Jacob J. A Survey of Authentication Protocol Literature: Version 1. 0. http://www.cs.york.ac.uk/jac/papers/drareview.ps.gz, 1997. 109 p.
Compagna L. SAT-based Model-Checking of Security Protocols. PhD Thesis, Universitа degli Studi di Genova and the University of Edinburgh, September 2005. 216 p.
Cremers C. J. F. Unbounded Verification, Falsification, and Characterization of Security Protocols by Pattern Refinement // Proc. of the 15th ACM conference on Computer and communications security, 2008. P. 119–128.
Durgin N., Lincoln P., Mitchell J., Scedrov A. Undecidability of bounced security protocols // Proc. of the FLOC’99 Workshop on Formal Methods and Security Protocols (FMSP’99), 1999.
Denker G., Millen J. CAPSL integrated protocol environment // Proc. of DARPA Information Survivability Conference, DISCEX 2000. IEEE Computer Society, 2000. P. 207–221.
Gritzalis S., Spinellis D., Georgiadis P. Security protocols over open networks and distributed systems: Formal methods for their analysis, design, and verification // Computer Communications. May 1999. Vol. 22, № 8. P. 695–707.
Hoare C. A. R. Communicating sequential processes // Communications of the ACM, 1978. Vol. 21, № 8. P. 666–677.
Josang A. Security Protocol Verification Using SPIN // Proc. of SPIN'95 Workshop, 1995. 9 p.
Lowe G. An attack on the Needham-Schroeder public key authentication protocol // Information Processing Letters, November 1995. Vol. 56, № 3. P. 131–136.
Lowe G. Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR Tools and Algorithms for Construction and Analysis of Systems // Proc. of the Second International Workshop, TACAS 96, Passau, Germany, March 27–29, 1996. Lecture Notes in Computer Science. 1996. Vol. 1055. P. 147–166.
Lowe G. Casper: A Compiler for the Analysis of Security Protocols // J. of Computer Security. 1998. Vol. 6, № 1–2. P. 53–84.
Meadows C. Formal Verification of Cryptographic Protocols: A Survey // Proc. of ASIACRYPT. 1994. P. 135–150.
Meadows C. Formal methods for cryptographic protocol analysis: emerging issues and trends // IEEE J. on Selected Areas in Communications. January 2003. Vol. 21, Issue 1. P. 44–54.
Mitchell J. C., Mitchell M., Stern U. Automated analysis of cryptographic protocols using Murphi // IEEE Symposium on Security and Privacy, 1997. P. 141–151.
Millen J., Shmatikov V. Constraint Solving for Bounded-Process Cryptographic Protocol Analysis // Proc. of the ACM Conference on Computer and Communications Security, 2001. P. 166–175.
Mitchell J. C., Shmatikov V., Stern U. Finite-State Analysis of SSL 3. 0 // 7th USENIX Security Symposium, 1998. 15 p.
Nieh B. and Tavares S. Modeling and analyzing cryptographic protocols using Petri nets. // Proc. of the Workshop on the Theory and Application of Cryptographic Techniques: Advances in Cryptology, 1992. Vol. 718. P. 275–295.
Norman G., Shmatikov V. Analysis of Probabilistic Contract Signing // J. of Computer Security, 2006, Volume 14 , Issue 6. P. 561–589.
Oehl F., Cece G., Kouchnarenko O., Sinclair D. Automatic Approximation for the Verication of Cryptographic Protocols // Proc. of the International Conference on Formal Aspects of Security (FASec), London, UK. Lecture Notes in Computer Science. November 2003. Vol. 2629. P. 33–48.
Paulson L. C. The foundation of a generic theorem prover // J. of Automated Reasoning, September 1989. Vol. 5, Issue 3. P. 363–397.
Rusinowitch M. Automated Analysis of Security Protocols // Proc. of the 12th Intern. Workshop on Functional and (Constraint) Logic Programming (WFLP'03). Electronic Notes in Theoretical Computer Science. 2003. Vol. 86, № 3. 4 p.
Shmatikov V. Probabilistic Model Checking of an Anonymity System // J. of Computer Security, 2004. Vol. 12, № 3. P. 355–377.
Viganò L. Automated Security Protocol Analysis with the AVISPA Tool // Proc. of the XXI Mathematical Foundations of Programming Semantics (MFPS'05), ENTCS, Elsevier, 2005. № 155. P. 61–86.
Десницкий В. А., Котенко И. В. Защита программного обеспечения на основе механизма удаленного доверия” // Изв. вузов. Приборостроение, Т. 51, № 11. 2008, С. 26–30.
Опубликован
2009-03-01
Как цитировать
Котенко, И. В., Резник, С. А., & Шоров, А. В. (2009). Верификация протоколов безопасности на основе комбинированного использования существующих методов и средств. Труды СПИИРАН, (8), 292-310. https://doi.org/10.15622/sp.8.14
Выпуск
Раздел
Статьи
Авторы, которые публикуются в данном журнале, соглашаются со следующими условиями:
Авторы сохраняют за собой авторские права на работу и передают журналу право первой публикации вместе с работой, одновременно лицензируя ее на условиях Creative Commons Attribution License, которая позволяет другим распространять данную работу с обязательным указанием авторства данной работы и ссылкой на оригинальную публикацию в этом журнале.
Авторы сохраняют право заключать отдельные, дополнительные контрактные соглашения на неэксклюзивное распространение версии работы, опубликованной этим журналом (например, разместить ее в университетском хранилище или опубликовать ее в книге), со ссылкой на оригинальную публикацию в этом журнале.
Авторам разрешается размещать их работу в сети Интернет (например, в университетском хранилище или на их персональном веб-сайте) до и во время процесса рассмотрения ее данным журналом, так как это может привести к продуктивному обсуждению, а также к большему количеству ссылок на данную опубликованную работу (Смотри The Effect of Open Access).
