Preview

Труды Института системного программирования РАН

Расширенный поиск

Оптимизация программ на ProVerif для криптографических протоколов выработки общего ключа

https://doi.org/10.15514/ISPRAS-2021-33(5)-6

Полный текст:

Аннотация

Криптографические протоколы используются для установления безопасного соединения между “честными” агентами, которые общаются строго в соответствии с правилами протокола. Для того, чтобы убедиться, что спроектированный криптографический протокол является криптографически стойким, обычно используются различные программные инструменты. Однако, адекватная спецификация криптографического протокола обычно представляется в виде набора требований к последовательностям передаваемых сообщений, включая формат таких сообщений. Выполнение всех этих требований приводит к тому, что формальная спецификация для реального криптографического протокола становится громоздкой, в следствии чего её трудно анализировать формальными методами. Одним из таких стремительно развивающихся инструментов для формальной верификации криптографических протоколов является ProVerif. Отличительной особенностью инструмента ProVerif является то, что при больших протоколах он часто не справляется с их анализом, т.е. не может ни доказать безопасность протокола, ни опровергнуть её. В таких случаях прибегают либо к апроксимации задачи, либо к эквивалентным преобразованиям модели программы на языке ProVerif, упрощающих ProVerif-модель. В этой статье мы предлагаем способ для упрощения ProVerif-спецификаций для AKE-протоколов, использующих схему шифрования Эль-Гамаля. А именно, мы предлагаем эквивалентные преобразования, позволяющие построить ProVerif-спецификацию, которая упрощает анализ спецификации для инструмента ProVerif. Экспериментальные результаты для криптопротоколов Нидхема-Шрёдера и Yahalom показывают, что такой подход может быть перспективным для автоматической проверки реальных протоколов.

Об авторах

Евгений Максимович ВИНАРСКИЙ
Институт системного программирования им. В.П. Иванникова РАН, Национальный исследовательский университет «Высшая школа экономики»
Россия

Аспирант факультета ФКН ВШЭ, старший лаборант ИСП РАН



Алексей Васильевич ДЕМАКОВ
Институт системного программирования им. В.П. Иванникова РАН
Россия

Кандидат физико-математических наук, ведущий научный сотрудник



Список литературы

1. B. Blanchet. Symbolic and Computational Mechanized Verification of the ARINC823 Avionic Protocols. In Proc. of the 30th IEEE Computer Security Foundations Symposium (CSF'17), 2017, pp. 68-82.

2. K. Bhargavan, B. Blanchet, and N. Kobeissi. Verified models and reference implementations for the TLS 1.3 standard candidate. Research Report RR-9040, Inria, 2017.

3. K. Bhargavan, B. Blanchet, and N. Kobeissi. Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate. In Proc. of the IEEE Symposium on Security and Privacy (S&P'17), pp. 483-503.

4. S. Meier, B. Schmidt et al. The TAMARIN prover for the symbolic analysis of security protocols. In Proc. of the 25th International Conference on Computer Aided Verification, 2013. pp. 696-701.

5. S. Meier. Advancing automated security protocol verification. Doctoral Thesis. ETH Zurich, 2013, 214 p.

6. B. Schmidt. Formal analysis of key exchange protocols and physical protocols. Doctoral Thesis. ETH Zurich, 2012, 199 p.

7. B. Blanchet. Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif. Foundations and Trends in Privacy and Security, vol. 1, no. 1-2, 2016, pp 1-135.

8. B. Blanchet. Automatic Verification of Correspondences for Security Protocols. Journal of Computer Security, vol. 17, issue 4, 2009, pp 363-434.

9. B. Blanchet. Automatic Verification of Security Protocols in the Symbolic Model: the Verifier ProVerif. Lecture Notes in Computer Science, vol. 8604, 2012, pp. 54-87.

10. B. Blanchet. CryptoVerif: A Computationally Sound Mechanized Prover for Cryptographic Protocols. In Proc. of the Dagstuhl Seminar on Formal Protocol Verification Applied, 2007.

11. T. Elgamal. A Public-Key Cryptosystem and a Signature Scheme Based on Discrete Logarithms. IEEE Transactions on Information Theory, vol. 31, no. 4, 1985, pp. 469-472, 1985.

12. E. Vinarskii. URL: https://github.com/vinevg1996/proverif_code_optimisation, accessed 24.10.2021.


Рецензия

Для цитирования:


ВИНАРСКИЙ Е.М., ДЕМАКОВ А.В. Оптимизация программ на ProVerif для криптографических протоколов выработки общего ключа. Труды Института системного программирования РАН. 2021;33(5):105-116. https://doi.org/10.15514/ISPRAS-2021-33(5)-6

For citation:


VINARSKII E.M., DEMAKOV A.V. Optimization of ProVerif programs for AKE-protocols. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2021;33(5):105-116. (In Russ.) https://doi.org/10.15514/ISPRAS-2021-33(5)-6

Просмотров: 74


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 2079-8156 (Print)
ISSN 2220-6426 (Online)