A Squirrel file begin with a series of declarations. They define nonces, functions and, ultimately, systems built with them. Then we can define properties of such systems as goals that we will prove. The proof is a sequence of tactics placed between keywords Proof and Qed.


Terms can be of type message, boolean, index and timestamp. The first two are message kinds, respectively corresponding to a bitstring and a single bit. Indices are used to have infinite collections of objects, and timestamps are used to represent points in an execution trace.

Some functions are built-ins. For example:


A timestamp denotes an action that may belong to the execution. The syntax for timestamps is as follows:


Terms may contain macros, describing data relative to the protocol under study.

input@t and output@t are the input and output of the action denoted by t.

cond@t is the individual execution condition of t, and exec@t is the conjunction of all conditions up until t (included).

frame@t is the knowledge gathered by the attacker at t. It contained the status of the execution at each step and all the outputted messages. When pred(tau) is defined, frame@tau is equal to <frame@pred(tau), <exec@tau, if exec@tau then output@tau>>.

Macros are also used to model mutable states: if s is a mutable state, then s(〈indices〉)@t is the contents of s after t.


Before we declare systems, we need to declare element used to build these systems.


name n : 〈indices〉 -> message

name allows to create nonces, i.e. random samplings of length the security parameter. Names can be indexed, which allows to model unbounded collections of nonces, which is typically used to model protocols with an unbounded number of sessions, each one using its own nonce.

Examples :

Functions and constants

abstract f : 〈indices〉 -> 〈message_types〉 -> 〈message_type〉

abstract declares a function f. The behaviour of f is not specified but can be constrained later by axioms. This function can be declared with an arbitrary number of indices and arguments. If there is no argument, f corresponds to a constant. If there are only index arguments, then f can be seen as an unbounded collection of constants, used e.g. to model identities.

Examples :

In the last example, the function symbol will be used with infix notation, i.e. we will write u ~< v.

hash h

Declares a function h. This function will correspond to a hash function and therefore is subject to some cryptographic tactics. Its type is message -> message -> message.

Mutable states

mutable s(〈indices〉) : 〈message_type〉 = 〈term〉

Defines a new mutable state and set its initial value.


channel c

Declare a new channel c.


Processes can be declared using process 〈identifier〉p(〈args〉) = 〈process〉.

A process is a built from the following constructs:

The diff operator can be used inside processes, so they are actually biprocesses. A biprocess corresponds to two processes: the left one obtained by projecting each occurrence of diff(t1,t2) to t1, and the right one obtained by performing right projections.


process tag(i:index,k:index) =
  new nT;
  out(cT, <nT, h(nT,diff(key(i),key'(i,k)))>)

process reader(j:index) =
  if exists (i,k:index), snd(x) = h(fst(x),diff(key(i),key'(i,k))) then


A system is declared from a process using the following syntax:

system [name] 〈process〉

This will actually declare name/left and name/right, the two projections of the biprocess.


system [BasicHash] ((!_j R: reader(j)) | (!_i !_k T: tag(i,k))).

When a system is declared, Squirrel transforms the process into a set of actions (with sequential dependencies on actions). Squirrel will group elements of the process to put inside one action:

Some of these fields may be empty.

Each of these actions will have an number of indices (corresponding to indices created by unbounded replications) and a name.

After this, Squirrel returns the set of name of these actions with the sentence:

System 〈system_name〉 registered with actions 〈list_of_action〉.

It is possible to obtain a full description of these actions using the following command:

print system [system_name].

To have clearer names for your action, you can use aliases. These are naming hints added in the system to guide the naming of actions. The syntax is: 〈alias〉 : process

Example : system (out(c,ok) | out(c,ko)) becomes system (A: out(c,ok) | B: out(c,ko)).



A local formula is formed with:

Quantifiers can be grouped, as in forall (i:index,t,t':timestamp), input@t = <n(i),output@t'>.

Global formulas are written with the same quantifiers, but logical connectives are noted ->, /\ and \/. Atoms of global formulas are of the form [phi] (where phi is a local formula) and equiv(u1,...,uN) (where the uI are bi-terms).


Goals (i.e. lemmas) are declared as follows:

local goal [〈system_annotation〉] 〈goal_name〉 : 〈local formula〉.
global goal [〈system_annotation〉] 〈goal_name〉 : 〈global formula〉.

The keyword local can be omitted in the first declaration: goals are local by default. A blank name _ can be used if there is no need to name a goal.

The system annotation indicates with respect to which systems macros should be understood. We first describe the common use:

It is sometimes useful to specify separately the systems for interpreting local formulas and equivalences. The full syntax is [set: <system list>; equiv: <system pair>] where the first component is used for local formulas and the second one for equivalences.


After the declaration of a goal, the proof begins with Proof and ends with Qed.

A proof starts with the initial goal specified by the user. This goal is reduced to subgoals by successive applications of tactics. If no new subgoal is generated, then the goal is proved. When all goals are proved, the proof is complete. Tactics are documented in a separate file.

It is always possible to write proofs as sequences of tactics, but it is useful (for readability and maintainability) to structure proofs as trees, following the goal-subgoal relationship. To this effect, one can use bullets. A bullet is simply a marker, formed by a combination of the signs +-*, that shows where a branch starts. It is used as follows (indentation is not mandatory, and actually ignored by the tool, but recommended):

(* Suppose this first tactic reduces the current goal to two subgoals. *)
(* Each bullet + below marks the beginning of the proof of each subgoal. *)
+ tac2. tac3.
+ tac4.

When a bullet is used for one subgoal, it must be used for all siblings, i.e. all subgoals generated from the same original goal. Bullets can be nested. It is possible to use bullets in parts of the proof but not others.