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