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

Proofs¶

The proof of a lemma is given after the lemma declaration, between the Proof and Qed markers. It consists in a list of tactics. The invocation of each tactic modifies the proof state, which contains a list of goals to prove. Each goal is displayed as a judgement. Initially, the proof state consists of a single goal, as declared by the user. Each tactic then reduces the first goal of the proof state to an arbitrary number of new sub-goals. When no goal is left, the proof is completed and Qed can be used.

The complete list of tactics can be found in the corresponding tactic index.

Judgements¶

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

Logical variables¶

Logical variables are free variables in a current goal. Such variables are implicitly quantified universally based on their type and tags.

Hypotheses¶

Hypotheses are referred to by a hypothesis identifier hypothesis_id.

hypothesis_id::=ident

Local judgement¶

The general layout for a local judgement is as follows:

System: currentSystem
Type variables: tvars
Variables: vars
H_1: hypothesis_1
…
H_k: hypothesis_k
——————————————
conclusion

The judgement asserts that the conclusion below the line holds in the context given above the line. We now describe the various components of the judgement:

the system currentSystem is a system_expr in which the judgement’s formulas should be understood;
tvars are the judgement’s type variables;
vars are the judgement’s term variables with their types and tags;
each hypothesis is identified by its hypothesis identifier (e.g. H_1, H_2) and is either a global hypothesis, whose body is a global formula, or a local hypothesis, whose body is a local formula;
conclusion is a local formula.

Global judgement¶

The general layout for a global judgement is similar to the local one except that now:

currentSystem is a system_context;

all hypotheses, as well as the conclusion, are global formulas.

When the conclusion is a single equiv(term,...,term) predicate, all the bi-terms that need to be proved equivalent are displayed as a numbered list.

Example: Initial judgement for observational equivalence

Consider a lemma for observational equivalence, where the frame is enriched with some public key, as follows:

global lemma [myProtocol] obs_equiv t : [happens(t)] -> equiv(frame@t, pk(sk))

When starting its proof, after doing intro H, the goal that the user must prove is displayed as:

