The PROUVÉ Test Parser

This is an example application of the PROUVÉ Parser Library. This tool can be used to check the syntax and static semantics of protocol specifications files, as well as of security asssertions. Syntax and semantics of the PROUVÉ specification language and of the PROUVÉ assertion language are described in the PROUVÉ manual [Postscript] [PDF]. This tool, as well as the library providing the functionality, is written in Objective CAML (OCaml). To compile this library you need an OCaml compiler of version 3.07 or later, as well as the PROUVÉ Parser Library.
[PROUVÉ main page]