• Introduction
• Terms
  • Timestamps
  • Macros
• Declarations
  • Nonces
  • Functions and constants
  • Mutable states
  • Channels
  • Processes
• Systems
• Logic
  • Formulas
  • Goals
• Proofs

Introduction

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

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:

• <m1, m2> is a message containing the pair of messages m1 and m2;
• fst(m) and snd(m) are projections of a pair m.

Timestamps

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

• 〈action〉(〈indices〉)
• pred(〈timestamp〉) denotes the previous action during the execution.
• 〈variable〉

Macros

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.

Declarations

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

Nonces

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 :

• name k : message
• name n : index -> index -> message

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 :

• abstract ok : message
• abstract mySucc : message -> message
• abstract id : index -> message
• abstract (~<): message -> message -> boolean

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.

Channels

channel c

Declare a new channel c.

Processes

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

A process is a built from the following constructs:

• in(〈channel〉, 〈variable〉) receive a message from channel and store it in a variable. The attacker is able to choose all inputed messages wrt. the messages they already knows.
• out(〈channel〉, 〈message〉) output a message into channel. The message is added to the knowledge of the attacker.
• 〈process〉 | 〈process〉 create two parallel processes
• !_〈index〉 〈process〉 create a non-bounded number of parallel processes. Each of them is identified by the value of its index.
• if 〈boolean〉 then 〈process〉 else 〈process〉
• try find 〈indices〉 such that 〈boolean〉 in 〈process〉 else 〈process〉 execute the first process with indices checking the boolean or the second process if there are none.
• new 〈name〉 create a new nonce
• 〈mutable_state〉(〈indices〉) := 〈term〉
• null process that does nothing

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.

Example:

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

process reader(j:index) =
  in(cT,x);
  if exists (i,k:index), snd(x) = h(fst(x),diff(key(i),key'(i,k))) then
    out(cR,ok)
  else
    out(cR,ko)

Systems

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.

Example:

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:

• an input;
• some codition;
• some mutable state modifications;
• an output.

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

Logic

Formulas

A local formula is formed with:

• 〈term〉 = 〈term〉
• happens(〈timestamp〉): does the timestamp appears in the execution
• 〈timestamp〉 < 〈timestamp〉 and 〈timestamp〉 <= 〈timestamp〉: order of timestamps
• 〈formula〉 && 〈formula〉, 〈formula〉 || 〈formula〉, 〈formula〉 => 〈formula〉and 〈formula〉 <=> 〈formula〉
• forall (i:index), 〈formula〉 and exists (i:index), 〈formula〉: quantifier over indices
• forall (tau:timestamp), 〈formula〉 and exists (tau:timestamp), 〈formula〉: quantifier over timestamps

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

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:

• A local goal comes with a system annotation that lists systems: it means that the formula is true for each of these systems. Including a bisystem in the list is equivalent to including its two projections.
• For a global goal, the annotation describes the two systems necessary to interpret equivalences: the user must specify a bisystem or two single systems. The local formulas that might appear inside the global formula are then interpreted with respect to the same two systems: they must be true for both of them.

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.

Proofs

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. *)
tac1.
(* 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.