[goal> Focused goal (1/1):
Systems: left:myProtocol/left, right:myProtocol/right (same for equivalences)
Variables: t:timestamp[glob]
H: [happens(t)]
—————————————-
0: frame@t
1: pk (sk)

Generalities¶

Tactic arguments¶

Tactics that apply to judgements whose conclusion is an equivalence may take a natural number as argument to identify one item in the equivalence. This is represented using the position token.

position::=natural

Many tactics expecting a term support term patterns, which are underspecified terms that can include term holes _. Most tactics will match the pattern against sub-terms of the current goal until it manages to infer values for the term holes.

Term patterns are produced by appending to the production of term and sterm the hole construct:

term_pat::=…|_sterm_pat::=…|_

Intro patterns¶

Introduction patterns are the principal tool used to do proof-context book-keeping. They are used in Squirrel with an SSReflect-inspired syntax. For a more comprehensive and detailed guide to introduction patterns, see here. Note however that Squirrel supports only a sub-set of SSReflect intro patterns, and that their behaviour in Squirrel may vary in small ways.

Introduction patterns take a different meaning depending on the tactic in which they are used (intro, have, destruct, …). Nonetheless, a introduction pattern always applies to a set of focused formulas (sometimes taken in a judgement, with a full proof-context) which they modify. A introduction pattern may create or remove focused formulas. Most introduction patterns act only on the top-most variables or assumptions of the focused formulas (e.g. if the formula is forall x. G or H => G then the pattern will start by acting on x or H).

naming_ip::=_?identand_or_ip::=[][ simpl_ip+ ][ simpl_ip+| ]simpl_ip::=naming_ipand_or_iprewrite_ips_item::=///=//=rewrite_ip::=-><-expand_ip::=@/macro_idoperator_idclear_switch::={ hypothesis_id+ }intro_pat::=simpl_ip | s_item | expand_ip | clear_switch | * | >

A naming introduction pattern naming_ip pops the top-most assumption or universally quantified variable of the focused formula and introduces it in the proof context, with a name chosen according to the pattern:

ident: using the name ident provided, which fails if ident is already in use;
?: using a name chosen automatically by Squirrel;
_: using an automatically chosen name for variables, and the name _ for assumptions, which is a special name that can never be referred to by the user. Note that, contrary to other hypothesis_id, several hypotheses may be named _.

A and/or introduction pattern and_or_ip will, for each focused formula, destruct the top-most assumption of the formula:

[ simpl_ip ... simpl_ip ]: the top-most assumption of the formula must be a conjunction with as many conjuncts as simple patterns are provided. Destruct the conjunction, handling each conjunct according to the corresponding simpl_ip.
[ simpl_ip | ... | simpl_ip ]: the top-most assumption of the formula must be a disjunction with as many disjuncts as simple patterns are provided. Destruct the disjunction, creating a formula for each disjunct and handling each of them according to the corresponding simpl_ip.

Note

Existentials are viewed as conjunctions in intro patterns. Hence, when the conclusion is of the form (exists x, phi) => psi, the tactic intro [x H] will introduce a variable x and hypothesis H : phi. Here, the conjunctive intro pattern has been used to destruct the existentially quantified hypothesis during its introduction.

A simplification item s_item simplifies the focused formulas:

// removes all formulas on which auto concludes;
/= simplifies all formulas using simpl;
//= is short-hand for // /=;

A rewrite intro pattern item rewrite_ip uses the top-most assumption to rewrite the focused formulas. The top assumption is cleared after rewriting.

-> reads the top-most assumption as a left-to-right rewrite rule.
<- reads the top-most assumption as a right-to-left rewrite rule.

An expansion item expand_ip expands definitions in the focused formulas:

@/macro_id expands the applications of the macro symbol; macro_id whenever it is applied to a time-point that can be shown to happen;
@/operator_id expands the operator operator_id, $\beta$-reducing the operator if it is applied.

A clear switch clear_switch clears the specified hypotheses from the proof context.

Proof terms¶

Proof terms are used by several tactics (see e.g. have or apply) as a convenient way to combine and (partially) apply hypotheses, axioms or proved lemmas, in order to derive new facts.

proof_term::=ident pt_arg*pt_arg::=sterm_pat | ident | (% proof_term) | _

In a proof_term or a pt_arg, an identifier ident must refer to a hypothesis in the current proof context, an axiom or a previously proved lemma.

Note that the grammar for proof term arguments pt_arg is ambiguous (because of the ident and sterm productions). When this happens, Squirrel tries to desambiguate using the context.

Note

The (% proof_term) syntax is experimental, and is subject to change in the future.

Proof-term resolution¶

A proof-term ident pt_arg₁ ... pt_arg_n is resolved into a local or global formula as follows:

First, the proof-term head ident is resolved as a local_formula or global_formula F.
Then, this local or global formula F is successively modified by applying to it the arguments pt_arg₁ ... pt_arg_n, in order, as follows:
- sterm_pat: the top-most element of F must be a universally quantified variable, which is then substituted with sterm_pat, e.g. forall x, F0 is replaced with (F0{x -> sterm}). Moreover, a new term unification variable is created for each hole _ in sterm_pat.
- ident: the top-most element of F must be an assumption, which is popped and unified with the formula corresponding to the hypothesis, axiom or lemma identified by ident.
- (% proof_term): the proof-term argument proof_term is recursively resolved into a formula, which is then unified with the top-most element of F.
- _: if F’s top-most element is a universally quantified variable then a new unification variable is created and applied to F. If F’s top-most element is an assumption H, a new sub-goal requiring to prove H is created and must be discharged by the user.
Finally, depending on which tactic uses the proof-term, Squirrel checks that the term unification variables can all be inferred, generalizes the term unification variables that remain, or leaves the term unification environment unclosed.

In practice, the application of a proof-term argument is more complex than described above, for several reasons:

checks must be perfomed to ensure the compatibility of the systems corresponding to the applied formulas, e.g. applying an axiom over system [any] to a formula over system [default] is valid, but the converse is not;
some formula manipulations occur when trying to mix global and local formulas, e.g. when applying a global formula to a local formula.

Reduction¶

Several tactics (e.g., simpl and auto) rely on a reduction engine. This engine repeatedly applies several transformations, corresponding to the following flags.

simpl_flags::=~flags:[ rwbetaprojdeltaconstr*, ]

Leaving the flags unspecified results in the rw, beta and proj transformations being used. Specifying an empty list of flags results in no transformations being applied. Otherwise, only the specified transformations are applied, as described next:

rw: perform user-defined rewriting;

beta: perform beta-reductions;

proj: compute tuple projections;

delta: replace macros and operators with their definitions;

constr: automatically simplify trace formulas using constraint reasoning.

The constr transformation replaces trace (sub-)formulas that are provably equal to true or false with that value. When doing so, the constraint solver takes into account the current hypotheses but also the conditionals that surround the trace formula.

The user-defined rewriting transformation eagerly applies the rewrite rules added to the rewriting database using the hint rewrite command.

Automatic simplification tactics¶

There are three automated tactics. The autosimpl tactic is called automatically after each tactic, unless the tactical nosimpl is used.

Tactic auto simpl_flags?¶

Attempt to automatically prove a goal using the hypotheses.

The tactic uses the reduction engine with the provided flags (defaults to rw,beta,proj).

Moreover, for local goals, the tactic relies on basic propositional reasoning, rewriting simplications, and both constraints and congruence.

Error cannot close goal¶: The current goal could not be closed.

Tactic autosimpl¶

Simplify a goal, without closing it.

The tactic uses the reduction engine with the flags rw,beta,proj.

When the conclusion of the goal is a conjunction, it splits the goal into several sub-goals, automatically closing only the trivial goals proved by true and assumption.

When the conclusion of the goal is a global formula which only contains a local formula, the goal is then turned into a local formula. Otherwise the tactic does nothing.

Tactic simpl simpl_flags?¶

Simplify a goal and its hypotheses. This tactic always succeeds, replacing the initial goal with a single simplified goal.

The tactic uses the reduction engine with the provided flags (defaults to rw,beta,proj).

When the goal is a conjunction, the tactic will attempt to automatically prove some conjuncts (using auto) and will then return a simplified sub-goal without these conjuncts. In the degenerate case where no conjunct remains, the goal will be true.

When the conclusion of the goal is an equivalence, the tactic will automatically perform fa when at most one of the remaining sub-terms is non-deducible. It may thus remove a deducible item from the equivalence, or replace an item <u,v> with u if it determines that v is deducible.

Tactics¶

The full syntax of tactic combinations is as follows:

Tactic combinators behaves as follows:

the semi-column ; is used for judgemential composition. The second tactic is applied to all sub-goals created by the first one, unless the indices of some sub-goals are specified using a tac_selector.
A different tactic can be applied to different sub-goals, for example tactic; [1: tactic₁ | 3,4: tactic₂] applies tactic₁ to the first created sub-goal, and tactic₂ to the third and fourth sub-goals.
The + combinator performs an or-else, i.e. tries applying the first tactic, and if that fails, applies the second one.

The remainder behaves as follows:

Tactic by tactic¶: Fail unless the tactic closes the goal.

Tactic nosimpl tactic¶: Call the given tactic without the implicit use of simplifications. This can be useful to understand what’s going on step by step. This is also necessary in rare occasions where simplifications are actually undesirable to complete the proof.

Tactic try tactic¶: Try to apply the given tactic. If it fails, succeed with the sub-goal left unchanged.

Tactic repeat tactic¶: Apply the given tactic, and recursively apply it again on the generated sub-goals, until it fails.

Tactic tactic => intro_pat_list: intro_pat_list::=intro_pat*
tactic => intro_pat_list is equivalent to tactic; intro intro_pat_list

Common errors¶

Error Out of range position.¶: Argument does not correspond to a valid equivalence item.

Error Assumption not over valid system¶: Trying to use a proof term that does not apply to the current system.

Tactics¶

Tactics are organized in three categories:

generic tactics, that rely on generic logical reasoning;

structural tactics, that rely on properties of protocols and equality;

cryptographic tactics, that rely on cryptographic assumptions.

In addition, they are also split between tactics applicable to local goals only, global goals only, or tactics common to both types of goals. Remark that applying a tactic to a local goal may produce a global sub-goal, and conversely.

Additionally, there are a few utility tactics listed at the end.

Generic tactics¶

Common tactics¶

Tactic admit position?¶: Admit the current goal, or admit the element at position position when the goal is an equivalence.

Tactic assumption hypothesis_id?¶: Conclude if the conclusion of the current goal (or false) appears in the hypotheses. The hypothesis to be checked against may be directly specified using hypothesis_id.

Tactic case hypothesis_idterm_pat¶

Perform a case analysis over the given argument:

hypothesis_id: create one sub-goal for each disjunct of hypothesis_id;
term_pat a term of type timestamp: create one sub-goal for each possible action constructor of the current goal’s system (all systems appearing in a judgement have the same set of actions, as they must be be compatible).

Tactic induction @system:expr_annot? term_pat?¶

Apply the induction scheme to the conclusion. The behaviour of the tactic depends on the type of the current goal, and whether the optional arguments are given.

For a local goal, if no argument is specified, the conclusion must start with a universal quantification over a well-founded type and the induction is performed over the first quantified variable. If a term is manually specified, the goal is first generalized (see generalize) w.r.t. that term, understood in system expr_annot. Only then is the induction applied.

For a global goal, an argument must always be specified, and,

if the given term is a timestamp variable, a weak induction is performed over this variable, as well as a case disjunction over all possible actions;

for any other term argument, the tactic behaves as in the local case.

The weak induction variant is in fact the most widely used tactic in current Squirrel examples to prove the observational equivalence of a protocol.

Example: Induction for observational equivalence.

Over a goal of the form

[goal> Focused goal (1/1):
Systems: left:myProtocol/left, right:myProtocol/right (same for equivalences)
Variables: t:timestamp[glob]
H: [happens(t)]
—————————————-
0: frame@t

Calling induction t will apply the weak induction and case disjunction, yielding as many goals as there are actions in the protocol, plus one additional goal for the initialization. Assuming an action A is in the protocol, that has a total of 3 actions, a sub-goal created for the case of A looks like

[goal> Focused goal (1/4):
Systems: left:myProtocol/left, right:myProtocol/right (same for equivalences)
H: [happens(A)]
IH: equiv(frame@pred (A))
—————————————-
0: frame@A

Tactic dependent induction @system:expr_annot? variable?¶

Apply the induction scheme to the conclusion. If no argument is specified, the conclusion must be a universal quantification over a well-founded type. Alternatively, a term of a well-founded type can be given as argument, in which case the goal is first generalized in the dependent variant (see generalize dependent) before proceeding with the induction.

This tactic always uses a strong induction principle (as opposed to the induction tactic, which performs a weak induction when the conclusion is an equivalences).

Tactic destruct hypothesis_id as simpl_ip?¶

Destruct a hypothesis based on its top-most connective (existential quantification, disjunction or conjunction), applying the simple introduction pattern simpl_ip to it.

simpl_ip defaults to ? if no pattern is provided by the user.

Example: Destruct

If we have the hypothesis H: A \/ (B /\ C), the tactic

destruct H as [H1 | [H2 H3]]

removes the H hypothesis and creates two sub-goals, one with the hypothesis H1:A, the other with the hypotheses H2:B, H3:C.

Tactic exists term*¶

exists term₁ ... term_n uses the terms term₁ ... term_n as witnesses to prove an existentially quantified conclusion.

For example, exists t transforms the conclusion of a goal (exists x, phi) into (phi{x -> t}).

Tactic generalize @system:expr_annot? term_pat+ as variable+?¶

generalize @system:expr_annot term_pat looks in the conclusion of the sequent for an instance term of term_pat understood in system @expr_annot. Then, it replaces all occurrences of term in the conclusion with a fresh universally quantified variable (automatically named, or variable if provided).

The @system argument, which specifies in which system the given terms are to be understood, is optional. If no system is provided, terms are by default understood in the current goal’s set for a local goal, and in its equiv in global goals.

Tactic generalize dependent @system:expr_annot? term_pat+ as variable+?¶: Same as generalize, but also generalizes in the proof context. All hypotheses in which generalization occurred are pushed back into the conclusion before the newly added quantified variables.

Tactic have have_ip : termglobal_formula¶

have_ip::=s_item* simpl_ip s_item*

have have_ip : F introduces the new hypothesis F, which can be a term or a global_formula. The new hypothesis is processed by have_ip (see below). A new sub-goal requiring to prove F is created.

If have_ip is the introduction pattern s_item_pre simpl_ip s_item_post then:

the simplification item s_item_pre is applied to the conclusion before adding the hypothesis;
the simple intro-pattern simpl_ip is applied to introduce the new hypothesis F;
the simplification item s_item_post is applied to the conclusions after adding the hypothesis.

It there are mutliple pre or post simplification items, they are applied in order.

Tactic assert term as simpl_ip?¶: This is an alternative syntax for have simpl_ip : term, where simpl_ip defaults to ?.

Tactic have have_ip := proof_term¶: have have_ip := proof_term resolves proof_term — requiring that the term unification enviroment is closed — and processes the resulting formula using introduction pattern have_ip.

Tactic apply proof_term¶

Backward reasoning tactic. First, proof_term is resolved as a formula F_pt — without closing the term unification environment. Then, it is unified with the conclusion, and finally the term unification environment is closed.

If the unification of F_pt with the conclusion fails, the tactic introduces the top-most element of F_pt as described below, and then tries again to unify with the conclusion:

if it is a variable (i.e. F_pt = forall x, F), it introduces a new term unification variable x and continues from F;
if it is an assumption (i.e. F_pt = G => F), the assumption G is discharged as a new sub-goal, and the tactic continues from F.

Tactic apply proof_term in hypothesis_id¶

Forward reasoning variant of apply, which unifies the premisses of proof_term against the conclusion of hypothesis_id, replacing hypothesis_id content with proof_term’s conclusion.

For instance, if H1:A=>B and H2:A, then apply H1 in H2 replaces H2:A with H2:B.

Tactic rewrite rw_arg* in rw_target?¶

rw_arg::=s_itemrw_itemrw_item::=natural? !?? -? (proof_term)/ident/( infix_op)/*rw_target::=hypothesis_id*

Apply a sequence of rewriting and simplification items to the rewrite target, which is:

the hypothesis hypothesis_id if rw_target = hypothesis_id;
all hypotheses if rw_target = hypothesis_id;
the conclusion if no specific rewrite target is given.

Rewrite items are applied as follows:

proof term rewrite item proof_term:
- It is first resolved — without closing the term unification environment — as a local formula F or global formula [F] where F = forall x1...xn, H1=>...=>Hn=> l = r. At that point, l and r are swapped if the rewrite item is prefixed by -.
- Then, Squirrel tries to unify l with a sub-term of the rewrite target, where x1...xn are handled as term unification variables. If it succeeds, all occurrences of the matched instance of l are replaced with the corresponding instantiation of r.
- The term unification environment is closed, and new sub-goals are created for the instantiated assumptions H1,...,Hn.
expansion items /ident and /( infix_op) tries to expand the corresponding symbol (see expansion item), while /* tries to expand all possible symbols;
! applies the rewrite item as many times as possible, but at least once, while (natural !) applies the rewrite item exactly natural times. ? behaves as !, except that the rewrite item may be applied zero times. Otherwise, the rewrite item must be applied exactly once.

Error rule bad systems¶: Rewrite item applies to a system which is not compatible with the rewrite target.

Error nothing to rewrite¶: No instance of the rewrite rule were found.

Error max nested rewriting reached¶: There were too many nested rewriting. This is to avoid infinite rewriting loops.

Tactic id¶: The identity tactic, which does nothing. Sometimes useful when using tactic combinators.

Tactic intro intro_pat+¶: Introduce the top-most assumptions and universally quantified variables of the conclusion as specified by the given introduction patterns.

Tactic clear ident*¶

clear id drops the specified hypothesis, variable declaration or definition, as long as id is not used elsewhere in the sequent.

clear id1 ... idN is syntactic sugar for clear id1; ...; clear idN.

Calling clear without arguments clears all possible unused variable declarations and definitions.

Tactic reduce simpl_flags?¶

Reduce all terms in a goal, working on both hypotheses and conclusion.

This tactic always succeeds, replacing the initial goal with a unique sub-goal (which may be identical to the initial one).

The tactic uses the reduction engine with the provided flags (defaults to rw,beta,proj).

Tactic remember term_pat¶: remember behaves as generalize, except that it adds as a hypothesis the equality between the generalized term and the new variable.

Tactic revert hypothesis_id*¶

Remove the hypotheses from the proof context, and add them back into the conclusion of the goal.

For example, running revert H on the judgement H : F, Γ ⊢ conc yields Γ ⊢ F => conc.

Tactic left¶: Reduce a goal with a disjunction conclusion into the goal where the conclusion has been replaced with the first disjunct. That is, left turns Γ ⊢ F || G into Γ ⊢ F.

Tactic right¶: Reduce a goal with a disjunction conclusion into the goal where the conclusion has been replaced with the second disjunct. That is, right turns Γ ⊢ F || G into Γ ⊢ G.

Tactic split¶: Split a conjunction goal, creating one sub-goal per conjunct. For example, split replaces the goal ⊢ F && G && H with the three goals ⊢ F, ⊢ G and ⊢ H.

Tactic use hypothesis_id with term+? as simpl_ip?¶: Instantiate a lemma or hypothesis using the provided arguments (if any). An introduction pattern can also be specified to handle the new hypothesis.

Warning

This tactic is a deprecated (and less powerful) variant of the have tactic (with the have have_ip := proof_term form).

Local tactics¶

TraceTactic true¶: Close a goal when the conclusion is (syntactically) true.

Global tactics¶

EquivTactic byequiv¶: Transform a global judgement ⊢ [F] into a local judgement ⊢ F.

EquivTactic constseq position: (fun binders => term) term+¶

Simplify a sequence at the given position when it only contains a finite number of possible values v_1,…, v_i depending on the value of the sequence variable.

Given a sequence over a variable of a given type, the arguments passed must be of the form (fun_1 v_1) ... (fun_i v_i), where all the fun functions must be binders over the sequence type and must return a boolean. This tactic creates two sub-goals asking to prove the two required properties of the arguments and sequence:

All the functions must be such that for any given input element, exactly one of the functions returns true.
The sequence is then expected to be equal to the value of v_i for all input elements such that fun_i is true.

Example: Constseq one or zero

Consider the following conclusion for a global goal 0: seq(t':timestamp=>(if (t' < t) then one)) (assuming that t' is a free timestamp variable).

It is clear that this sequence only returns one or zero (zero is in the implicit else branch). It can then be simplified by calling the tactic:

constseq 0:
(fun (t’:timestamp) => t’ < t) one)
(fun (t’:timestamp) => not (t’ < t)) zero).

This replaces in the current goal the constant by zero and one, and creats two sub-goal, asking to prove the two following formulas:

forall (t’:timestamp),
(fun (t’:timestamp) => t’ < t) t’
|| (fun (t’:timestamp) => not (t’ < t)) t’

(forall (t’:timestamp),
(fun (t’:timestamp) => t’ < t) t’ => if (t’ < t) then one = one) &&
forall (t’:timestamp),
(fun (t’:timestamp) => not (t’ < t)) t’ => if (t’ < t) then one = zero

EquivTactic enrich term+,¶: Enrich the conclusion of an equivalence goal with the given terms. Note that this changes the positions of items in the equivalence, and if added before other tactics may break later references.

Tactic localize hypothesis as simpl_ip¶

Change a global hypothesis containing a reachability formula [term] to a local hypothesis term, and applies the given simple introduction pattern simpl_ip to the new hypothesis.

For example, the tactic turns [F],G ⊢ H into F,G ⊢ H.

EquivTactic memseq¶: Prove that a bi-frame element appears in a sequence of the bi-frame.

EquivTactic refl¶: Close a goal by reflexivity. Cannot apply if the goal contains variable or macros, as those may have different left and right behaviours.

EquivTactic sym¶: Swap the left and right system of the equivalence goal.

EquivTactic trans ~left~right? @system : single_system_expr? position : term*,¶

Prove an equivalence by transitivity.

Used when proving a goal equiv(u), where u is a sequence of terms whose left and right projections are u_l and u_r, in a system context equiv: S_l, S_r. The tactic introduces an intermediate sequence u_m and system S_m and splits the goal in two, asking to prove first the equivalence of u_l and u_m in context equiv: S_l, S_m, and then the equivalence of u_m and u_r in context equiv: S_m, S_r.

The sequence u_m is constructed by taking u_l or u_r, depending on the ~left or ~right parameter, and replacing in it the elements at the specified positions with the terms given as parameter. By default, ~right is used.

The system S_m in which u_m is understood is the one given as parameter. By default, S_l is used when ~left is specified, and S_r when ~right is.

In the resulting goals, the set of the system context is set to be equal to the equiv.

Example: Transitivity on terms

If the conclusion of the goal to prove is

0:diff(a,a’)
1:diff(b,b’)
2:diff(c,c’)

then calling trans ~left 1:d, 2:e will produce the intermediate terms u_m = 0:a, 1:d, 2:e, and use the intermediate system S_l.

The conclusions of the resulting goals will then be

0:diff(a,a)
1:diff(b,d)
2:diff(c,e)

and

0:diff(a,a’)
1:diff(d,b’)
2:diff(e,c’)

to be proved respectively in contexts equiv: S_l, S_l and equiv: S_l, S_r.

Example: Particular case to change systems

In particular, when no indices and terms to modify are specified, only the system changes. For instance, when proving equiv(frame@tau) in equiv: S1, S2, one may call trans @system:S3, resulting in two goals asking to prove equiv(frame@tau), first in equiv: S1, S3, and then in equiv: S3, S2.

EquivTactic trans system_context

Prove a goal by transitivity on systems. This tactic transposes the current equivalence goal in a different system context.

When proving that u ~ v in equiv:S1,S2, calling trans [S3, S4] will split the goal in three, asking to prove that

u ~ u in equiv:S1,S3

u ~ v in equiv:S3,S4

v ~ v in equiv:S4,S2

The set of the system context will be unchanged in the first and third of these goals, and set to S3,S4 (the same as the equiv) in the middle one.

A set can even be specified when calling the tactic, e.g. trans [set:S5; equiv:S3,S4], in which case that set will be used for the middle goal (the others remain unchanged).

This tactic can be seen as a particular case of the trans @system tactic described above, performing two transitivity steps without changing the terms (roughly trans ~left @system:S3 followed by trans ~right @system:S4).

EquivTactic splitseq position: (fun binders => term)¶

Split a sequence according to some boolean test, replacing the sequence with two subsequences.

The function passed as argument must be take as argument a variable of the same type as the sequence, and must return a boolean.

Example: Splitting a sequence

Called in a goal with a conclusion of the form 0: seq(x:message => value), the tactic:

splitseq 0: (fun y:message => some_test)

replaces the conclusion with:

0: seq(x:message=>
(if (fun y:message => some_test) x then
value))
1: seq(x:message=>
(if not ((fun y:message => some_test) x) then
value))

Structural tactics¶

Common tactics¶

Tactic constraints¶: Attempt to conclude by automated reasoning on trace literals. Literals are collected from hypotheses, both local and global, after the destruction of conjunctions (but no case analysis is performed to handle conjunctive hypotheses). If the conclusion is a trace literal then it is taken into account as well.

Tactic depends timestamp, timestamp¶

If the second action depends on the first action, and if the second action happens, then add the corresponding timestamp inequality.

Error Not dependent¶: The two actions are not dependent, i.e. were not derived from two outputs in sequence in the source process.

Tactic expand macro_id | macro_application+,¶: Expand all occurences of the given macros in both the conclusion and proof-context, either fully specified with an action or simply a type of macro.

Tactic expandall¶: Expand all possible macros in the current proof-context and conclusion.

Tactic fa positionfa_arg+,¶

fa_arg::=!?? term_pat

Apply the function application rule, simplifying the goal by removing the head function symbol, as follows:

in a local goal with conclusion f u = f v, the conclusion is replaced with u=v. This produces as many sub-goals as there are arguments of the head function symbol. For a local goal, the tactic takes no arguments.
in a global goal, f(u1,...,un) is replaced with u1,...,un.

In the global goal setting, the target can be selected with its position, or using a fa_arg, which behave as follow:

fa term_pat selects the first position in the equivalence that matches term_pat.
fa !t repeats the function application as many times as possible, but at least once.
fa ?t repeats the function application as many times as possible, including 0.
fa arg1, arg2, ... is syntactic sugar for fa arg1; fa arg2; ....

Local tactics¶

TraceTactic congruence¶: Attempt to conclude by automated reasoning on message (dis)-equalities. Equalities and disequalities are collected from hypotheses, both local and global, after the destruction of conjunctions (but no case analysis is performed to handle conjunctive hypotheses). If the conclusion is a message (dis)-equality then it is taken into account as well.

TraceTactic const variable¶

Add the const tag to a variable.

The variable must be of a finite and fixed (η-independent) type, and must not appear in any global hypothesis (some global hypotheses may be localised (see localize) if necessary.

TraceTactic eqnames¶: Add index constraints resulting from names equalities, modulo the known equalities.

If n(i) = n(j) then i = j. This is checked on all name equality entailed by the current context.

TraceTactic executable term¶: Assert that exec@_ implies exec@_ for all previous timestamps.

Given as input a timestamp ts, this tactic produces two new sub-goals, requiring to prove that happens(ts) holds and that exec@ts also holds. The fact that (forall (t:timestamp), t <= ts => exec@t) is added as a hypothesis to the current goal.

TraceTactic project¶: Turn a local goal on a multi-system into one goal for each single system in the multi-system.

TraceTactic rewrite equiv -?proof_term¶

Use an equivalence to rewrite a reachability goal.

First, try to resolve proof_term as an equivalence equiv (diff(u,v)). Then, try to find a context C that does not contain any names, diff-terms or macro terms such that the current local goal phi is convertible with C[u]. If such a context is found, the current goal is is changed to C[v].

If a - sign is added in front of proof_term, the rewriting occurs in the other direction, replacing v with u.

Example: Hash rewrite

Consider the following goal.

[goal> Focused goal (1/1):
System: default/left (equivalences: left:default/left, right:default/right)
H: equiv(diff(h (a, k), n), diff(h (b, k), m))
U: [a <> b]
—————————————-
h (a, k) <> h (b, k)

Assuming we have been able to prove that two hashes are indistinguishable from names, we have hypothesis H. We then use H to replace the hashes with names in the conclusion of the goal, where we want to prove that the two hashes are not equal.

Calling rewrite equiv H produces the new goal:

[goal> Focused goal (1/1):
System: default/right (equivalences: left:default/left, right:default/right)
H: equiv(diff(h (a, k), n), diff(h (b, k), m))
U: [a <> b]
—————————————-
n <> m

TraceTactic smt ~prover? ~style? ~timeout:natural?¶: Try to discharge the current goal using an SMT solver.

The prover called can be chosen using the flag ~prover, supported provers include CVC5 (CVC5), Z3 (Z3) and Alt-Ergo (AltErgo). The alternative counterexamples can be used by adding (_counterexamples) after the name of the prover. The same goes with alternatives (_BV) for Alt-Ergo and (_noBV) for Z3.

The time before the timeout can be set with the flag ~timeout (in seconds). By default it is 1s.

The theory used to translate timestamps is chosen using the flag ~style. We can chose to translate timestamps to integers (nat) or to an abstract type with the usual equality (abstract) or not (abstract_noeq).

TraceTactic subst term, term¶

If x = t where x is a variable, then subst x, t substitutes all occurrences of x with t and removes x from the logical variables.

Error Unequal arguments¶

Terms given as argument are not equal.

Global tactics¶

EquivTactic cs pattern in position?¶

Performs case study on conditionals inside an equivalence.

Without a specific target, cs phi will project all conditionals on phi in the equivalence. With a specific target, cs phi in i will only project conditionals in the i-th item of the equivalence.

Example

When proving an equivalence

equiv(if phi then t1 else t2, if phi then u1 else u2)

invoking cs phi results in two sub-goals:

equiv(phi, t1, u1)
equiv(phi, t2, u2)

Error Argument of cs should match a boolean.¶

Error Did not find any conditional to analyze.¶

EquivTactic deduce position?¶

deduce i removes the i’th element from the bi-frame when it can be computed from the rest of the bi-frame. Without any argument, it will remove the first element that can be dropped, if it exists.

Here, the fact that the bi-frame element u can be computed from the other bi-frame elements x,y,... means that there exists a context C made of function applications such that u is equal to C[x,y,..].

This relies on some heuristical automated reasoning. Some properties on macros are automatically exploited, e.g. that for any timestamp t, frame@pred(t) allows to deduce input@t, all frame@t' for t' < pred(t), as well as the output@t' for whenever exec@t' is true.

EquivTactic diffeq¶: Close a reflexive goal up to equality. That is, if all diff-term whitin the global goal’s conclusion always evaluate to the same value in all systems, the equivalence holds. For each diff-term, a dedicated sub-goal is created.

Warning

This tactic is still at an experimental development stage. We do not recommend its usage.

Cryptographic tactics¶

Cryptographic tactics enable reasoning over cryptographic and probabilistic properties of random samplings and primitives.

Occurrence formula¶

Several reasoning techniques require tracking how a given name is used. For instance, if the name n does not occur at all in term t, then n=t is false with overwhelming probability. To apply a cryptographic assumption relying on a secret key, one needs to check that all occurrences of the secret key are valid (i.e. correspond to the key argument of the corresponding primitive).

Over macro-free terms, collecting occurrences is simply equivalent to looking at the subterms. However, if some macros occur in t, typically input@ts or output@ts, we need to look through all the actions that may have happened before ts to look for occurrences.

We define here how to build an occurrence formula that will be reused in several tactics description. For any name n, any term t and a set of allowed patterns pats (patterns built over the name n and function applications), we define the formula occurs(n,t,pats) as the conjunction of conditions under which it is possible that n occurs in t without following one of the allowed pattern of pats:

whenever t contains as a subterm an occurrence n that does not match any of the allowed patterns pats, the formula is true.
whenever t contains a system-defined macro, macro@ts, if ts is a concrete action, we simply unfold the definition of the macro, and whenever is it not concrete, we collect all actions of the form A1 such that n occurs in the definition of the action not as an allowed pattern, and the formula A1<=ts is added to the conjunction of occurs(n,t,pats).

occurs is of course generally defined for indexed names that may occur in indexed actions.

Example: Basic name occurrence

Consider the following process:

name n : index->message

channel c

system (!_i !_j A : out(c,n(i)) | B :in(c,x);out(c,x)).

The formula occurs(n(i),input@B,none) is equal to exists j. A(i,j) < B.

Example: Key corruption

Consider the following process:

name k : message
name r : message

senc enc,dec.

channel c.

system (Corr: out(c,k) | B : in(c,x);out(c,enc(x,r,k))).

To reason about the encrypted message, the key k needs to be secret, and thus the dynamic corruption should not have happened. This intuition is captured by the formula occurs(k,input@B,enc(_,r,k)), which is equal to Corr < B.

This formula may be imprecise, for example due to states.

Example: Imprecise state occurrence

name n : message

mutable s = n.

channel c

system (A: out(c,s) | B :in(c,x);out(c,x)).

Here, n occurs only inside the init action, where the mutable state is initialized with value n. The formula occurs(n,input@B,none) is then equal to init < B. However, the occurrence can happen only if A did occur between init and B to reveal the value of the state.

We define a precise variant precise_occurs(n,t,pats), that tracks more precisely the usages of the states, and also adds the condition that the correct value of the state is revealed if a state can contain an occurrence of n.

We also generalize occur to allow for collecting multiple name occurrences at once, which is useful when we want to allow patterns depending on two names at once (see e.g. gdh or ddh).

Common tactics¶

Tactic fresh ~precise_ts? positionhypothesis_id¶

Fresh is an information-theoretically sound tactic exploiting the fact that names represent independent random samplings. This can be exploited in two ways: i) to remove a fresh name from an equivalence; or ii) to obtain that a term has a negligible probability of being equal to a fresh name.

In a local goal with conclusion phi, the tactic may be called on a hypothesis of the form t=n for some name n sampled over a type with tag large. For such a sampling, if term t is computed without knowing n, this equality can only hold with negligible probability. We may thus assume that n occurs in t. Accordingly, the tactic turns the conclusion into the formula occur(n,t,none) => phi (see the definition of the occurrence formula).

If one can then prove that n cannot occur in t, that is that occur(n,t,none) is false, that new conclusion trivially holds. If occur(n,t,none) is trivially false, e.g. if t is a macro-free term without n as a subterm, the goal will be directly closed.

Example: Name leak

Consider a small process in(c,x); A : out(c,x);in(c,x); B: out(c,n), where we wish to prove that input@A <> n. Intuitively, this holds as n is only revealed after A has occurred.

The goal corresponding to this proof will look like this:

[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Eq: input@A = n
H: happens(A)
—————————————-
false

Calling fresh Eq turns the goal into:

[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Eq: input@A = n
H: happens(A)
—————————————-
B < A => false

Here, Squirrel automatically deduced that n can only occur inside input@A if the output of B happened before A. One would conclude by using the fact, according to the process definition, this is impossible.

In an equivalence goal, on the other hand, the tactic must be applied to a bi-frame element i of the form diff(nL,nR), where nL, nR are names sampled over the same type. Since samplings are independent, the two names are indistinguishable, unless some information on them is revealed by the rest of the bi-frame. Note that, contrary to the local case, that property holds even if the type is not large.

If we let bf denote the bi-frame, the :g:ì`th bi-frame element is replaced by the tactic with

if not(diff(occur(nL,bf,i : diff(nL,nR)),occur(nR,bf,i : diff(nL,nR)))) then
zero
else
diff(nL,nR)

We specify through the occurrence formula that the only possible occurrence of nL is in fact the one we are currently looking at.

In all cases, the precise_ts makes the tactic use precise_occur instead of occur.

Latest formal Squirrel description: [BKL23] (Appendix F).

Local tactics¶

TraceTactic cdh hypothesis_id, term¶

This tactic applies the Computational Diffie-Hellman assumption (see e.g. [OP01]), stating for a generator $g$ and randomly sampled exponents $a$ and $b$, it is computationally hard to compute $g^{ab}$ when only $g^a$ and $g^b$ are known.

A cdh, ddh or gdh group declaration must have been specified (the DDH or GDH assumptions indeed both imply the CDH assumption). For a group with generator g and exponentiation ^, the tactic cdh M, g may be called in a local goal on a message equality hypothesis M of the form t=g^{a b}. Following the CDH assumption, M can only hold if t accesses a or b in some way other than g^a and g^b.

Therefore, the tactic will replace in the current goal the conclusion phi with occur(a,t,g^a) || occur(b,t,g^b) => phi (see the definition of the occurrence formula). If both occurrence formulas are trivially false, then the goal is closed automatically.

A formal description of this tactic has not yet been given in any published work.

TraceTactic gdh hypothesis_id, term¶

This tactic applies the Gap Diffie-Hellman assumption (see e.g. [OP01]), which is similar to CDH over $g^a$ and $g^b$, except that the attacker is additionally allowed to access an oracle testing equality to $g^{ab}$. It also includes the Square-GDH variant (see [FS11]), which is equivalent to the GDH assumption for prime order groups, where the attacker can also test equality to $g^{aa}$ and $g^{bb}$.

A gdh group declaration must have been specified.

The behaviour of this tactic is similar to cdh, expect that the current goal’s conclusion phi is replaced with a more permissive formula occur((a,b),t,(g^a,g^b,_=g^(ab), _=g^(bb), _=g^(aa)) => phi (see the definition of the occurrence formula).

A formal description of this tactic has not yet been given in any published work.

TraceTactic collision¶

Requires a hash function declaration.

This tactic applies the known-key collision resistance assumption (see e.g. the cr2-kk assumption from [GB96]).

It collects all equalities between hashes occurring at top-level in message hypotheses, that is all hypotheses of the form h(u,k)=h(v,k), and for each such hypothesis adds as new hypothesis u=v.

As this implements the known-key variant of the collision resistance assumption, no side condition is checked on the hash key.

Latest formal Squirrel description: [BKL23] (only as an example).

TraceTactic euf hypothesis_id¶

Requires either a hash function or a signature scheme declaration.

This tactic applies the EUF-CMA axiom in a local goal, either for keyed-hashes or signatures. (see e.g. [GB96])

For a hash function h(x,k), one may call euf M over a message equality M of the form t = h(m,k) or h(m,k)=t. EUF-CMA then states that, provided the key k is always used in correct position, M can only hold if computing t requires already knowing the hash of m. Accordingly, the tactic creates a first new sub-goal asking to prove that the key is only used in correct position, i.e. a sub-goal with conclusion not(occur(k,goal,h(_,k)) (see the definition of the occurrence formula). The tactic then collects all possible occurrence of a honest hash h(u,k) inside t, and for each of them, creates a sub-goal with the original conclusion and a new hypothesis stating that m=u. Moreover, if the occurrence is under a macro, additional new hypotheses will state that these macros must be taken at an earlier timestamp than t.

Example: Basic hashing

Consider the following system:

hash h
name k:message
channel c
name n : message
name m : message

system (!_i out(c,h(n,k)) | in(c,x);out(c,x)).

Calling euf over a hypothesis of the form input@tau <> h(m,k) would add the fact that h(m,k) needs to be equal to one of the honestly computed hashes appearing in input@tau, which are all of the form h(n,k). The new hypothesis would then be:

(exists (i:index), A(i) < tau && m = n)

For a signature function sign(x,r,k), public key pk(k) and verification function check(s,m,pub), euf must be called on a hypothesis of the form check(s,m,pk(k)). The behaviour is then similar to the hash case: honest signatures that may occur in s will be collected, and m must be equal to one of the honestly signed messages. A sub-goal for each possible honest signing case is created, as well as a sub-goal specifying that the key is correctly used, i.e. with conclusion not(occur(k,goal,sign(_,k), pk(k)).

Latest formal Squirrel description: [BKL23].

TraceTactic intctxt hypothesis_id¶

This tactic applies the INT-CTXT assumption (see e.g. [BN00]) in a local goal.

It requires the declaration of a symmetric encryption scheme.

It can be applied to a hypothesis either of the form dec(c,k)<>fail or dec(c,k) = t (in the latter case, it will generate as an additional proof obligation that t <> fail).

The INT-CTXT assumption then states that, provided the key k is correctly used, such a decryption may only succeed if c was produced by an honest encryption.

In both cases, Squirrel will thus collect all honest encryptions made with key k, and produce a subogal corresponding to each case where c is equal to one of those honest encryptions.

The key k must only be used in key position, so a sub-goal asking to prove that not(occur(k,c,(enc(_,_,k),dec(_,k))) is created when it is not trivially true (see the definition of the occurrence formula).

In addition, a goal asking to prove that all randomness used for encryption are disjoint and fresh (when it is not trivially true).

Latest formal Squirrel description: [BDJ+21].

Global tactics¶

EquivTactic cca1 position¶

This tactic applies the IND-CCA assumption (see e.g. [BN00]) in a global goal.

It requires the declaration of a symmetric encryption or asymmetric encryption scheme.

The tactic may be called over a bi-frame element containing a term of the form C[enc(n, r, m)], where

r must be a fresh name;
there is no decryption in C;
no universal message variable occurs;
m is a key or a public key that only appears in key position, i.e. under pk, dec or enc.

The tactic will then replace the encryption occurrence by an encryption of a bitstring of zeroes of the correct length, yielding C[enc(zeroes(len(n)), r, pk(k))].

In addition, the tactic creates a sub-goal asking to prove that all occurrences of the key and encryptions are correct. Notably, one must prove that occur(k,bi-frame,(enc(_,_,k), dec(_,k)) (see the definition of the occurrence formula) is false (or occur(k,bi-frame,(pk(k), dec(_,k))) for the asymmetric case).

In addition, in the asymmetric case, a sub-goal is created to prove the freshness of the random used in the encryption, with the conclusion occur(r,bi-frame,enc(n,r,m)).

In the symmetric case, an additional sub-goal is created ensuring that all encryptions are made with distinct fresh randoms (and not just the the encryption we are looking at).

Latest formal Squirrel description:[BKL23].

EquivTactic ddh term, term, term, term¶

This tactic applies the Decisional Diffie-Helman assumption (see e.g. [OP01]), stating that for a generator $g$, and randomly sampled exponents $a$, $b$, $c$, it is computationally hard to distinguish $g^{ab}$ from $g^c$, when only $g^a$ and $g^b$ are known.

A ddh group declaration must have been specified.

When calling, ddh g,a,b,k, the goal must contain only diff terms of the form diff(g^(ab),g^(c))). The tactic will close the goal if the formula occur((a,b,c),goal,(g^a,g^b,diff(g^(ab),c))) instantly reduces to false (see the definition of the occurrence formula).

Latest formal Squirrel description: [BDJ+21].

EquivTactic enckp position term_pat? term?¶

ENC-KP assumes that a symmetric or an asymmetric encryption scheme does not leak any information about the public (or secret) key used to encrypt the plaintext. It is based on the IK-CPA notion of [BBDP01].

The tactic can be called on a bi-frame element containing a term of the form C[enc(n, r, m)], where

r must be a fresh name;
there is no decryption in C;
no universal message variable occurs;
m is either a key or the diff of two keys, that only appear in key position, i.e. under pk, dec or enc;
if m is a key, and a second key has been given as argument to the tactic, that key must also occur only in key position.

When m is the diff of two keys, the diff is simplified by keeping only the key on the left. When m is just one key, a new key with which it is replaced can be specified as arugment.

Example: Basic ENC-KP application

On a bi-frame element of the form

i : enc(n,r,diff(pk(k1),pk(k2)))

calling the tactic enckp i will simplify the bi-frame element by only keeping the key on the left, yielding

i: enc(n,r,pk(k1))

The tactic expects as arguments:

the position identifying the bi-frame element;
optional: the encryption term on which to apply the tactic;
optional: the new key with which to replace the key.

Example: Switching key with ENC-KP

On a bi-frame element of the form

i: enc(n,r,m)

the tactic enckp i, k will simplify the bi-frame element by using the specified key, yielding

i: enc(n,r,pk(k))

Example: Targeted ENC-KP application

On a bi-frame element of the form

i: ⟨ enc(n,r,m),m’⟩

the tactic enckp i,enc(n,r,m), k will simplify the bi-frame element by using the specified key, yielding

i: ⟨ enc(n,r,pk(k)),m ‘⟩

To apply the enckp tactic, the key k must be such that occur(k,bi-frame,(enc(_,_,k), dec(_,k)) (see the definition of the occurrence formula) is trivially false. (or occur(k,bi-frame,(pk(k), dec(_,k))) for the asymmetric case).

When it is not trivially true, a sub-goal is created, asking to prove the freshness of the random used in the encryption, with the conclusion occur(r,bi-frame,enc(n,r,m)).

In the symmetric case, an additional check is performed ensuring that all encryptions are made with distinct fresh randoms (and not just the encryption we are looking at).

Latest formal Squirrel description:[BDJ+21].

EquivTactic prf position , term_pat?¶

This tactic applies the PRF assumption (see e.g. [GB96]).

It requires a hash function declaration.

This tactic applied to a bi-frame element containg a hash application h(m,k) tries to replace the hash value with a fresh name, under the condition that m has never been hashed before, and that the key k is correctly used.

Formally, when called over a bi-frame element i : C[h(m,k)], the tactic replaces in the current goal the element with i : C[nPRF] where nPRF is a newly generated unique name. It in addition produces sub-goals requiring to prove the side conditions described above. It notably produces a goal asking to prove that the key is only used in key position, i.e. that occur(k,bi-frame,h(_,k)) is false (see the definition of the occurrence formula). In addition, it creates for each occurrence of h(t,k) within the bi-frame (that may occur under macros) a sub-goal asking to prove that t <> m, that is, that m was never hashed before. Such sub-goals may need to be created separately for both projections of the bi-frame.

Example: Basic PRF application

Consider the following system:

channel c
hash h
name k : message
name n :message
name m :message
name p :message
system (A: out(c,h(n,k)) | B: out(c,h(m,k))).

When trying to prove that [happens(A)] -> equiv(frame@pred(A),diff(output@A,p)), one may call the tactic prf on the bi-frame element corresponding to the diff(output@A,p), which after expanding output is diff(h(n,k),p).

This replaces in the current goal the hash occurrence with diff(n_PRf,p), and creates a sub-goal asking to prove that the hash message n is different from any possible previously hashed message. Here, the only other possible hash would occur in frame@pred(A), in the output of B if it occurred before A. The created sub-goal then asks to prove that [B < A => n <> m].

If multiple occurrences of hashes occur in the bi-frame element, the first one is targeted by default. Calling the tactic with an optional term_pat allows to target a specific hash occurrence.

Latest formal Squirrel description: [BKL23].

EquivTactic xor position , term_pat? , term_pat?¶

This tactic applies the unconditionally sound one time pad property of the xor operation.

The tactic applied to a bi-frame element of the form i : C[n XOR t] will replace the XOR term by

if occur(n,bi-frame, i : C[n XOR t] ) && len(n) = len(t) then n_FRESH else (n XOR t)

This new term then allows us to drop the old term only if n and t do have the same length (as the one time pad does not work otherwise), and if this is the only occurrence of n in the bi-frame.

When multiple XOR occur in the bi-frame, one can specify one or two optional term patterns, to specify in any order the name n or the full XOR-ed term n XOR t to target.

Latest formal Squirrel description: [BDJ+21].

Utility tactics¶

Tactic help tacnconcise?¶: When used without arguments, display all available commands. The tactic can also display the details for a given tactic name, or display or more concise list. It is a tactic and not a command, and as such can only be used inside proofs.

Tactic lemmas¶: Print all axioms and proved lemmas. This is useful to know which lemmas can be used through the use or apply tactics.

Tactic show term_pat¶: Print the messages given as argument. Can be used to print the values matching a pattern.