About This Tutorial
This tutorial is extracted from Squirell repository file squirrel-prover/examples/tutorial.sp
If you have installed Squirrel along with Proof General (cf. readme), you can also open this file with emacs and all code blocks provided bellow will be executable.
Messages exchanged by a protocol are modelled using terms.
Concretely, a message is either
- a name
nused to model a random sampling;
- the application of a function
In Squirrel, a function symbol without any assumption can be defined with:
abstract ok : message abstract ko : message abstract f1 : message -> message abstract f2 : message -> message -> message.
ko are constants, and
f1 is a function that expects a message, and then return a message.
f2 is then a function symbol of arity two, and function symbols of any arity can be defined this way.
n allows to model secret keys, or some random challenge. As we wish to be able to refer to an unbounded number of session, we allow names to be indexed, each value of the index yielding a fresh independent random. We denote by
n[i] an indexed name, with variable
i as an index. Names can be indexed by any number of indices.
In the tool, one can declare names and indexed names with the following.
name n : message name n1 : index -> message name n2 : index -> index -> message.
To model a setting where multiple people each have their own secret key, one could declare an indexed name as follows.
name key : index -> message.
Symbol functions can be defined as being an encryption, or a hash function, or a signature, or… The tool will then assume that such functions satisfy some classical cryptographic assumptions.
The possible sorts and corresponding assumptions are:
- encryption, CCA1 & INT-CTXT, symmetric and asymmetric
- signatures, EUF-CMA
- hash functions, PRF, and thus EUF-CMA, CR
Each are declared in the following way.
signature sign,checksign,pk hash h senc enc,dec aenc asenc,asdec,aspk.
Protocols are described inside a pi-calculus. It is based on the following constructs:
new nid used to instantiate a fresh name;
out(c,m)is used to send the term
mover the channel
in(c,x)is used to receive some value from channel
c, bound to the variable
act; Pcorrespond to the sequential composition of action
P; … TODO
As an example, we use a small RFID based protocol, with a tag and a reader, called the basic hash protocol:
- Mayla Brusò, Kostas Chatzikokolakis, and Jerry den Hartog. Formal Verification of Privacy for RFID Systems. pages 75–88, July 2010.
T --> R : <nT, h(nT,kT)> R --> T : ok
We first declare the channels used by the protocol. Remark that channels are mostly byproducts of the theory, and do not play a big role.
channel cT channel cR.
We then define a first process of a protocol, which may correspond to multiple identies, and thus depend on some index variable
process tag(i:index) = new nT; out(cT, <nT, h(nT,key(i))>). T :
We can then declare the reader.
process reader(j:index) = in(cT,x); in try find i such that snd(x) = h(fst(x),key(i)) out(cR,ok) R : else out(cR,ko).
And we finally declare the final system. We instantiate multiple copies of the reader, and for each value
i, we also instantiate multilpe copies of
tag(i) with the replicaiton over
system ((!_j reader(j)) | (!_i !_k tag(i))).
A system declared this way is given the name
default. Other systems can be defined and given an epxlicit name. For instance, the following declare the system
simple, where each tag can only be executed once for each identity.
system [simple] ((!_j reader(j)) | (!_i tag(i))).
We express reachabilities formulas inside a first-order logic. In this logic, terms can be of type
timestamp. The logic proves that formulas are true for all possible traces of the protocol, and for all possible values of the variable given this trace/
For instance, a timestamp variable
t allows to talk about a given point inside a trace.
t will intuitively have to take the value of some concrete action, e.g.,
R(j) in our example.
To discuss about the value of the output performed at some timestamp, we use macros:
input@tis the value given as input by the attacker to the action at t;
output@tis the output performed by action at t;
cond@tis the executability condition at t;
frame@tis the sequence of all previous outputs up to t;
exec@tis the conjonction of all executability conditions up to t.
It is then possible to write formulas that capture properties satisfied by all executions of the protocol. For instance, the following formula describes that the executability execution of the reader in fact implies some authentication property, in the sense that there must exists an action T(i,k) that was executed before the reader, and such the input of the reader corresonds to the name of T(i,k).
goal wa : forall (i:index, j:index), happens(R(j,i)) => cond@R(j,i) =>exists (k:index), T(i,k) <= R(j,i) && fst(input@R(j,i)) = nT(i,k).
We write bellow the simple proof of this statement. Once inside a proof context, delimited by
Qed., it is possible to get the list of available tactics by typing
help., and details about any tactic with
Proof. help. help simpl. simpl. expand cond@R(j,i). euf H. exists k. by Qed.