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

Криптографические протоколы используются для установления безопасного соединения между “честными” агентами, которые общаются строго в соответствии с правилами протокола. Для того, чтобы убедиться, что спроектированный криптографический протокол является криптографически стойким, обычно используются различные программные инструменты. Однако, адекватная спецификация криптографического протокола обычно представляется в виде набора требований к последовательностям передаваемых сообщений, включая формат таких сообщений. Выполнение всех этих требований приводит к тому, что формальная спецификация для реального криптографического протокола становится громоздкой, в следствии чего её трудно анализировать формальными методами. Одним из таких стремительно развивающихся инструментов для формальной верификации криптографических протоколов является 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.