\[\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}\]

Declarations¶

Declarations allow to introduce the various kinds of objects that are used to model protocols and security properties in Squirrel. Declared objects may be purely abstract, carry assumptions, or have a concrete, explicit meaning.

Terms¶

Names¶

Names are used to model random samplings.

name_id::=ident

Declaration name name_id : type ->? type¶

A name declaration name name_id : type_i ->? type_s introduces a new name symbol name_id optionally indexed by type_i and sampling values of type type_s.

Whenever a name n is defined, a corresponding namelength axiom is declared as:

axiom [any] namelength_n : [len (n) = namelength_message]

It states that all names have the same length, given by a constant.

It is required that the indexing type type_i is a finite type, but there are no restrictions over the sampling type type_s.

The sampling distribution used over the sampling type type_s is usually arbitrary — though it can be restricted using type tags.

Two distinct applied name symbols, or the same name symbol applied to two different index values, denote independent random samplings (using the same distribution). This is reflected by the fresh tactic.

Abstract functions¶

Abstract functions model arbitrary functions over which no assumptions are made, apart from the fact that they are deterministic and polynomial-time computable. In other words, their implementation cannot depend on the random tapes, but it may still depend on the security parameter $\eta$. If needed, their behaviour can be restricted further through axioms.

fun_id::=ident | (infix_op)

Declaration abstract fun_id [tvar_params]? : type¶

Declares a deterministic and polynomial-time computable abstract function of type type and named fun_id.

The function can be polymorphic through the optional tvar_params type variable parameters.

An abstract function must be used in prefix notation if its name is an ident, and in infix notation if its name is an infix_op (note the parentheses around (infix_op) in the declaration).

Example

Equality is defined in Squirrel as an axiomatized polymorphic abstract function:

abstract (=) [’a] : ‘a -> ‘a -> bool

Operators¶

Operators are function symbols with a concrete user-defined semantics. An operator’s semantics must be deterministic.

operator_id::=ident | (infix_op)

Declaration op operator_id [tvar_params]? binders : type? = term¶

Declares an operator named op_id, with arguments binders and returning term.

The return type type can be provided, or left to be automatically inferred by Squirrel.

Operator declarations can be polymorphic through the optional tvar_params type variable parameters.

An operator declaration fails if Squirrel cannot syntactically check that its body represents a deterministic value.

An operator must be used in prefix notation if its name is an ident, and in infix notation if its name is an infix_op (note the parentheses around (infix_op) in the declaration).

Built-ins¶

Squirrel features several built-in function symbols with built-in axiomatizations.

if term then term else term, used in terms, may theoretically be viewed as a built-in.
happens(term), pred(term) and init are three function symbols dealing with the timestamp type. Each model instantiates the set of timestamps by specifying which ones actually happen on the given trace, and for all the ones that happen, their total ordering, init refering to a fixed first timestamp and pred being the predecessor function.
The boolean connectors of local formulas are built-ins: true, false, &&, ||, =>, <=> and not.
Comparison functions =, <>, <=, <, >= and >.
A witness function witness.
A dedicated xor symbol along with its zero.
A conversion function from bool to message, of_bool.
Utility constants for failure, fail, and an empty message, empty.
The successor function over natural numbers succ.
The pairing function pair (also noted <x,y>) with its projection functions fst and snd.
A length function for the number of bits in a message, len, as well as a function producing a bitstring of zeroes of the same length as its input, zeroes.

Cryptographic functions¶

Squirrel allows to declare functions modelling standard cryptographic functions with associated cryptographic assumptions.

crypto_ty_arg::=ident : type

Types over which the cryptographic functions operate can be specified using crypto_ty_arg, where ident:type states that the argument named ident is of type type. See the declarations below for a description of which argument names can be provided for each tactic. If no argument is provided for ident, type default to message.

Declaration hash fun_id where crypto_ty_arg+?¶

hash h where m:tym h:tyh k:tyk

declares a keyed hash function with types tyk for keys, tym for messages and tyh for hash digests. It is assumed to satisfy the PRF and known-key collision resistance assumptions.

Enables the use of prf, euf and collision.

Declaration signature fun_id, fun_id, fun_id where crypto_ty_arg+?¶

signature sig, ver, pk where m:tym sig:tysig sk:tysk pk:typk

declares a signature scheme with types tym for messages to be signed, tysig for signatures, tysk for secret signing keys and typk for public verification keys. It is assumed unforgeable against chosen message attacks (EUF-CMA) and satisfying the equation ver(sig(m,sk),m,pk(sk)) = true.

Enables the use of euf.

Declaration aenc fun_id, fun_id, fun_id where crypto_ty_arg+?¶

