This tutorial provides a very quick introduction to the main concepts
of **Squirrel**. It can be used to ease its discovery and to get an
intuitive grasp of the multiple concepts by going through a concrete
example. The reference manual provides a more extensive presentation
of all the concepts.

In many cases, the concepts introduced here are also direct clickable references to the more extensive presentation in the reference manual.

# Protocol modelling¶

Squirrel allows performing proofs of security for communication protocols relying on cryptography. It works within a high-order logic, and a first step is to be able to model all the components of a protocol inside the logic.

## Messages¶

Messages computed by a protocol and sent over the network are modelled using terms.

Concretely, a term is built from

names

`n`

used to model random sampling;application of functions

`f(m_1,...,m_k)`

.

This allows effectively modelling any computation, as one can have function symbols modelling any sort of computations, from equality testing to conditional branching or encryption functions.

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.

When using such function symbols inside a protocol, we are effectively saying that those function symbol may be in practice instantiated by any function of the correct type. And a proof in such a model holds for any possible implementation of those functions. This is notably useful to model a constant ok, without giving any specific concrete value to this constant.

ok and ko are constants, and f1 is a function that expects a message, and returns a message. f2 is then a function symbol of arity two. Function symbols of any arity can be defined similarly.

A name n typically allows to model secret keys or nonces. As we wish to be able to refer to an unbounded number of sessions, we allow names to be indexed, each value of the index yielding a fresh independent random value. An indexed name is denoted by n[i], 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 as follows.

- name n : message name n1 : index -> message name n2 : index * index -> message.
- global axiom [any] namelength_n : [len n = namelength_message] global axiom [any] namelength_n1 : [forall (i:index), len (n1 i) = namelength_message] global axiom [any] namelength_n2 : [forall (i:index * index), len (n2 i) = namelength_message]

Compared to usual game based cryptography, one can think about names as sampling at the beginning of the protocol execution all possible random values that will ever be needed, and store them within indexed cells, which are our names.

To model a setting where multiple people each have their own secret key, one could declare an indexed name as follows.

- name kT : index -> message.
- global axiom [any] namelength_kT : [forall (i:index), len (kT i) = namelength_message]

## Basic assumption¶

We can declare axioms over our abstract function symbols, for instance
to state that the two abstract constant `ok`

and `ko`

are not
equal.

- axiom [any] ok_not_ko: ok <> ko.
- axiom [any] ok_not_ko : ok <> ko

A proof made in such a model would then apply to any concrete
implementation in which `ok`

and `ko`

are given two distinct
concrete values.

Axioms are formulas in a high-order logic, for instance allowing free
variables, universal and existential quantification, implications,
etc. Here, we define the axiom as true over `any`

protocol.

Another axiom that could be useful to prove the security of a protocol
is for instance that `ko`

can never be equal to any pair
`<x,y>`

.

- axiom [any] ok_not_pair (x,y:message): <x,y> <> ko.
- axiom [any] ok_not_pair : forall (x,y:message), <x,y> <> ko

Going back to the name declaration, if we now display the **Squirrel**
output after a declaration, we see the following:

- name skey : index -> message.
- global axiom [any] namelength_skey : [forall (i:index), len (skey i) = namelength_message]

This means that whenever a new name is declared, we also create a dedicated axiom stating that the length of the name (which is a random bitstring) is equal to some constant. In other words, all names have the same length.

## Cryptographic assumptions¶

Function symbols can be defined as being encryption functions, hash functions, signature functions, etc. The tool will then assume that such functions satisfy some classical cryptographic assumptions.

Some possible primitives, and the corresponding assumptions, are:

symmetric and asymmetric encryption,

CCA1&INT-CTXT(only in the symmetric case)signature,

EUF-CMAhash function,

PRF, and thusEUF-CMA,CR

Each is declared in the following way.

- signature sign,checksign,pk hash h senc enc,dec aenc asenc,asdec,aspk.

## Protocols¶

Protocols are described in a variant of the pi-calculus as processes. They are defined by the following constructs:

`new n`

is used to declare a fresh name (this is optional, and equivalent to the style of name declarations described earlier);

`out(c,m)`

is used to send term m over channel c;

`in(c,x)`

is used to receive some value from channel c, bound to the variable x;

`act; P`

correspond to the sequential composition of action act with process P;

`process name(vars) = ...`

allows to give a name to a process: using name(vars) inside another process then unfold the process definition;

`P | Q`

is the parallel composition of two processes;

`if phi then P else Q`

is conditional branching;

`try find vars such that phi in P else Q`

is a global lookup over indices, it can be seen as a lookup in a database.

As an example, we use a small *RFID*-based protocol, with a tag and a reader,
called the basic hash protocol [BCDH10].

Example: Basic Hash

T –> R : <nT, h(nT,kT)>

R –> T : ok

Here, a tag `T`

sends to the reader `R`

a fresh challenge
`nT`

, authenticated via a MAC using the tag’s key
`kT`

. Each tag has a distinct `kT`

