The tactics are split in three groups:
- logical tactics correspond to general logical reasoning (these tactics are similar to the ones you would find in Coq);
- structural ones are specific to Squirrel, dealing with equivalences, freshness of names, and systems;
- cryptographic tactics are the ones that reflect crypto assumptions.
Automatically prove a goal. Performs basic logical reasoning and reasoning on indices, timestamps and message equalities. Does not incorporate any cryptographic reasoning.
Admit the current goal: it does not count as a valid proof, of course, but is used to leave a subgoal aside to look at the next one, or to let a student treat it as an exercise ;)
If the conclusion is an equivalence,
admit N will remove its
The apply tactic allows to use an assumption to prove the conclusion of the current goal. The assumption can start with a series of universal quantifications and implications, ending with a formula that matches the current goal. It will generate new subgoals to justify the implications. It may require the user to provide terms for instantiating the universal quantifications.
apply H k,
apply le_trans _ t. The last form asks
apply to guess the first term but specifies the second one, and it uses a previously proved lemma rather than an hypothesis from the current goal.
When the conclusion is an equivalence,
apply use bi-deduction to justify the target equivalence using the one provided by the applied assumption.
Case analysis on an hypothesis (
case H) a formula (
case (i = j)) or a timestamp (
Introduce the existentially quantified variables in the conclusion of the judgment, using the arguments as existential witnesses.
have H : formula.
Prove an intermediate goal, which will then be available as an hypothesis to prove the initial goal.
Apply the induction scheme to the conclusion.
Introduce topmost universal quantifications and implications. Names should be provided for universally quantified variables, and identifiers for hypotheses of implications.
When the conclusion is a disjunction, prove its left or right subformula.
H : t1 = t2, the tactic
rewrite H will rewrite all occurrences of
t2 in the conclusion (which can be a local formula, an equivalence or an arbitrary global formula).
The tactic can also be used to rewrite a macro into its definition, by using e.g.
rewrite /output for the output macro.
It is possible to rewrite in an hypothesis using
rewrite H in H'. It is also possible to rewrite in the reverse direction using
Split a conjunction conclusion, creating one subgoal per conjunct. Also works when the conclusion is an equivalence, seen as a conjunction of two implications.
A(i) depends on
B(j) in the system under consideration,
depends B(j),A(i) introduces the hypothesis
B(j)<=A(i) in the goal. It must be done manually, since
auto does not take it into account.
Apply the function application axiom. Concretely,
fa N will remove the toplevel function symbol from an equivalence conclusion. It is also possible to invoke the tactic with a pattern to avoid using explicit numbers (which result in fragile proofs): for example,
fa <_,_> will use the function application rule on the first item that is a pair.
fadup N can remove the
N-th item in an equivalence conclusion if this item is of the form
exec@tau && formula and
frame@tau is available elsewhere in the equivalence, and
formula can be computed from
exec@tau, in the same way on the left and right projections (hence
formula must not contain diff operators).
Attempt to remove a name from an equivalence by showing that it is fresh.
fresh N where
N is the position of the target name.
Turn a goal on a multi-system into one goal for each projection of the mutli-system.
Finds all pairs of hashes that are equal according to the current hypothesis, and adds as new hypotheses the equalities of the hashed messages.
Apply the EUF axiom to the given hypothesis name. The hypothesis must be of the form
u = h(v,k) where
h is a hash function or
checksign(sign(v,pk),sk) = v for a signature scheme.
The equations can be provided in the reverse direction (the tactic will reverse the equation by itself before starting its work) but when both sides of the equality are hashes it might be necessary to orient it first (using
have to obtain a new hypothesis with the properly oriented equality) in order to obtain the desired behaviour.
Apply the PRF axiom. Takes the position of the equivalence item as argument.