aenc enc, dec, pk where ptxt:typtxt ctxt:tyctxt rnd:tyrnd sk:tysk pk:typk

declares an asymmetric encryption scheme with types typtxt for plain-texts, tyctxt for cipher-texts, tyrnd for encryption randomness, tysk for secret decryption keys and typk for public encryption keys. It is assumed IND-CCA1 and ENC-KP, and satisfying the equation dec(enc(m,pk(sk)),sk) = m.

Enables the use of cca1 and enckp.

Declaration senc fun_id, fun_id, fun_id where crypto_ty_arg+?¶

senc enc, dec where ptxt:typtxt ctxt:tyctxt rnd:tyrnd k:tyk

declares a symmetric encryption scheme with types typtxt for plain-texts, tyctxt for cipher-texts, tyrnd for encryption randomness and tyk for keys. It is assumed IND-CPA and INT-CTXT, and satisfying the equation dec(enc(m,sk),sk) = m.

Enables the use of cca1, intctxt and enckp.

Declaration ddhcdhgdh fun_id, fun_id ,fun_id? where crypto_ty_arg+?

The group declaration:

ddh g, (^), ( ** ) where group:tyg exponents:tye

declares a group with generator g, exponentation (^) and exponent multiplication ( ** ). The group is assumed to satisfy the DDH assumption when declared with ddh, the CDH assumption with cdh, and the Gap-DH assumption with g:gdh.

Enables the use of cdh, gdh and ddh.

Processes¶

Protocols are modelled as systems, which provide a meaning to macros (e.g., output, cond) used in our logic. Systems are themselves defined through processes written in a dialect of the applied pi-calculus.

Note

The first presentations of Squirrel’s logic relied explicitly on notions of systems, first without state [BDJ+21] and then with state [BDKM22]. The latest presentation [BKL23] does not feature a notion of system, but allows to encode systems through a more expressive logic. So far, the translation from processes to systems has not been formally defined in the literature.

Channels¶

Communications over the network are performed over public channels, identified by a name.

channel_id::=ident

Declaration channel channel_id¶: Declares a channel named channel_id.

Memory cells¶

Processes in Squirrel can use mutable states.

state_id::=ident

Declaration mutable state_id binders : type? = term¶

Declares a memory cell named state_id indexed by arguments binders and initialized to term. Due to technical limitations, Squirrel currently only supports binders of finite type.

The return type type can be provided, or left to be automatically inferred by Squirrel.

Example: State counter

A set of mutable counters indexed by i,j,k, all initialized to zero, may be declared as follows:

mutable counter (i,j,k:index) : message = zero

With this declaration, the following formula is valid:

forall i j k, counter i j k @ init = zero

Processes¶

We first introduce process prefixes, which correspond to basic operations performed by processes:

process_prefix::=new name_id|state_id term*? := term|out(channel, term)|in(channel, term)

The last three prefixes correspond to the update of a memory cell, and input and asynchronous output over a channel. Their semantics is straightforward.

From a process semantics viewpoint, new name samples a new random value. From a logical viewpoint, this is reflected by declaring a new name, indexed by the current replication indices. This is syntactic sugar that can be avoided by manually declaring the needed name symbols with the appropriate arities before the process declaration.

Processes are then built from prefixes using parallel composition, (indexed) replication and conditionals, as well as other common constructs:

The construct A : proc does not have any semantic impact: it is only used to give an alias to this location in the process.

Declaration process process_id binders = proc¶: Declares a new process named process_id with arguments binders and body process.

Systems and actions¶

Squirrel’s logic only deals with systems, which are obtained by translating protocols. Systems are (partially ordered) sets of actions, which correspond to atomic execution steps of a protocol comprising:

the reception of a message input from the (malicious) network;
the verification of an executability condition;
and, if the action is executable, the output of a message to the network.

A system can currently only be defined from a process. For the same reasons that make multi-terms useful, it is useful to define multiple systems at once (i.e., a multi-system) using a process featuring multi-terms.

system_id::=ident

Declaration system [system_id]? process¶

Declare a bi-system whose actions are obtained by translating process, which may use bi-terms. The obtained single systems can be referred to as system_id/left and system_id/right. The left (resp. right) single system corresponds to the process obtained by taking the left (resp. right) projections of all bi-terms appearing in process.

The system name system_id defaults to default when no identifier is specified.

Actions are referred to through identifiers:

action_id::=ident

When translating processes into sets of actions, fresh action identifiers are automatically generated to name created actions. Alternatively, the user can give a naming hint using the alias process construct. Note however that Squirrel may not respect such naming hints.

Internally, an action is defined by:

an action identifier or constructor action_id;
a list of index variables corresponding to surrounding replications and try find constructs;
a term of type bool representing the action executability condition;
a term of type message representing the action output.

