Cryptographic stack machine notation one
Автор: Prokopev S.E.
Журнал: Труды Института системного программирования РАН @trudy-isp-ran
Статья в выпуске: 3 т.30, 2018 года.
Бесплатный доступ
A worthy cryptographic protocol specification has to be human-readable (declarative and concise), executable and formally verified in a sound model. Keeping in mind these requirements, we present a protocol message definition notation named CMN.1, which is based on an abstraction named cryptographic stack machine. The paper presents the syntax and semantics of CMN.1 and the principles of implementation of the CMN.1-based executable protocol specification language. The core language library (the engine) performs all the message processing, whereas a specification should only provide the declarative definitions of the messages. If an outcoming message must be formed, the engine takes the CMN.1 definition as input and produces the binary data in consistency with it. When an incoming message is received, the engine verifies the binary data with respect to the given CMN.1 definition memorizing all the information needed in the further actions. The verification is complete: the engine decrypts the ciphertexts, checks the message authentication codes and signatures, etc. Currently, the author's proof-of-concept implementation of the language (embedded in Haskell) can translate a CMN.1-based specifications both to the interoperable implementations and to the programs for the ProVerif protocol analyzer. The excerpts from the CMN.1-based TLS protocol specification and corresponding automatically generated ProVerif program are provided as an illustration.
Cryptographic stack machine, cryptographic protocol message notation, executable cryptographic protocol specification languages, embedded domain-specific languages, haskell, proverif, tls
Короткий адрес: https://sciup.org/14916536
IDR: 14916536 | DOI: 10.15514/ISPRAS-2018-30(3)-12
Список литературы Cryptographic stack machine notation one
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- Concrete Syntax Notation One (CSN.1). Available at: http://csn1.info, accepted 10.06.2018.
- Transfer Syntax Notation One (TSN.1). Available at: http://www.protomatics.com/tsn1. Html, accessed 10.06.2018.
- The BinPAC language. Available at: https://www.bro.org/sphinx/components/binpac/README.html, accessed 10.06.2018.
- Mario Baldi, Fulvio Risso. NetPDL: An Extensible XML-Based Language for Packet Header Description. Computer Networks, vol, 50, issue 5, 2006, pp. 688-706.
