Нотация криптографической стековой машины версии один
https://doi.org/10.15514/ISPRAS-2018-30(3)-12
Аннотация
Список литературы
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