StatVerif: Verification of stateful processes

What is StatVerif?

Eike Ritter and Mark Ryan

StatVerif is an automated verifier for security protocolswhich extends ProVerif with constructions which may used to model security protocols with global mutable state. In particular, the kind of security properties which may be verified is the same as ProVerif, and the syntax of StatVerif processes is an extension of the syntax for ProVerif processes with constructs for modelling states.

More details may be found in the paper introducing StatVerif.

Downloading and Installing StatVerif

The current version of StatVerif was finished in August 2017 and is based on ProVerif, version 1.97. A previous distribution of StatVerif had incorrect vrsions of the example input files. This version corrects thoses errors and also fixes a few bugs in the StatVerif code. It is available from the following sources:

  • via opam:
    If opam is installed, use the command
    opam install statverif
    to install StatVerif. This procedure works for Linux, MacOS and Windows.
  • as a package for Ubuntu 16.04:
    Download the package and install it with
    sudo apt-get install ocaml ocaml-findlib
    sudo dpkg -i statverif_1.97-1_amd64.deb
  • as a package for Fedora 26:
    Download the package and install it with
    sudo yum install ocaml ocaml-findlib
    sudo rpm -i statverif-1.97-1.x86_64.rpm
  • from sources on github:
    Download the sources via
    git clone https://github.com/rittere/statverif.git
    and follow the instructions in the README-file to build and install StatVerif.

Case Studies

A simple banking app

This hypothetical app makes it possible to read the bank balance via an authenticated channel. The protocol works as follows:

  • The app submits to the bank a new channel encrypted with the public key of the bank.
  • The bank then sends a nonce on this channel.
  • The app has a signing key which it uses to sign this nonce and send it back.
  • If the bank receives a valid signature, it uses the now authenticated channel to send the bank balance.
  • The bank uses state to store this channel together with the information whether the channel has been authenticated or not.

[StatVerif input]

A simple security device

This hypothetical security device is a piece of hardware that can be given pairs of secrets {(x, y)}k, encrypted with its public key k. The device decrypts each pair with its private key and returns either x or y, but not both. The device can be configured as left to return x, or right to return y, but can only be configured once.

The following example allows us to explain our results more fully. Consider a hardware device whose behaviour can be configured by the user. The device generates a public key k. A user Alice may use software to encrypt pairs (x, y) of secrets with k, resulting in {(x, y)}k. Later, she can hand the device and a set {{(x1, y1)}k, ..., {(xn, yn)}k} of such ciphertexts to another user Bob. The device allows Bob to configure it as "left" or "right". If Bob chooses to configure it as "left", then after doing so he can use the device to obtain the first components {x1, ..., xn} of the pairs. If he configures it with "right", then he gets to have the second components {y1 , ..., yn}. Such a device might, for example, be used to allow a customer to choose between vouchers for a music website, or vouchers for a social networking site, but not both.

[StatVerif input]

Contract signing protocol

A contract signing protocol allows a set of participants to sign a pre-agreed contract. A good contract signing protocol should not let a participant send their signature to another, without an assured means to obtain a signature from all the other participants. This property is called fairness.

Ensuring fairness requires a trusted party. Garay and Mackenzie proposed a contract signing protocol that, for efficiency, only involves the trusted party when a dispute needs to be resolved. This protocol is based on private contract signatures, which act as promises to sign the contract.

In the paper, our techniques are applied to the two-party instance of Garay and Mackenzie's protocol (GM), resulting in an automatic proof of fairness. To achieve this, no bound on the number of sessions, contracts or agents is needed. In comparison, when run with a plain ProVerif model of this protocol, using private channels to model the state of the trusted party, ProVerif reports a false attack. It reports the same false attack even if only one contract is considered.

The security of a protocol like this, with participants holding global mutable state, has been proved automatically only once before, by Mödersheim. Because his language is so low-level, his proof's hypotheses were very difficult to understand just by inspecting his model of the protocol. It isn't clear how many participants or contracts are considered.

Our translation only applies to processes with a finite number of cell names, i.e. with no cells s:= M under a replication. However, in the GM protocol, the trusted party creates two cell names for each contract. So for an unbounded number of contracts, the trusted party creates an unbounded number of cell names.

To use our technique to prove the GM protocol's fairness, we make the following correct abstraction:

The trusted party only follows the protocol for one contract, ct. Fairness of the protocol is proved only for ct.

For requests about ct, the trusted party will reply and update its memory according to the protocol. For requests about any other contract, it will reply as if it were the first time it received a request for that contract.

[StatVerif input]