Формальный язык первичных спецификаций криптографических протоколов
https://doi.org/10.15514/ISPRAS-2021-33(5)-7
Аннотация
Применение формальных методов в разработке реализаций сетевых протоколов способствует повышению качества этих реализаций. Наибольший эффект даст изложение на формальном языке первичных спецификаций протоколов, публикуемых в документах RFC. В статье предлагается формальный язык описания криптографических протоколов, нацеленный на более полное, по сравнению с существующими языками первичных спецификаций, выполнение следующих требований: лаконичность, декларативность, выразительность, однозначность, исполнимость, возможность автоматического извлечения из спецификаций наборов тестов высокого качества. Основа языка – вычислитель, специально разработанный для предметной области криптографических протоколов, – т. н. C2-машина. В статье при изложении принципов построения и функционирования C2-машины используется метод последовательного уточнения модели: сначала вводится недетерминированный автомат, на котором в наиболее общем виде задается операционный контракт протокола, затем вводится машина C0, на которой демонстрируется предлагаемый подход к специфицированию недетерминизма протоколов, и далее – машина C1, на которой в формализованном виде задается семантика базовых инструкций C2-машины. Статья иллюстрирована примерами для протокола TLS.
При поддержке: Исследование поддержано грантом Минобрнауки России № 075-15-2020-788
Об авторе
Сергей Евгеньевич ПРОКОПЬЕВ
Институт системного программирования им. В.П. Иванникова РАН, АО НПК «Криптонит»
Россия
Россия
Кандидат технических наук, старший научный сотрудник отдела технологий программирования ИСП РАН, руководитель направления сетевых протоколов безопасности лаборатории сетевой и информационной безопасности АО НПК «Криптонит»
Список литературы
1. А.В. Никешин, Н.В. Пакулин, В.З. Шнитман. Тестирование реализаций клиента протокола TLS. Труды ИСП РАН, том 27, вып.2, 2015 г., стр. 145-160 / A. V. Nikeshin, N. V. Pakulin, V. Z. Shnitman. TLS clients testing. Trudy ISP RAN/Proc. ISP RAS, vol. 27, issue 2, 2015, pp. 145-160 (in Russian), DOI: 10.15514/ISPRAS-2015-27(2)-9.
2. K. Bhargavan, A. Delignat-Lavaud et al. Implementing and Proving the TLS 1.3 Record Layer. In Proc. of the 38th IEEE Symposium on Security and Privacy, 2017, pp.463-482.
3. J. Goubault-Larrecq and F. Parrenne. Cryptographic protocol analysis on real C code. Lecture Notes in Computer Science, vol. 3385, 2005, pp. 363-79.
4. J. Bozic, L. Marsso et al. A formal TLS handshake model in LNT. In Proc. of the Third Workshop on Models for Formal Analysis of Real Systems and Sixth International Workshop on Verification and Program Transformation, 2018, pp. 1-40.
5. K. Bhargavan, B. Blanchet, N. Kobeissi. Verified models and reference implementations for the TLS 1.3 standard candidate. In Proc. of the IEEE Symposium on Security and Privacy; 2017, pp.483-502.
6. J. Zhang, L. Yang et al. Formal analysis of 5G EAP-TLS authentication protocol using ProVerif. IEEE Access, vol. 8, 2020, pp. 23674-23688.
7. M. Backes, A. Busenius, C. Hriţcu. On the Development and Formalization of an Extensible Code Generator for Real Life Security Protocols. Lecture Notes in Computer Science, vol. 7226, 2-12, pp. 371-387.
8. M. Aizatulin, A. Gordon, J. Jurjens. Extracting and verifying cryptographic models from C protocol code by symbolic execution. In Proc. of the 18th ACM Conference on Computer and Communications Security (CCS’11), 2011, pp. 331-340.
9. P. Arcaini, A. Gargantini, E. Riccobene. AsmetaSMV: a way to link high-level ASM models to low-level NuSMV specifications. Lecture Notes in Computer Science, vol. 5977, 2010, pp. 61-74.
10. J. Jürjens. Automated Security Verification for Crypto Protocol Implementations: Verifying the Jessie Project. Electronic Notes in Theoretical Computer Science, vol. 250, issue 1, 2009, pp. 123-136.
11. I. Abdullah, D. Menascé. Protocol Specification and Automatic Implementation Using XML and CBSE. In Proc. of the International Conference on Communications, Internet and Information Technology. (CIIT2003), 2003, pp. 1-7.
12. E.W. Dijkstra. Guarded commands, non-determinacy and a calculus for the derivation of programs. Communications of the ACM, vol. 18, issue 8, 1975, pp. 453-457.
13. K.L. McMillan and L.D. Zuck. Formal specification and testing of QUIC. In Proc. of ACM Special Interest Group on Data Communication (SIGCOMM’19), 2019, 14 p.
14. D. Rozenzweig, D. Runje. The Cryptographic Abstract Machine. Lecture Notes in Computer Science, vol. 3052, 2004, pp. 202-217.
15. M. Veanes, C. Campbell et al. Model-Based Testing of Object-Oriented Reactive Systems with Spec Explorer. Lecture Notes in Computer Science, 2008, vol. 4949, pp. 39-76.
16. E. Gagliardi, O. Levillain. Analysis of QUIC session establishment and its implementations. In Proc. of the IFIP International Conference on Information Security Theory and Practice, 2019, pp.169-184.
17. A. Gargantini, E. Riccobene. ASM-based Testing: Coverage Criteria and Automatic Test Sequence Generation. Journal of Universal Computer Science, vol. 7, no. 11, 2001, pp. 1050-1067.
18. Y. Gurevich. Sequential Abstract State Machines Capture Sequential Algorithms. ACM Transactions on Computational Logic, vol. 1, issue 1, 2000, pp. 77-111.
19. D. Angluin. Learning Regular Sets from Queries and Counterexamples. Information and Computation, vol. 75, issue 2, 1987, pp. 87-106.
Рецензия
Для цитирования:
ПРОКОПЬЕВ С.Е. Формальный язык первичных спецификаций криптографических протоколов. Труды Института системного программирования РАН. 2021;33(5):117-136. https://doi.org/10.15514/ISPRAS-2021-33(5)-7
For citation:
PROKOPEV S.E. A formal language for primary specifications of the cryptographic protocols. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2021;33(5):117-136. (In Russ.) https://doi.org/10.15514/ISPRAS-2021-33(5)-7
Послать статью по эл. почте 