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

Typing for secrecy¶

This section describes the typing tactic enabled by set securityTypes = true. The user must give types when declaring names and mutable states describing which messages are public or secret. Then, Squirrel will type-check all systems in the file when they are defined. Finally, the typing tactic proves that a public term, i.e., a message possibly known by the attacker, cannot be equal to a secret term.

Note

This tactic implements the work published in [DHL25].

Flag securityTypes¶: Allows to declare security types and to use the typing tactic.

Types¶

Types used to express security guarantees are different from the usual types defined by the @type production. They do not replace them, but are used in addition to them.

To typecheck a term, the user must have assigned a security type to some base elements of that term (i.e. names and mutable states). There are two kinds of security types: types for messages and types for keys.

A message type describes the level of knowledge the attacker may have on a term with that type.

Msg is the most general type: it does not give any guarantee.
High means the term is secret: its exact value cannot be computed from public values (except with negligible probility). However, some bits of information about it could be publicly available.
Low is the type of a value that may be published.
Bool is the type of a boolean value. These values are always public.
Cst c designates a term overwhelmingly interpreted as the constant c. The identifier c must designate an abstract function with a type of the form index ->* message.
T_1 * T_2 designates a pair of a term of type T_1 and one of type T_2.
T_1 + T_2 is a sum type: a term of this type will be a term of type T_1 in some executions, and of type T_2 in others.

key_type::=SK[fun_id, message_type]|AK[fun_id, message_type]|SSK[fun_id, message_type]

A key type describes an honest uncompromised key for encryption/signature:

SK[f, T] is a symmetric encryption key. T is the type of the plaintexts that can be encrypted with this key. f must be the associated encryption function, declared using senc.
AK[f, T] is an asymmetric encryption private key. T is the type of the plaintexts that can be encrypted with this key by honest agent in the protocol. f must be the associated encryption function, declared using aenc.
SSK[f, T] is a signature private key. A signature with this key ensures the signed message is of type T. f must be the associated signature function, declared using signature.

security_type::=message_type|key_type|Rand

A security type is either a message type, a key type, or Rand, a special type reserved for randomness used when encrypting. To encrypt a message typed T with a key typed SK[f, T] or AK[f, T], the randomness given to the encryption function must be typed Rand. The type system checks, among other conditions, that the same random is not used twice.

Typing algorithm¶

The typing procedure does not support all features of Squirrel’s language. In particular, it cannot consider terms with user-defined types, higher-order, or names and mutable states with non-index arguments.

The typing procedure is sound w.r.t the type system described in [DHL25], but it is not complete. One notable source of incompleteness is a rule of the type system that allows, when a variable is known to be of type T_1 + T_2, to perform a case disjunction, and continue the typechecking twice, assuming first that the variable has type T_1, and then T_2. One must be careful when applying that rule, since it may lead to the same randomness being apparently used in different encryptions, once in each branch of the proof. Typing may thus require a subtle use of that rule to break sums. The implemented algorithm relies on a heuristic to decide when to apply it, which is not complete. As much as possible, when typechecking fails because of the heuristic, the error message reports it.

Declarations¶

The flag securityTypes modifies the syntax and/or behaviour of some declarations. Once it is set to true, the user can add security types to name and mutable state declarations.

Name declarations¶

Declaration Variant name name_id : type ->? type , security_type?: A name declaration name name_id : type_i ->? type_s introduces a name symbol name_id, with a user-defined security_type. The same constraints on type_i and type_s as on normal name declarations apply. A name can only be declared with types Low, High, Rand, or a @key type. Additionally, a security type other than Low can only be declared if the type in which the name is sampled is tagged large.

State declarations¶

Declaration Variant mutable state_id binders : typesecurity_typetype, security_type? = term

Declares a mutable state with a user-defined @security_type. The same restrictions on binders and type as usual apply.

When using a security_type, type must be message.

If the term provided as initial value cannot be typed with the given security_type, then the mutable state state_id is not well-typed. Since, when declaring a state, action init is updated in all systems to set its initial value, any past or future system immediately stops being well-typed as well, and a warning is displayed to the user.

Protocol declarations¶

The syntax for protocol declarations is unchanged. However, each system is typechecked when it is declared. The typechecker ensures all outputs are Low, all conditions are Bool, and each update of a mutable state sets it to a value of the expected type, provided at the state’s declaration. These verifications are performed separately on each projection of the system, unless the system does not use the diff operator, in which case it is only typechecked once.

When declaring a system, some proof obligations may be opened. Indeed, to typecheck some terms, the type system may need to assume that some constants with different symbols are different – typically, constants used as tags to distinguish protocol messages. If the typechecker makes this assumption, and cannot automatically prove it holds, it opens a subgoal asking the user to prove it, before declaring the system to be well-typed.

The typing tactic is enabled in all well-typed projections of a system, but is unavailable in projections where the typechecking failed. In that case, a message describing the action in which the error occurred is displayed.

Tactic¶

Tactic typing hypothesis_id¶

This tactic applies to a hypothesis of the form t_1 = t_2. The current goal’s system_context must specify a set consisting in a finite number of well-typed (projections of) systems. The tactic attempts to give t_1 the type Low and t_2 the type High, or vice-versa if that first attempt fails, in each system of the set. These typing derivations cannot use encryption randomness, of type Rand.

The typing tactic does not unfold macros, and it may thus be necessary to unfold global macros and conditions manually.

Like for protocol declarations, typechecking can open subgoals:

Again, if typechecking t_1 and t_2 requires the assumption that some constants are different, a proof obligation is generated for it.
If a subterm of the form output@tau appears in t_1 or t_2, the user must prove that it appears under a condition that implies exec@tau.
If a mutable state s@tau appears in t_1 or t_2, the user must prove that it appears under a condition that implies happens(tau).

In these subgoals, not all hypotheses from the original proof context are sound to keep, according to the soundness proof of the type system in [DHL25]. The tactic only keeps global hypotheses, and local hypotheses that are either [const] or of type Bool in the type system.

If typechecking succeeds, the hypothesis hypothesis_id is contradictory, and typing closes the original goal. If typechecking fails in one or more systems, the tactic fails, and displays the errors obtained by both attempts at typing (t_1:Low/t_2:High and the converse).