StatVerif: Verification of stateful processes

We extend the ProVerif process calculus with constructs for explicit state, in order to be able to reason about protocols that manipulate global state. Global state is required by protocols used in hardware devices (such as smart cards and the TPM), as well as by protocols involving databases that store persistent information. We provide the operational semantics of our language. We extend the ProVerif compiler that takes processes written in the process language, and produces Horn clauses. Our translation is carefully engineered to avoid many false attacks. We prove the correctness of the extended compiler. We illustrate our method on two examples: a small hardware security device, and a contract signing protocol. We are able to prove their desired properties automatically.

1. 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.

2. 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 [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:

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.