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

Logic¶

We define here the syntax and informal semantics of our logic independently from protocols and cryptographic constructs.

Types¶

Base types¶

A base type can generally be thought of as a set of bitstrings, though this is a simplified view as we shall see below.

base_type::=bool | message | timestamp | index | ident

Squirrel comes with several built-in base types:

message represents bitstrings;
bool represents a single bit;
timestamp represents the points in a finite execution trace;
index represents an arbitrary finite set used to index unbounded collections of objects.

Additional custom types may be declared by the user using the following declaration:

Declaration type ident [ type_tag+, ]?¶

Declare a new base type called ident. The values of that type are assumed to be encodable as bitstrings. Type tags can optionally be passed to impose assumptions on the type’s implementation.

type_tag::=large | well_founded | finite | fixed | name_fixed_length

Tags have the following semantics:

a type is well-founded when the built-in function symbol < is well-founded on that type, for any $\eta$;
a type is finite if it has a finite cardinal for each $\eta$;
a type is fixed if its interpretation does not depend on $\eta$;
a type is large when random samplings over that type (declared using name) are such that two distinct names have a negligible probability of collision w.r.t to $\eta$;
a type is name_fixed_length if all names over that type sample values of the same length (for a given $\eta$).

Built-ins types come with the following type tags:

message is fixed, well_founded, name_fixed_length and large;
bool, timestamp and index are fixed, finite and well_founded.

The parameter $\eta$ corresponds to the underlying security parameter used in security proofs.

Note

A finite type is still unbounded: the semantics for the type can be any finite set.

Type variables and polymorphism¶

Squirrel supports type polymorphism à la Hindley–Milner in most places (operators, lemmas, …). Type variables are identifiers preceded by a single apostrophe, e.g. 'x.

type_variable::='identtvar_params::=type_variable*

