Preview

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

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

Нотация криптографической стековой машины версии один

https://doi.org/10.15514/ISPRAS-2018-30(3)-12

Аннотация

Хорошая спецификация криптографического протокола должна легко восприниматься человеком (быть декларативной и лаконичной), быть исполнимой и пройти процедуру формальной верификации в некоторой адекватной модели. Нацеливаясь на эти требования, в статье предложена нотация CMN.1, предназначенная для описания сообщений криптографических протоколов и основанная на вычислительной абстракции под названием криптографическая стековая машина (CSM). Статья описывает синтаксис и семантику CMN.1, а также представляет результаты разработки языка спецификаций криптографических протоколов, построенного на основе данной нотации и встроенного в язык Haskell. В авторской реализации вся обработка сообщений инкапсулирована внутри базового библиотечного модуля, в то время как спецификация должна лишь дать декларативные определения этих сообщений. При формировании исходящего сообщения протокола базовый модуль берет описание данного сообщения в нотации CMN.1 и возвращает фрагмент данных, сгенерированный по этому описанию. При обработке входящего сообщения базовый модуль берет поступивший фрагмент данных и описание ожидаемого сообщения в нотации CMN.1 и возвращает вердикт об их соответствии друг другу, извлекая и запоминая при этом все содержащиеся в сообщении данные, необходимые для формирования или верификации следующих сообщений протокола. Процесс верификации является полным: базовый модуль осуществляет расшифрование, проверку кодов аутентификации сообщений и значений цифровой подписи и т.д. Текущая реализация языка включает функции трансляции спецификаций в исполняемый код, совместимый с существующими программными реализациями протоколов, а также функции конвертации спецификаций в программы на входном языке анализатора протоколов ProVerif. В качестве иллюстрации приводятся выдержки из CMN.1-спецификации протокола TLS и соответствующей ей автоматически сгенерированной программы для ProVerif.

Об авторе

С. Е. Прокопьев
Независимый исследователь
Россия


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

1. S. Chaki and A. Datta. Aspier: An automated framework for verifying security protocol implementations. In Proceedings of the Computer Security Foundations Workshop, 2009, pp. 172-185.

2. J. Goubault-Larrecq and F. Parrennes. Cryptographic protocol analysis on real C code. In Proceedings of the 6th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI’05), Lecture Notes in Computer Science, vol. 3385, 2005, pp. 363-379.

3. Mihhail Aizatulin, Andrew D. Gordon, and Jan 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.

4. Nicholas O’Shea. Using Elyjah to analyse Java implementations of cryptographic protocols. In Proc. of the Joint Workshop on Foundations of Computer Security, Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security (FCS-ARSPA-WITS’08), 2008.

5. Karthikeyan Bhargavan, Cedric Fournet, Andrew Gordon, and Stephen Tse. Verified interoperable implementations of security protocols. ACM Transactions on Programming Languages and Systems (TOPLAS), vol. 31, no. 1, 2008.

6. Karthikeyan Bhargavan, Bruno Blanchet, and Nadim Kobeissi. Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate. In Proc. of the IEEE Symposium on Security and Privacy, 2017.

7. Matteo Avalle, Alfredo Pironti, Riccardo Sisto, and Davide Pozza. The JavaSPI framework for security protocol implementation. In Proc. of the 6th International Conference on Availability, Reliability and Security (ARES’11), 2011, pp. 746-751.

8. David Cade, Bruno Blanchet. From Computationally-Proved Protocol Specifications to Implementations and Application to SSH. Available at: http://prosecco.gforge.inria.fr/personal/dcade/CadeBlanchetJoWUA13.pdf, accessed 10.06.2018.

9. A. Delignat-Lavaud et al. Implementing and Proving the TLS 1.3 Record Layer. In Proc. of the 2017 IEEE Symposium on Security and Privacy (SP), 2017, pp. 463-482.

10. Bruno Blanchet. Automatic Verification of Security Protocols in the Symbolic Model: the Verifier ProVerif. In Foundations of Security Analysis and Design VII, FOSAD Tutorial Lectures, Lecture Notes in Computer Science, vol. 8604, 2014, pp. 54-87.

11. Cas Cremers, Marko Horvat, Jonathan Hoyland, Sam Scott, and Thyla van der Merwe. 2017. Source files and annotated RFC for TLS 1.3 analysis. (2017). Available at: https://tls13tamarin.github.io/TLS13Tamarin/, accessed 10.06.2018.

12. Concrete Syntax Notation One (CSN.1). Available at: http://csn1.info, accepted 10.06.2018.

13. Transfer Syntax Notation One (TSN.1). Available at: http://www.protomatics.com/tsn1. Html, accessed 10.06.2018.

14. The BinPAC language. Available at: https://www.bro.org/sphinx/components/binpac/ README.html, accessed 10.06.2018.

15. Mario Baldi, Fulvio Risso. NetPDL: An Extensible XML-Based Language for Packet Header Description. Computer Networks, vol, 50, issue 5, 2006, pp. 688-706.


Рецензия

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


Прокопьев С.Е. Нотация криптографической стековой машины версии один. Труды Института системного программирования РАН. 2018;30(3):165-182. https://doi.org/10.15514/ISPRAS-2018-30(3)-12

For citation:


Prokopev S.E. Cryptographic Stack Machine Notation One. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2018;30(3):165-182. https://doi.org/10.15514/ISPRAS-2018-30(3)-12



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


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