Example: Actions corresponding to a process definition

Consider the following system declaration:

abstract one : message.
name n : index -> message.
channel c.

system
(!_i (in(c,x);
if x=zero then
A: out(c,n(i))
else
B: out(c,x)
) | in(c,x); out(c,empty)).

The provided process yields a system with three actions:

action A(i), which on input x checks whether x=zero and outputs n(i);
action B(i), which on input x checks whether x<>zero and outputs x;
and action A1 (automatically named) which checks whether true and outputs empty.

System-defined macros¶

Declaring a system provides a meaning to several macros for the system’s actions. Given an action A(indices) with output value o(x) and condition c(x) over the input x, the following holds:

output@A(indices) = o(input@A(indices));
cond@A(indices) = c(input@A(indices));
input@A(indices) = att(frame@pred(A(indices))).

Other macros have a meaning that does not depend on the specific action:

frame@tau = <frame@(pred tau), exec@tau, if exec@tau then output@tau> provided that tau happens and is not the initial timestamp init (otherwise, frame@tau is empty);
exec@tau = exec@(pred tau) && cond@tau> provided that tau happens and is not the initial timestamp init (otherwise, exec@init is true).

System expressions¶

System expressions describe one or several systems. We first introduce single system expressions:

single_system_expr::=system_id/left | system_id/right

Here, system_id/proj is an unlabelled single system representing the left (if proj = left) or right (if proj = right) component of the bi-system named system_id.

system_expr::=any | system_id | single_system_expr*,

A system expression may be generic (any, corresponding to any system, already declared or not) or specify a fixed list of systems, each of them coming with a label identifying it. When system_id is a multi-system, the system expression system_id corresponds to the list of its single systems, with the labels that they carry in this multi-system. A system expression can also be explicitly formed as single_system_expr₁,...,single_system_expr_n. In this case, the labels are:

ε if n = 1;

left and right if n = 2;

the n first positive integers otherwise.

System contexts¶

system_context::=set: system_expr; equiv: system_expr|system_id

A concrete system context set:S; equiv:P comprises:

a multi-system specified by S used to interpret reachability atoms;
a pair of systems (i.e. a multi-system with two elements) P used to interpret equivalence atoms.

A system_id S can also be used as a system context: it stands for set:S; equiv:S/left,S/right.

Axioms and Lemmas¶

Squirrel supports two kinds of lemmas, one for each kind of formulas: local lemmas for local formulas and global lemmas for global formulas. Similarly, there are local and global axioms. The only difference between a lemma and an axiom declaration is that the former creates a proof-obligation that must be discharged by the user through a proof.

statement_id::=identlocal_statement::=[system_expr]? statement_id_ [tvar_params]? binders : formulaglobal_statement::=[system_context]? statement_id_ [tvar_params]? binders : global_formula

A local statement as described above expresses that the local formula forall binders, formula holds in the context [system_expr] (which defaults to [default]). The statement is named statement_id for future reference.

Similarly, a global statement expresses that Forall binders, global_formula holds in the context [system_context] (which defaults to [default]).

Local and global statements can be polymorphic through the optional tvar_params type variable parameters (they hold for all instances of the given type variables).

Unnamed (local and global) statements can be declared using an underscore _ instead of a statement identifier statement_id.

Declaration local? lemmaaxiom local_statement¶: Declares a new local lemma or axiom.

Declaration global lemmaaxiom global_statement¶: Declares a new global lemma or axiom.

Example: Local axioms and lemmas

We declare an axiom stating that in any system, a pair has a negligible probability of being equal to the constant fail.

axiom [any] fail_not_pair (x,y:message): <x,y> <> fail

Next, we state that in system [default], the adversary never sends the same message twice.

axiom no_repeat t t’ : happens(t,t’) => t <> t’ => input@t <> input@t’

Finally, the following unnammed local lemma states that, for the single system myProtocol/left, action A2 can execute only if the adversary sends the message ok at time-point A1:

lemma [myProtocol/left] _ : cond@A2 => input@A1 = ok

Example: Global lemmas

The next (typical) global lemma states that the two projections of the bi-system myProtocol are observationally equivalent:

global lemma [myProtocol] obs_equiv (t:timestamp[const]) : [happens(t)] -> equiv(frame@t)

As a slight variant, we now state that real/left and ideal/right are observationally equivalent, this time using only real/left to interpret [_] atoms (which does not change anything in that case since happens(_) does not depend on the details of system actions):

global lemma [set: real/left; equiv: real/left,ideal/right] ideal_real_equiv :
Forall (tau:timestamp[const]), [happens(tau)] -> equiv(frame@tau)