\[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\In}{\kw{in}} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[4]{\kw{Ind}_{#4}[#1](#2:=#3)} \newcommand{\Indpstr}[5]{\kw{Ind}_{#4}[#1](#2:=#3)/{#5}} \newcommand{\injective}{\kw{injective}} \newcommand{\kw}[1]{\textsf{#1}} \newcommand{\length}{\textsf{length}} \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} \newcommand{\List}{\textsf{list}} \newcommand{\lra}{\longrightarrow} \newcommand{\Match}{\kw{match}} \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} \newcommand{\ModImp}[3]{{\kw{Mod}}({#1}:{#2}:={#3})} \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} \newcommand{\mto}{.\;} \newcommand{\nat}{\textsf{nat}} \newcommand{\Nil}{\textsf{nil}} \newcommand{\nilhl}{\textsf{nil\_hl}} \newcommand{\nO}{\textsf{O}} \newcommand{\node}{\textsf{node}} \newcommand{\nS}{\textsf{S}} \newcommand{\odd}{\textsf{odd}} \newcommand{\oddS}{\textsf{odd}_\textsf{S}} \newcommand{\ovl}[1]{\overline{#1}} \newcommand{\Pair}{\textsf{pair}} \newcommand{\plus}{\mathsf{plus}} \newcommand{\SProp}{\textsf{SProp}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \newcommand{\Sort}{\mathcal{S}} \newcommand{\Str}{\textsf{Stream}} \newcommand{\Struct}{\kw{Struct}} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\tl}{\textsf{tl}} \newcommand{\tree}{\textsf{tree}} \newcommand{\trii}{\triangleright_\iota} \newcommand{\Type}{\textsf{Type}} \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} \newcommand{\WF}[2]{{\mathcal{W\!F}}(#1)[#2]} \newcommand{\WFE}[1]{\WF{E}{#1}} \newcommand{\WFT}[2]{#1[] \vdash {\mathcal{W\!F}}(#2)} \newcommand{\WFTWOLINES}[2]{{\mathcal{W\!F}}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} \newcommand{\with}{\kw{with}} \newcommand{\WS}[3]{#1[] \vdash #2 <: #3} \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} \newcommand{\zeroone}[1]{[{#1}]} \end{split}\]

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-CMA

• hash function, PRF, and thus EUF-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(cT,<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(cT,x); find (i) such that snd x = h (fst x, kT i) in R: out(cR,ok); null else R1: out(cR,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(cT,x); find (i) such that snd x = h (fst x, kT i) in R: out(cR,ok); null else R1: out(cR,ko); null) ) | !_i( !_k( T: out(cT,<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(cT,x); find (i) such that snd x = h (fst x, kT i) in R: out(cR,ok); null else R1: out(cR,ko); null) ) | !_i( T1: out(cT,<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(cT,<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(cT,x); if exists (i,k:index), snd x = h (fst x, diff(kT i, kT’ (i, k))) then out(cR,ok); null else out(cR,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(cT,x); if exists (i,k:index), snd x = h (fst x, diff(kT i, kT’ (i, k))) then R2: out(cR,ok); null else R1: out(cR,ko); null) ) | !_i( !_k( T: out(cT,<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.