Translating ProScript to OCaml¶
Why build ProScript into OCaml?
There is OCaml documentation that describes how to use the ProScript-generated OCaml KBB2017 libraries. But in this documentation, we describe the machine translation of KBB2017 ProScript into OCaml, with some general pointers if you are using your own ProScript algorithm. So you can use the structure of this code for integrating ProScript into your own OCaml libraries. Read on.
- Integration Guide
Nadim Kobeissi, Karthikeyan Bhargavan, Bruno Blanchet. Automated Verification for Secure Messaging Protocols and Their Implementations: A Symbolic and Computational Approach. 2nd IEEE European Symposium on Security and Privacy , Apr 2017, Paris, France. pp.435 - 450, 2017, <https://www.ieee-security.org/TC/EuroSP2017/>. <10.1109/EuroSP.2017.38>. <hal-01575923>