VSCode ProVerif Language Service

Visual Studio Code extension for ProVerif files (.pv, .pvl, .pcv).

Functionality:

• Highlights the first syntax errors ProVerif finds with the corresponding error. For libraries, see below.
• Press CTRL and click on an identifier to navigate to its definition. This feature is sill experimental, so do not fully trust it.
• Press CTRL+SHIFT+B to execute ProVerif over the currently opened file.
• Configure the proverif bin in the settings, else it is taken from the $PATH.

Use in combination with https://github.com/georgio/proverif-vscode to get syntax highlighting.

Libraries (.pvl)

If your .pv or .pvl file depends on libraries, include a corresponding comment (* -lib {library_path}.pvl *):

(* -lib types.pvl *)

fun senc(bitstring, key): bitstring.
reduc forall m: bitstring, k: key; sdec(senc(m,k),k) = m.