, and the reader has a
database containing all of them.

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 the first process for the tags, which may correspond to multiple identities, and thus depends on some index variable i.

- process tag(i:index) = new nT; T : out(cT, <nT, h(nT,kT(i))>).
- process tag (i:index) = new nT : message; T: out([mcT,<nT,h (nT, kT i)>); null

We now declare the process for the reader.

- process reader = in(cT,x); try find i such that snd(x) = h(fst(x),kT(i)) in R : out(cR,ok) else R1 : out(cR,ko).
- process reader = in([mcT,x); find (i) such that snd x = h (fst x, kT i) in R: out([mcR,ok); null else R1: out([mcR,ko); null

Finally, we declare the complete system. We instantiate multiple copies
of the reader process, and for each value i, we also instantiate multiple copies of
`tag(i)`

with the replication over k.

- system ((!_j reader) | (!_i !_k tag(i))).
- Typed-check process: ( !_j( reader ) ) | !_i( !_k( tag i)) global axiom [any] namelength_nT : [forall (i:index * index), len (nT i) = namelength_message] Added action dependencies lemmas: axiom [default] mutex_default_R1_R : forall (j,i:index), not happens(R1(j)) || not happens(R(j, i)) axiom [default] mutex_default_R_R1 : forall (j,i:index), not happens(R(j, i)) || not happens(R1(j)) axiom [default] depends_default_init_T : forall (t:timestamp,i,k:index), t = T(i, k) => happens(t) => init < T(i, k) axiom [default] depends_default_init_R1 : forall (t:timestamp,j:index), t = R1(j) => happens(t) => init < R1(j) axiom [default] depends_default_init_R : forall (t:timestamp,j,i:index), t = R(j, i) => happens(t) => init < R(j, i) System after processing: ( !_j( in([mcT,x); find (i) such that snd x = h (fst x, kT i) in R: out([mcR,ok); null else R1: out([mcR,ko); null) ) | !_i( !_k( T: out([mcT,<nT (i, k),h (nT (i, k), kT i)>); null)) System Empty registered with actions (init). System default registered with actions (init,R,R1,T).

We see that with this declaration, in the resulting system after
processing, all outputs have been given a name, and each output
corresponds to a possible action that can be triggered by the
attacker. Here, the possible actions are `(init,R,R1,T)`

.
Many axioms are created, expressing the fact that for instance
actions `R1`

and `R`

are mutually exclusive, as they
are exclusive branches; this is the
`mutex_default_R1_R`

axiom, stating that for any possible
execution, the two actions cannot both happen in the trace.

A system declared this way is given the name default. Other systems can be defined and given an explicit name. For instance, the following declares the system simple, where each tag can only be executed once for each identity.

- system [simple] ((!_j reader) | (!_i tag(i))).
- Typed-check process: ( !_j( reader ) ) | !_i( tag i) global axiom [any] namelength_nT1 : [forall (i:index), len (nT1 i) = namelength_message] Added action dependencies lemmas: axiom [simple] mutex_simple_R1_R : forall (j,i:index), not happens(R1(j)) || not happens(R(j, i)) axiom [simple] mutex_simple_R_R1 : forall (j,i:index), not happens(R(j, i)) || not happens(R1(j)) axiom [simple] depends_simple_init_T1 : forall (t:timestamp,i:index), t = T1(i) => happens(t) => init < T1(i) axiom [simple] depends_simple_init_R1 : forall (t:timestamp,j:index), t = R1(j) => happens(t) => init < R1(j) axiom [simple] depends_simple_init_R : forall (t:timestamp,j,i:index), t = R(j, i) => happens(t) => init < R(j, i) System after processing: ( !_j( in([mcT,x); find (i) such that snd x = h (fst x, kT i) in R: out([mcR,ok); null else R1: out([mcR,ko); null) ) | !_i( T1: out([mcT,<nT1 i,h (nT1 i, kT i)>); null) System Empty registered with actions (init). System default registered with actions (init,R,R1,T). System simple registered with actions (init,R,R1,T1).

# Reachability properties¶

We consider reachability formulas, that is, properties that talk
about what is possible or not for all traces.
In **Squirrel**, we express such formulas in a first order logic,
and call them local formulas.

In this logic, terms can be of type `message`

, `boolean`

,
`index`

and `timestamp`

. The logic lets us prove that formulas are
true for all possible traces of the protocol, and for all possible
values of the variables given a 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.*, T(i) or R(j) in our case.

## Macros¶

To discuss about the value of the output performed at some timestamp, we use macros:

`input@t`

is the value given as input by the attacker to the action at t;

`output@t`

is the output performed by the action at t;

`cond@t`

is the executability condition of the action at t;

`frame@t`

is the sequence of all previous outputs up to t;

`exec@t`

is the conjunction of all executability conditions up to t.

## Formulas¶

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. More precisely,
there must exist an action `T(i,k)`

that was executed before the
reader, and such the input of the reader corresponds to the name of
`T(i,k)`

.

- lemma 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).
- Goal wa : forall (i,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 below the simple proof of this statement. The high-level
idea of the proof is to use the **EUF** cryptographic axiom:
only the tag T(i,k) can compute h(nT(i,k),kT(i)) because the
secret key is not known by the attacker. Therefore, any message
accepted by the reader must come from a tag that has played before.
The converse implication is trivial, because any honest tag output is
accepted by the reader.

Once inside a proof context, delimited by Proof. and Qed., it is possible to display the list of available tactics by typing help., and details about any tactic with help tacticname.

We now start the proof.

- Proof.
- [goal> Focused goal (1/1): System: default —————————————- forall (i,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)

After the `Proof`

command, **Squirrel** displays the current
judgement. It contains the number of goals that remain to be proved
(one at first, but additional subgoals may be created by tactics), the system we are
working in, and the formula to be proved.

- intro i j Hh Hc.
- [goal> Focused goal (1/1): System: default Variables: i,j:index[const] Hc: cond@R(j, i) Hh: happens(R(j, i)) —————————————- exists (k:index), T(i, k) <= R(j, i) && fst (input@R(j, i)) = nT (i, k)

We have performed an introduction with the `intro`

tactic. This
pushes universal quantification inside the judgment context, where
the universally quantified variables become free variables. This allows us
to then push the left-hand side of the implications as hypotheses of
the judgment, that we can then reason on. The free variables and
assumptions are named according to the identifiers given as parameters to `intro`

.

- expand cond.
- [goal> Focused goal (1/1): System: default Variables: i,j:index[const] Hc: snd (input@R(j, i)) = h (fst (input@R(j, i)), kT i) Hh: happens(R(j, i)) —————————————- exists (k:index), T(i, k) <= R(j, i) && fst (input@R(j, i)) = nT (i, k)

After introducing the hypotheses and expanding the executability
condition of `R`

, we get an equality between a hash and some other
term `snd (input@R(j, i))`

. We then use the unforgeability of the
hash function, the **EUF** assumption, to get that the hashed value
`fst (input@R(j, i))`

must be equal to some honestly hashed value
in `snd (input@R(j, i))`

, since the key `kT`

is secret. All
honestly hashes are produced by the tag, which will then conclude our
proof. This cryptographic axiom is applied thanks to the `euf`

tactic.

- euf Hc.
- Indirect bad occurrences of key kT(i), and messages authenticated by it in other actions: nT (i, k) auth. by kT(i) (collision with fst (input@R(j, i)) auth. by kT(i)) in action T(i, k) in term <nT (i, k),h (nT (i, k), kT i)> Total: 1 occurrence 0 of them are subsumed by another 1 occurrence remaining [goal> Focused goal (1/1): System: default Variables: i,j:index[const] Hc: snd (input@R(j, i)) = h (fst (input@R(j, i)), kT i) Hh: happens(R(j, i)) —————————————- (exists (k:index), T(i, k) < R(j, i) && fst (input@R(j, i)) = nT (i, k)) => exists (k:index), T(i, k) <= R(j, i) && fst (input@R(j, i)) = nT (i, k)

To conclude, we just have to use the `k`

introduced by the
`euf`

tactic as a witness for the existential `k`

we have to
find.

- intro [k _].
- [goal> Focused goal (1/1): System: default Variables: i,j,k:index[const] Hc: snd (input@R(j, i)) = h (fst (input@R(j, i)), kT i) Hh: happens(R(j, i)) _: T(i, k) < R(j, i) && fst (input@R(j, i)) = nT (i, k) —————————————- exists (k:index), T(i, k) <= R(j, i) && fst (input@R(j, i)) = nT (i, k)
- by exists k.
- [goal> lemma wa is proved
- Qed.
- lemma [default] wa : forall (i,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) Exiting proof mode.

# Equivalence properties¶

More complex properties based on equivalence can be expressed. Intuitively, two processes are equivalent if the attacker cannot know whether it is interacting with one or the other. This is a generic security property used in the computational model to prove many distinct flavours of security.

We can declare in **Squirrel** two variants of a protocol at once using
the `diff(t1,t2)`

operator. A process containing diff-terms is
called a bi-process, as it can lead to two distinct processes when
projecting on the left or the right of the diff. This allows to easily
model some security properties.

For instance, we can declare a bi-process `tagD`

, where
on one side each tag may be called many times and always use
there own key, while on the right side, we in
fact use a new fresh independent key every time a tag is called.
The left-hand side of the process can be seen as the real world,
while the right-hand side is an idealised world where a new tag is used each time.
Proving that these two worlds are equivalent will establish
that tags cannot be tracked.

- name kT’: index * index -> message process tagD(i:index,k:index) = new nT; out(cT, <nT, h(nT,diff(kT(i),kT’(i,k)))>).
- global axiom [any] namelength_kT’ : [forall (i:index * index), len (kT’ i) = namelength_message] process tagD (i,k:index) = new nT : message; out([mcT,<nT,h (nT, diff(kT i, kT’ (i, k)))>); null
- process readerD(j:index) = in(cT,x); if exists (i,k:index), snd(x) = h(fst(x),diff(kT(i),kT’(i,k))) then out(cR,ok) else out(cR,ko) system [BasicHash] ((!_j R: readerD(j)) | (!_i !_k T: tagD(i,k))).
- process readerD (j:index) = in([mcT,x); if exists (i,k:index), snd x = h (fst x, diff(kT i, kT’ (i, k))) then out([mcR,ok); null else out([mcR,ko); null Typed-check process: ( !_j( R: readerD j) ) | !_i( !_k( T: tagD i k)) global axiom [any] namelength_nT2 : [forall (i:index * index), len (nT2 i) = namelength_message] Added action dependencies lemmas: axiom [BasicHash] mutex_BasicHash_R1_R2 : forall (j:index), not happens(R1(j)) || not happens(R2(j)) axiom [BasicHash] mutex_BasicHash_R2_R1 : forall (j:index), not happens(R2(j)) || not happens(R1(j)) axiom [BasicHash] depends_BasicHash_init_T : forall (t:timestamp,i,k:index), t = T(i, k) => happens(t) => init < T(i, k) axiom [BasicHash] depends_BasicHash_init_R1 : forall (t:timestamp,j:index), t = R1(j) => happens(t) => init < R1(j) axiom [BasicHash] depends_BasicHash_init_R2 : forall (t:timestamp,j:index), t = R2(j) => happens(t) => init < R2(j) System after processing: ( !_j( in([mcT,x); if exists (i,k:index), snd x = h (fst x, diff(kT i, kT’ (i, k))) then R2: out([mcR,ok); null else R1: out([mcR,ko); null) ) | !_i( !_k( T: out([mcT,<nT2 (i, k),h (nT2 (i, k), diff(kT i, kT’ (i, k)))>); null)) System BasicHash registered with actions (init,R2,R1,T). System Empty registered with actions (init). System default registered with actions (init,R,R1,T). System simple registered with actions (init,R,R1,T1).

Importantly, reachability formulas can be expressed and proved directly on bi-systems. We can for instance write a variant of the previous proof directly on the bi-system:

- lemma [BasicHash] wa_R : forall (tau:timestamp), happens(tau) => ((exists (i,k:index), snd(input@tau) = h(fst(input@tau),diff(kT(i),kT’(i,k)))) <=> (exists (i,k:index), T(i,k) < tau && fst(output@T(i,k)) = fst(input@tau) && snd(output@T(i,k)) = snd(input@tau))).
- Goal wa_R : forall (tau:timestamp), happens(tau) => (exists (i,k:index), snd (input@tau) = h (fst (input@tau), diff(kT i, kT’ (i, k)))) <=> exists (i,k:index), T(i, k) < tau && fst (output@T(i, k)) = fst (input@tau) && snd (output@T(i, k)) = snd (input@tau)

The idea of the proof is similar, except that we prove here a logical equivalence instead of an implication.

- Proof.
- [goal> Focused goal (1/1): System: BasicHash —————————————- forall (tau:timestamp), happens(tau) => (exists (i,k:index), snd (input@tau) = h (fst (input@tau), diff(kT i, kT’ (i, k)))) <=> exists (i,k:index), T(i, k) < tau && fst (output@T(i, k)) = fst (input@tau) && snd (output@T(i, k)) = snd (input@tau)
- intro tau Hap.
- [goal> Focused goal (1/1): System: BasicHash Variables: tau:timestamp[const] Hap: happens(tau) —————————————- (exists (i,k:index), snd (input@tau) = h (fst (input@tau), diff(kT i, kT’ (i, k)))) <=> exists (i,k:index), T(i, k) < tau && fst (output@T(i, k)) = fst (input@tau) && snd (output@T(i, k)) = snd (input@tau)

We have to prove two implications (`<=>`

): we thus split the proof
in two parts. We now have two different goals to prove.

- split; intro [i k Meq].
- [goal> Focused goal (1/2): System: BasicHash Variables: i,k:index[const],tau:timestamp[const] Hap: happens(tau) Meq: snd (input@tau) = h (fst (input@tau), diff(kT i, kT’ (i, k))) —————————————- exists (i,k:index), T(i, k) < tau && fst (output@T(i, k)) = fst (input@tau) && snd (output@T(i, k)) = snd (input@tau)

For the first implication (`=>`

), we actually consider separately
the real system (left) and the ideal system (right).

- project.
- [goal> Focused goal (1/3): System: left:BasicHash/left Variables: i,k:index[const],tau:timestamp[const] Hap: happens(tau) Meq: snd (input@tau) = h (fst (input@tau), kT i) —————————————- exists (i,k:index), T(i, k) < tau && fst (output@T(i, k)) = fst (input@tau) && snd (output@T(i, k)) = snd (input@tau)

The proof is very similar on both sides, and relies on the `euf`

tactic. Applying the `euf`

tactic on the Meq hypothesis
generates a new hypothesis stating that fst(input@R(j)) must be
equal to some message that has already been hashed before. The only
possibility is that this hash comes from the output of a tag that has
played before (thus the new hypothesis on timestamps).

- euf Meq.
- Indirect bad occurrences of key kT(i), and messages authenticated by it in other actions: nT2 (i, k) auth. by kT(i) (collision with fst (input@tau) auth. by kT(i)) in action T(i, k) in term <nT2 (i, k),h (nT2 (i, k), kT i)> Total: 1 occurrence 0 of them are subsumed by another 1 occurrence remaining [goal> Focused goal (1/3): System: left:BasicHash/left Variables: i,k:index[const],tau:timestamp[const] Hap: happens(tau) Meq: snd (input@tau) = h (fst (input@tau), kT i) —————————————- (exists (k:index), T(i, k) < tau && fst (input@tau) = nT2 (i, k)) => exists (i,k:index), T(i, k) < tau && fst (output@T(i, k)) = fst (input@tau) && snd (output@T(i, k)) = snd (input@tau)
- intro [k0 _].
- [goal> Focused goal (1/3): System: left:BasicHash/left Variables: i,k,k0:index[const],tau:timestamp[const] Hap: happens(tau) Meq: snd (input@tau) = h (fst (input@tau), kT i) _: T(i, k0) < tau && fst (input@tau) = nT2 (i, k0) —————————————- exists (i,k:index), T(i, k) < tau && fst (output@T(i, k)) = fst (input@tau) && snd (output@T(i, k)) = snd (input@tau)
- by exists i,k0.
- [goal> Focused goal (1/2): System: right:BasicHash/right Variables: i,k:index[const],tau:timestamp[const] Hap: happens(tau) Meq: snd (input@tau) = h (fst (input@tau), kT’ (i, k)) —————————————- exists (i,k:index), T(i, k) < tau && fst (output@T(i, k)) = fst (input@tau) && snd (output@T(i, k)) = snd (input@tau)

The right side of the proof is very similar.

- euf Meq => *.
- Indirect bad occurrences of key kT’((i, k)), and messages authenticated by it in other actions: nT2 (i, k) auth. by kT’((i, k)) (collision with fst (input@tau) auth. by kT’((i, k))) in action T(i, k) in term <nT2 (i, k),h (nT2 (i, k), kT’ (i, k))> Total: 1 occurrence 0 of them are subsumed by another 1 occurrence remaining [goal> Focused goal (1/2): System: right:BasicHash/right Variables: i,k:index[const],tau:timestamp[const] H: T(i, k) < tau && fst (input@tau) = nT2 (i, k) Hap: happens(tau) Meq: snd (input@tau) = h (fst (input@tau), kT’ (i, k)) —————————————- exists (i,k:index), T(i, k) < tau && fst (output@T(i, k)) = fst (input@tau) && snd (output@T(i, k)) = snd (input@tau)
- by exists i,k.
- [goal> Focused goal (1/1): System: BasicHash Variables: i,k:index[const],tau:timestamp[const] Hap: happens(tau) Meq: T(i, k) < tau && fst (output@T(i, k)) = fst (input@tau) && snd (output@T(i, k)) = snd (input@tau) —————————————- exists (i,k:index), snd (input@tau) = h (fst (input@tau), diff(kT i, kT’ (i, k)))

We use here the notation `euf Meq => *`

, which is a shortcut for
`euf Meq; intro *`

, the `*`

performing as many introductions
as possible, with automatic naming of variables and hypotheses.

For the second implication (`<=`

), the conclusion of the goal can
directly be obtained from the hypotheses.

- by exists i,k.
- [goal> lemma wa_R is proved
- Qed.
- lemma [BasicHash] wa_R : forall (tau:timestamp), happens(tau) => (exists (i,k:index), snd (input@tau) = h (fst (input@tau), diff(kT i, kT’ (i, k)))) <=> exists (i,k:index), T(i, k) < tau && fst (output@T(i, k)) = fst (input@tau) && snd (output@T(i, k)) = snd (input@tau) Exiting proof mode.

We now prove an equivalence property expressing the unlinkability of the
protocol. This property is expressed by the logical formula ```
forall
t:timestamp, [happens(t)] -> equiv(frame@t)
```

where `frame@t`

is
actually a bi-frame. It states that for any trace (the quantification
is implicit over all traces), at any point that happens in the trace,
the two frames (derived by projecting the diff operator) are equivalent. Square
brackets contain local formulas, and such a formula mixing both local
formulas and equivalences is called a global formula.

Here, we will have to prove that the left projection of `frame@t`

(*i.e.*
the real system) is indistinguishable from the right projection of
`frame@t`

(*i.e.* the ideal system).

As this goal is a frequent one, a shortcut allows declaring this goal
without writing the full formula, using the keyword `equiv`

.

- equiv [BasicHash] unlinkability.
- Goal unlinkability : forall t:timestamp[const, glob], equiv(frame@t)
- Proof.
- [goal> Focused goal (1/1): Systems: BasicHash (same for equivalences) Variables: t:timestamp[const, glob] H: [happens(t)] —————————————- 0: frame@t

An equivalence judgment contains the list of hypotheses, as before. The conclusion is however different to the reachability case. Now, we have a numbered list of diff-terms, and we must prove that the left projection and the right projection of this list are indistinguishable. We refer to this sequence of diff terms as the biframe of the goal.

The high-level idea of the proof is as follows:

if

`t`

corresponds to a reader’s action, we show that the outcome of the conditional is the same on both sides and that this outcome only depends on information already available to the attacker;if

`t`

corresponds to a tag’s action, we show that the new message added in the frame (*i.e.*the tag’s output) does not give any information that helps the attacker distinguish the real system from the ideal one. Indeed, hashes can intuitively be seen as fresh names thanks to the**PRF**cryptographic axiom.

The proof is done by induction over the timestamp `t`

. The
`induction`

tactic also automatically introduces a case analysis over
all possible values for `t`

. The first case, where ```
t =
init
```

corresponds to the initial point of the execution trace, before
any protocol action has happened. That case is trivial, we directly close it with
`auto`

. The other cases correspond to the 3 different actions
of the protocol.

- induction t.
- [goal> Focused goal (1/4): Systems: BasicHash (same for equivalences) H: [happens(init)] —————————————- 0: frame@init
- auto.
- [goal> Focused goal (1/3): Systems: BasicHash (same for equivalences) Variables: j:index[const, glob] H: [happens(R2(j))] IH: equiv(frame@pred (R2(j))) —————————————- 0: frame@R2(j)

For the case where `t = R2(j)`

, we start by expanding the macros
and splitting the pairs. Splitting the pairs is done by using the
`fa`

tactic, which when applied to all pairs thanks to the
pattern `!<_,_>`

splits a bi-frame element containing a pair into
two biframe elements, containing the the two components.

- expand frame, exec, output.
- [goal> Focused goal (1/3): Systems: BasicHash (same for equivalences) Variables: j:index[const, glob] H: [happens(R2(j))] IH: equiv(frame@pred (R2(j))) —————————————- 0: <frame@pred (R2(j)), <of_bool (exec@pred (R2(j)) && cond@R2(j)), if (exec@pred (R2(j)) && cond@R2(j)) then ok>>
- fa !<_,_>.
- [goal> Focused goal (1/3): Systems: BasicHash (same for equivalences) Variables: j:index[const, glob] H: [happens(R2(j))] IH: equiv(frame@pred (R2(j))) —————————————- 0: frame@pred (R2(j)) 1: exec@pred (R2(j)) && cond@R2(j)

Using the previously proved authentication goal `wa_R`

, we replace
the formula `cond@R2(j)`

with an equivalent formula, which states
that a tag `T(i,k)`

has played before and that the output of
this tag is equal to the message input by the reader. This is one of the
strength of **Squirrel**: we can finely reuse previously proved goals to
simplify a current goal. Here, we can see the `wa_R`

lemma as a
rewriting rule over boolean formulas, and so we use the `rewrite`

tactic.

- rewrite /cond (wa_R (R2 j)) //.
- [goal> Focused goal (1/3): Systems: BasicHash (same for equivalences) Variables: j:index[const, glob] H: [happens(R2(j))] IH: equiv(frame@pred (R2(j))) —————————————- 0: frame@pred (R2(j)) 1: exec@pred (R2(j)) && exists (i,k:index), T(i, k) < R2(j) && fst (output@T(i, k)) = fst (input@R2(j)) && snd (output@T(i, k)) = snd (input@R2(j))

We are now able to remove this formula from the frame because the
attacker is able to compute it using information obtained in the
past. Indeed, each of its elements is already available in
`frame@pred(R2(j))`

. This is done by the `deduce`

tactic.

- by deduce 1.
- [goal> Focused goal (1/2): Systems: BasicHash (same for equivalences) Variables: j:index[const, glob] H: [happens(R1(j))] IH: equiv(frame@pred (R1(j))) —————————————- 0: frame@R1(j)

The case where `t = R1(j)`

is similar to the previous one.

- expand frame, exec, output.
- [goal> Focused goal (1/2): Systems: BasicHash (same for equivalences) Variables: j:index[const, glob] H: [happens(R1(j))] IH: equiv(frame@pred (R1(j))) —————————————- 0: <frame@pred (R1(j)), <of_bool (exec@pred (R1(j)) && cond@R1(j)), if (exec@pred (R1(j)) && cond@R1(j)) then ko>>
- fa !<_,_>.
- [goal> Focused goal (1/2): Systems: BasicHash (same for equivalences) Variables: j:index[const, glob] H: [happens(R1(j))] IH: equiv(frame@pred (R1(j))) —————————————- 0: frame@pred (R1(j)) 1: exec@pred (R1(j)) && cond@R1(j)
- rewrite /cond (wa_R (R1 j)) //.
- [goal> Focused goal (1/2): Systems: BasicHash (same for equivalences) Variables: j:index[const, glob] H: [happens(R1(j))] IH: equiv(frame@pred (R1(j))) —————————————- 0: frame@pred (R1(j)) 1: exec@pred (R1(j)) && not exists (i,k:index), T(i, k) < R1(j) && fst (output@T(i, k)) = fst (input@R1(j)) && snd (output@T(i, k)) = snd (input@R1(j))
- by deduce 1.
- [goal> Focused goal (1/1): Systems: BasicHash (same for equivalences) Variables: i,k:index[const, glob] H: [happens(T(i, k))] IH: equiv(frame@pred (T(i, k))) —————————————- 0: frame@T(i, k)

Finally, for the case where `t = T(i,k)`

, we similarly start by expanding the
macros and splitting the pairs.

- expand frame, exec, cond, output.
- [goal> Focused goal (1/1): Systems: BasicHash (same for equivalences) Variables: i,k:index[const, glob] H: [happens(T(i, k))] IH: equiv(frame@pred (T(i, k))) —————————————- 0: <frame@pred (T(i, k)), <of_bool (exec@pred (T(i, k)) && true), if (exec@pred (T(i, k)) && true) then <nT2 (i, k),h (nT2 (i, k), diff(kT i, kT’ (i, k)))>>>
- fa !<_,_>, if _ then _, <_,_>.
- [goal> Focused goal (1/1): Systems: BasicHash (same for equivalences) Variables: i,k:index[const, glob] H: [happens(T(i, k))] IH: equiv(frame@pred (T(i, k))) —————————————- 0: frame@pred (T(i, k)) 1: nT2 (i, k) 2: h (nT2 (i, k), diff(kT i, kT’ (i, k)))

We now apply the `prf`

tactic, in order to replace the hash with a fresh
name. This creates a new subgoal, asking to prove that the hashed value
has never been hased before.

- prf 2.
- global axiom [any] namelength_n_PRF : [len n_PRF = namelength_message] Applying PRF to h (nT2 (i, k), diff(kT i, kT’ (i, k))) Checking for occurrences on the left Indirect bad occurrences of key kT(i), and messages hashed by it in other actions: fst (input@R2(j)) hashed by kT(i) (collision with nT2 (i, k) hashed by kT(i)) in action R2(j) in term snd (input@R2(j)) = h (fst (input@R2(j)), kT i) fst (input@R1(j)) hashed by kT(i) (collision with nT2 (i, k) hashed by kT(i)) in action R1(j) in term snd (input@R1(j)) = h (fst (input@R1(j)), kT i) nT2 (i, k) hashed by kT(i) (collision with nT2 (i, k) hashed by kT(i)) in action T(i, k) in term <nT2 (i, k),h (nT2 (i, k), kT i)> Total: 3 occurrences 0 of them are subsumed by another 3 occurrences remaining Checking for occurrences on the right Indirect bad occurrences of key kT’((i, k)), and messages hashed by it in other actions: fst (input@R2(j)) hashed by kT’((i, k)) (collision with nT2 (i, k) hashed by kT’((i, k))) in action R2(j) in term snd (input@R2(j)) = h (fst (input@R2(j)), kT’ (i, k)) fst (input@R1(j)) hashed by kT’((i, k)) (collision with nT2 (i, k) hashed by kT’((i, k))) in action R1(j) in term snd (input@R1(j)) = h (fst (input@R1(j)), kT’ (i, k)) nT2 (i, k) hashed by kT’((i, k)) (collision with nT2 (i, k) hashed by kT’((i, k))) in action T(i, k) in term <nT2 (i, k),h (nT2 (i, k), kT’ (i, k))> Total: 3 occurrences 0 of them are subsumed by another 3 occurrences remaining [goal> Focused goal (1/3): System: left:BasicHash/left (equivalences: BasicHash) Variables: i,k:index[const, glob] H: [happens(T(i, k))] IH: equiv(frame@pred (T(i, k))) —————————————- (forall (i0,j:index), R2(j) < T(i, k) => i = i0 => nT2 (i, k) <> fst (input@R2(j))) && (forall (i0,j:index), R1(j) < T(i, k) => i = i0 => nT2 (i, k) <> fst (input@R1(j))) && forall (i0,k0:index), T(i0, k0) < T(i, k) => i = i0 => nT2 (i, k) <> nT2 (i0, k0)

Several conjuncts must now be proved, the same tactic can be used on all of them. Here are a few representative cases:

In one case,

`nT(i,k)`

cannot occur in`input@R2(j)`

because`R2(j) < T(i,k)`

.In another case,

`nT(i,k) = nT(i0,k0)`

implies that`i=i0`

and`k=k0`

, contradicting`T(i0,k0)<T(i,k)`

.

In both cases, the reasoning is performed by the `fresh`

tactic on the
message equality hypothesis `Meq`

, whose negation was initially to be
proved. To be able to use (`split`

and) `fresh`

, we first project the
goal onto on the left projection and one goal for the right projection of the initial bi-system.

- repeat split; intro *; by fresh Meq.
- Freshness of occurrences of nT2((i, k)): Indirect occurrences of nT2((i, k)) in other actions: nT2((i, k)) (collision with nT2((i, k))) in action T(i, k) in term <nT2 (i, k),h (nT2 (i, k), kT i)> nT2((i, k)) (collision with nT2((i, k))) in action T(i, k) in term <nT2 (i, k),h (nT2 (i, k), kT i)> Total: 2 occurrences 1 of them is subsumed by another 1 occurrence remaining Freshness of occurrences of nT2((i, k)): Indirect occurrences of nT2((i, k)) in other actions: nT2((i, k)) (collision with nT2((i, k))) in action T(i, k) in term <nT2 (i, k),h (nT2 (i, k), kT i)> nT2((i, k)) (collision with nT2((i, k))) in action T(i, k) in term <nT2 (i, k),h (nT2 (i, k), kT i)> Total: 2 occurrences 1 of them is subsumed by another 1 occurrence remaining Freshness of occurrences of nT2((i, k)): Direct occurrences of nT2((i, k)) in nT2 (i0, k0): nT2((i0, k0)) (collision with nT2((i, k))) in term nT2 (i0, k0) Total: 1 occurrence 0 of them are subsumed by another 1 occurrence remaining [goal> Focused goal (1/2): System: right:BasicHash/right (equivalences: BasicHash) Variables: i,k:index[const, glob] H: [happens(T(i, k))] IH: equiv(frame@pred (T(i, k))) —————————————- (forall (k0,i0,j:index), R2(j) < T(i, k) => i = i0 && k = k0 => nT2 (i, k) <> fst (input@R2(j))) && (forall (k0,i0,j:index), R1(j) < T(i, k) => i = i0 && k = k0 => nT2 (i, k) <> fst (input@R1(j))) && forall (i0,k0:index), T(i0, k0) < T(i, k) => i = i0 && k = k0 => nT2 (i, k) <> nT2 (i0, k0)
- repeat split; intro *; by fresh Meq.
- Freshness of occurrences of nT2((i, k)): Indirect occurrences of nT2((i, k)) in other actions: nT2((i, k)) (collision with nT2((i, k))) in action T(i, k) in term <nT2 (i, k),h (nT2 (i, k), kT’ (i, k))> nT2((i, k)) (collision with nT2((i, k))) in action T(i, k) in term <nT2 (i, k),h (nT2 (i, k), kT’ (i, k))> Total: 2 occurrences 1 of them is subsumed by another 1 occurrence remaining Freshness of occurrences of nT2((i, k)): Indirect occurrences of nT2((i, k)) in other actions: nT2((i, k)) (collision with nT2((i, k))) in action T(i, k) in term <nT2 (i, k),h (nT2 (i, k), kT’ (i, k))> nT2((i, k)) (collision with nT2((i, k))) in action T(i, k) in term <nT2 (i, k),h (nT2 (i, k), kT’ (i, k))> Total: 2 occurrences 1 of them is subsumed by another 1 occurrence remaining Freshness of occurrences of nT2((i, k)): Direct occurrences of nT2((i, k)) in nT2 (i0, k0): nT2((i0, k0)) (collision with nT2((i, k))) in term nT2 (i0, k0) Total: 1 occurrence 0 of them are subsumed by another 1 occurrence remaining [goal> Focused goal (1/1): Systems: BasicHash (same for equivalences) Variables: i,k:index[const, glob] H: [happens(T(i, k))] IH: equiv(frame@pred (T(i, k))) —————————————- 0: frame@pred (T(i, k)) 1: nT2 (i, k) 2: n_PRF

We have now replaced the hash by a fresh name occurring nowhere else,
so we can remove it using the `fresh`

tactic.

- fresh 2; 1:auto.
- Freshness on the left side: Freshness on the right side: [goal> Focused goal (1/1): Systems: BasicHash (same for equivalences) Variables: i,k:index[const, glob] H: [happens(T(i, k))] IH: equiv(frame@pred (T(i, k))) —————————————- 0: frame@pred (T(i, k)) 1: nT2 (i, k)

We can also remove the name `nT(i,k)`

, and conclude (automatically) by the induction
hypothesis.

- by fresh 1.
- Freshness on the left side: Indirect occurrences of nT2((i, k)) in other actions: nT2((i, k)) (collision with nT2((i, k))) in action T(i, k) in term <nT2 (i, k),h (nT2 (i, k), kT i)> nT2((i, k)) (collision with nT2((i, k))) in action T(i, k) in term <nT2 (i, k),h (nT2 (i, k), kT i)> Total: 2 occurrences 1 of them is subsumed by another 1 occurrence remaining Freshness on the right side: Indirect occurrences of nT2((i, k)) in other actions: nT2((i, k)) (collision with nT2((i, k))) in action T(i, k) in term <nT2 (i, k),h (nT2 (i, k), kT’ (i, k))> nT2((i, k)) (collision with nT2((i, k))) in action T(i, k) in term <nT2 (i, k),h (nT2 (i, k), kT’ (i, k))> Total: 2 occurrences 1 of them is subsumed by another 1 occurrence remaining [goal> lemma unlinkability is proved
- Qed.
- global lemma [BasicHash (same for equivalences)] unlinkability : Forall (t:timestamp[const, glob]), [happens(t)] -> equiv(frame@t) Exiting proof mode.