Using HOL90, we have defined a number of new data types to describe IP datagrams, IPSEC security mechanisms, and mobile registration messages. Performing proofs however, remains a human-intensive process. To better support the use of our mechanized logic, we have developed a general infrastructure base, based on earlier work[12], for creating automated and interactive procedures to prove goals about inductively defined relations.

The infrastructure provides tools to build interactive functions and
goal-directed support functions, procedures to eliminate existentially
quantified variables from terms, and tactics to generalize existentially
quantified rules. Many of the functions are generic, expecting as arguments
the list of inference rules returned by `new_inductive_definition` and a
list of the relevant combinators. In our case, the list of relevant
combinators includes all of the type constructors from the newly defined types
(`key, keyuse, keyfact, item,` and `proposition`).

For many applications, validation of the inductively defined rules is, at least initially, of greater importance than automated proofs. For the automated proofs to be useful, their construction must be understood. Thus, it is valuable for the automated procedures to inform the user what rules are relevant and when rules are applied to a goal.

Interactive support is provided by a collection of parameterized functions
that suggest an appropriate rule to apply based on the current goal or a term.
(`suggested_rules()` and `rules_for_term()`, respectively). Using
these mechanisms, users don't need to remember all the rules that may apply,
but can request a list of potentially useful rules.
Many protocol logics have a significant number of inference rules
([4] lists 44 rules).
Even SVO logic, which was designed to significantly reduce the number of
rules compared with other protocol logics, requires 23 rules.

We have also developed a tactic generating function, `make_suggest_tac`
that returns a tactic specialized for a list of inference rules and a list of
combinators. The tactic searches for and then applies, an appropriate rule to
apply based on the current goal. In practice, this tactic appears to provide
a significant improvement over tactics that try every rule. The tactic also
outputs what rules where chosen to apply in a given situation. The displayed
list of decisions can assist the user understand why a proof is correct and
often, why it fails.

A second general tactic `EXISTS_ELIM_TAC` has also been developed to
search for witnesses to replace existentially quantified variables. The
tactic searches the assumption list for candidates that match the variable's
usage in the goal.
After replacement, goals can often be reduced by rewriting with the assumption
list. For performance considerations, the tactic defers rewriting until all
existentially quantified variables have been replaced.

Using the above two tactics, a general strategy was developed and programmed
into a tactic (`IND_RULES_TAC`). The initial proofs of the lemmas
required a fair number of steps, but with the use of the `
IND_RULES_TAC`, the proofs are performed with only a few tactics. The
resulting proofs also require less time with fewer intermediate theorems
generated. At this point in development, the tactic does not backtrack and so
occasionally, the user must select the correct rule.

The final general support mechanism developed supports generalizing some of
the rules returned by `new_inductive_definition`. When creating a new
inductive definition, there are often rules with existentially quantified
variables in the antecedent that could instead be universally quantified.
While this is not always beneficial, in many cases, proofs are simplified.