The tactics are split in three groups:

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.