The PROUVÉ Parsing Library

This library provides the functionality needed to parse protocol specifications files, as well as security asssertions. Syntax and semantics of the PROUVÉ specification language and of the PROUVÉ assertion language are described in the PROUVÉ manual [Postscript] [PDF]. The library is written in Objective CAML (OCaml). To compile this library you need an OCaml compiler of version 3.07 or later.
[PROUVÉ main page]