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.

# Logical

## auto

Automatically prove a goal. Performs basic logical reasoning and reasoning on indices, timestamps and message equalities. Does not incorporate any cryptographic reasoning.

## admit

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 `N`

-th element.

## apply

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.

Examples: `apply H`

, `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

Case analysis on an hypothesis (`case H`

) a formula (`case (i = j)`

) or a timestamp (`case tau`

).

## exists

Introduce the existentially quantified variables in the conclusion of the judgment, using the arguments as existential witnesses.

## have

Syntax: `have H : formula`

.

Prove an intermediate goal, which will then be available as an hypothesis to prove the initial goal.

## induction

Apply the induction scheme to the conclusion.

## intro

Introduce topmost universal quantifications and implications. Names should be provided for universally quantified variables, and identifiers for hypotheses of implications.

## left/right

When the conclusion is a disjunction, prove its left or right subformula.

## rewrite

If `H : t1 = t2`

, the tactic `rewrite H`

will rewrite all occurrences of `t1`

into `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 `rewrite -H`

.

## split

Split a conjunction conclusion, creating one subgoal per conjunct. Also works when the conclusion is an equivalence, seen as a conjunction of two implications.

# Structural

## depends

When action `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.

## fa

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

`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 `frame@tau`

assuming `exec@tau`

, in the same way on the left and right projections (hence `formula`

must not contain diff operators).

## fresh

Attempt to remove a name from an equivalence by showing that it is fresh.

Usage: `fresh N`

where `N`

is the position of the target name.

## project

Turn a goal on a multi-system into one goal for each projection of the mutli-system.

# Cryptographic

## collision

Finds all pairs of hashes that are equal according to the current hypothesis, and adds as new hypotheses the equalities of the hashed messages.

## euf

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.

## prf

Apply the PRF axiom. Takes the position of the equivalence item as argument.