When parametrizing a declaration, type variables are enclosed in brackets, e.g. ['a 'b 'c].

General types¶

General types are derived from base types and type variables using the arrow and tupling type constructors. A type (or part of a type) can be left unspecified using a type hole _, which must then be inferred by Squirrel.

explicit_type::=type_variable | base_type | type -> type | (type * … * type)type::=_ | explicit_type

The most common function symbols have types of the form (b1 * ... * bn) -> b where b1,...,bn and b are base types.

Example: Hash function

A hash function may have type (message * key_ty) -> hash_ty: it takes as input the value to be hashed (of type message) and a key (of type key_ty), and returns a digest of type hash_ty.

Binders and tags¶

A variable is just an identifier. A hole _ can be used as name for a variable which is either unused or whose name does not matter.

variable::=identvar_or_hole::=variable | _

Variable tags restrict a variable’s possible instantiations in various ways.

tag::=const | glob | adv

Currently, only a few different tags are supported. A tagged bound variable (x : t[tag]) restricts x’s instantiations according to tag:

Tag const requires that x is a constant random variable, which does not depend on the random tape nor the security parameter $\eta$.
Tag glob forces x to be a single random variable — said otherwise, x must represent a system-independent random variable ; for example, this excludes any diff-term (e.g. diff(s,t)), or any term with system-specific macros (e.g. output@tau).
Tag adv forces x to be computable by a probabilistic polynomial Turing Machine (PPTM) with access to a dedicated randomness tape. Such machines run in polynomial time w.r.t. to the security parameter and their input length. This tag is used to define adversarial functions, that can be seen as probabilistic polynomial time attackers.

Abstract function declarations cannot rely on tags, but we can declare free variables of axioms using tags, as well as globally quantify using tags.

Example: No guessing of large names

If we assume that n is a name over type message, as message is large, it is a random value long enough w.r.t. to $\eta$ so that it can at best be guessed with negligible probability. A formula modeling that any function symbol computable by a PPTM cannot return the value of n is expressed as Forall att : message -> message [adv], [att(0)=n]. This is in fact a valid global axiom of the logic. We can also express the axiom by using the tag over the free variable of a local axiom, yielding axiom [any] test (att : message -> message [adv]) : att(r)=n.

Squirrel uses the following syntax for binders:

binder::=var_or_hole | (var_or_hole+, : type [tag+]?+,)binders::=binder*

Note

Tags actually correspond to predicates in the logic: for instance, forall (x:ty[const]), phi should be understood as forall (x:ty), const(x) => phi in the theory. Predicates such as const(_) are however not directly accessible in the tool.

Note

Not all binders support tags, e.g. it would be meaningless to declare a function abstraction with a const tag, as in fun(x:int[const])=>t.

A binding declaration x without any attached type (i.e. using directly a var_or_hole) amounts to using a type hole (x:_), which will have to be be inferred by Squirrel.

Example: Type inference for bound variables

In the formula forall (z:message), exists x y, z =x && x=y, which is a valid Squirrel formula, the existential quantification uses the binder x y, which is in fact equivalent to x:_ y:_ or (x,y:_). Here, Squirrel automatically infer the type of the variables from the equalities.

Terms¶

Terms are syntactic expressions that denote probabilistic values (or, more precisely, families of probabilistic values indexed by the security parameter $\eta$, though this can often be ignored). For instance, a term of type message represents a probabilistic value which ranges over messages, and a term of type bool is a probabilistic boolean value.

A term can be

an application term₁ term₂ ; application is left-associative, and the term term₁ term₂ ... term_n corresponds to (...(term₁ term₂) ... term_n);
the application of an infix operator term₁ infix_op term₂, which corresponds to (infix_op) term₁ term₂;
a name term application name_id term_i?, see names (compared to the previous term application, here we must pass as many indices as the arity of the name, that is, the name must be fully instantiated);
the projection term # i of term over its i-th component (term must be a tuple with sufficiently many elements);
a macro term, see macro;
a conditional if term_b then term₀ else term₁ where term_b must be of type bool, and term₀ and term₁ must have the same type (for a conditional over messages, the else branch can be omitted, which stands for else zero);
a term with binders, see term_with_binders;
an identifier, which must be bound by the context (it can for instance refer to a logical variable, an operator or an abstract function symbol);
a diff-term representing several probabilistic values which depend on the system;
a tuple (term₁,...,term_n).

Many tactics use sterm instead of term, which creates less ambiguities in the parser. Note that enclosing a term in parentheses yields a sterm.

Note

Since [BKL23], terms no longer necessarily represent (PTIME) computable values. An example of a non PTIME-computable term is forall (x:message), x = f(x) which tests whether f is idempotent, something that is not necessarily computable even when f is.

Terms with binders¶

term_with_binders::=fun binders => term|quantif binders, term|find binders such that term in term else term?quantif::=forall | exists

Abstractions are of the form fun binders => term where term can use the variables bound by binders. For example, fun (x:type) => term_body is the function that maps a value x of type type to term_body.

Universal or existential quantifications are of the form quantif binders, term where term must be of type bool. For example, one can write exists (x:message), fst(x) = zero.

Multiple binders in an abstraction or quantifier construct represent multiple nested constructs, e.g. fun x y => term stands for fun x => (fun y => term).

A find performs a look-up through all values of a type, filtered according to some predicate, and returning some computation. For instance, if term_b is of type bool and term_i and term_e have the same type, then find (x:type) such that term_b in term_i else term_e looks for some x of type type such that term_b: if such a value exists, it returns term_b, otherwise it returns term_e (terms term_b and term_i can use the variable x, while term_b cannot). If no else branch term is provided, term_e defaults to zero (the zero bit-string).

Multi-terms¶

In several circumstances, we have to manipulate several variants of a term, which only differ in a few places. This happens when proving equivalences, which are typically between minor variations of the same term (e.g., equivalence between an output enc(m,k) and enc(zeroes(m),k)). This also happens when proving the same property for different systems: e.g., an authentication property might initially be identical for all systems, talking generically of a message output@tau, but unfolding this macro will reveal a different meaning for each system.

In order to factorize common parts of such collections of alternatives, and factorize reasoning over them, Squirrel makes use of multi-terms. A k-multi-term is a single syntactic object used to represent k alternative terms. The common part of the terms is simply written as a term, and the distinct parts are expressed using the the diff construct, see diff-terms. The i-th projection of a multi-term t is obtained from t by replacing any subterm of the form diff(t_1,..,t_n) by t_i.

A bi-term is a 2-multi-term.

Note

Currently, multi-terms are restricted to 2-multi-terms in most parts of Squirrel.

There is no syntactic separation between terms and multi-terms: any Squirrel term can be a multi-term (though syntactic checks are performed in some places, when it is necessary that the user provides a single term).

Squirrel heavily uses multi-terms. Most notably, the equivalence between two terms t₁ and t₂ is written equivalence atom equiv(term_bi), where term_bi is any bi-term (i.e. a 2 multi-term) such that its left (resp. right) projection is t₁ (resp. t₂).

Diff-terms¶

diff_term::=diff(term, term)

diff(term₁,term₂) is a diff-term representing a diverging behaviour between the left component term₁ and the right component term₂. Currently, diff-terms can only have two components, hence they can only be used in bi-terms.

Macros¶

Macros are special built-in probabilistic functions defined by induction over the execution trace (i.e. the timestamp type). Applied macros can occur in terms as follows:

macro_id::=identmacro_application::=macro_id term* @ term

The term macro_id term₁ ... term_n @ term_t represents the application of macro symbol macro_id to arguments term₁ ... term_n at a time-point term_t (of type timestamp).

The semantics of a macro symbol macro_id depends on the system in which it is interpreted:

its semantics over a single system, depends on the system definition, see the system-defined macros section.
over a multi-system S₁,...,S_n, it represents a n multi-term, whose i-th component corresponds to the interpretation of the macro over the single system S_i.

Formulas¶

Squirrel features two kinds of formulas: local formulas and global formulas.

Local formulas¶

Local formulas are terms of type bool. They correspond to the embedding of a lower-level logic inside using terms. They can in particular be constructed using the following (standard and Squirrel-specific) logical constructs:

term+=term && term | term || term | term => term | not term|happens(term+,)

Boolean connectives for local formulas are &&, ||, =>, not, where &&, ||, => are used with a right-associative infix notation. Concretely, these are all built-in function symbols.

Not all time-points are actually scheduled in an execution trace. The distinction is made through the happens predicate: happens(term) (where term is of type timestamp) states that term has been scheduled. Then, happens(term₁,...,term_n) is syntactic sugar for happens(term₁)&&...&&happens(term_n).

Global formulas¶

Global formulas are first order formulas, written as follows:

Global boolean connectives ->, /\, \/ are used in infix notation, and have a standard semantics.

A reachability atom [term] holds if term evaluates to true with overwhelming probability.

An equivalence atom equiv(term₁,...,term_n) is formed from a sequence of 2-diff-terms. Its meaning is that the sequence of left projections of the diff-terms is computationally indistinguishable from the sequence of right projections, i.e. any PPTM adversary has at most a negligible probability of distinguishing them.

Note

Compared to the theoretical presentations of the logic, which do not describe diff-terms, Squirrel variables are by default multi-term variables, and can be instantiated by diff-terms. When necessary, the glob variable tag is forced by the tool to forbid diff-terms; this is the case for global quantifications.