Simplified a proof

New comment in header

Tidied up some proofs

Ran expandshort

Removed commands made redundant by new one-point rules

Ran expandshort

New one-point rules for quantifiers

Greatly simplified the proof of A_can_trust

Working again with new theory Shared

Simplified main theorem by abstracting out newK

Moved sees_lost_agent_subset_sees_Spy to common file, and simplified main thm

Moved sees_lost_agent_subset_sees_Spy to common file

Added new guarantees for A and B

added shyps comment;

Inserted check for rewrite rules which introduce extra Vars on the rhs.

Removed some dead wood. Transferred lemmas used to prove analz_image_newK to Shared.ML

Improved discussion of shyps thanks to Markus Wenzel

prune_params_tac no longer rewrites main goal

Added catch-all clause to drop, preventing exception Match

Now replaces uses of ssubst by stac

Documented sort hypotheses and improved discussion of derivations

Documented defer_tac and moved back the obsolete tactics like fold_tac

Documented stac, and updated the documentation of hyp_subst_tac

Declared stac

Ran expandshort; used stac instead of ssubst

Ran expandshort; used stac instead of ssubst

Ran expandshort; used stac instead of ssubst

Ran expandshort; used stac instead of ssubst

Introduction of "lost" argument Changed Enemy -> Spy Ran expandshort

Ran expandshort

Changed freeze to freeze_thaw

Generalized freeze to freeze_thaw in order to implement defer_tac

Last working version prior to addition of "lost" component

Last working version before "lost"

Last working version prior to introduction of "lost"

Prevention of Overflow exception (for SML/NJ) in gensym

Rationalized the rewriting of membership for {} and insert by deleting the redundant theorems in_empty and in_insert

Calls discgarb -c to realize dramatic space savings!

Fixed spelling error in comment

Added miniscoping for UN and INT

Restoration of reference to Nipkow, LICS, 1993

Moved Option out of IOA into core HOL

Moved Option into core HOL which caused a few local changes.

Proofs made more robust to work in presence of le_refl

Now uses init_html

Simplification of proof of unique_session_keys

Correction of protocol; addition of Reveal message; proofs of correctness in its presence

Proof of Says_imp_old_keys is now more robust

Removal of the Notes constructor

New laws for messages

Simplification of definition of synth

Addition of le_refl to default simpset/claset

Removal of reference Nipkow-LICS-93

Proof of mult_le_mono is now more robust

New infix syntax: breaks line BEFORE operator

Optimized version of SELECT_GOAL, up to 10% faster

New operations on cterms. Now same names as in Logic

Addition of gensym

Bad version of Otway-Rees and the new attack on it

Reformatting; proved B_gets_secure_key

Abstraction of enemy_analz_tac over its argument

Reformatting

Reordering of premises for cut theorems, and new law MPair_synth_analz

No longer assumes Alice is not the Enemy in NS3. Proofs do not need it, and the assumption complicated the liveness argument

Uses the improved enemy_analz_tac of Shared.ML, with simpler proofs Weak liveness

Addition of Yahalom protocol

Removal of obsolete thm Fake_parts_insert

Addition of enemy_analz_tac and safe_solver Use of AddIffs for theorems about keys

added flat_eq, renamed adm_disj_lemma11 to adm_lemma11, localized adm_disj_lemma1, ..., adm_disj_lemma10, adm_disj_lemma12, modularized proof of admI

renamed adm_disj_lemma11 to adm_lemma11

added comment on is_flat

added stric tI

undo last revision

bin/isa2latex: copy the binary to bin/isa2latex instead of linking it there

new \subsubsection{Configuring conversion tables and keyboard bindings} (by Franz Regensburger) added to the manual.

Tidied many proofs, using AddIffs to let equivalences take the place of separate Intr and Elim rules. Also deleted most named clasets.

Installed AddIffs, and some code from HOL.ML

Simplification and tidying of definitions

Now hologic.ML is loaded in HOL.ML

New file cladata.ML

Split off classical reasoning code to cladata.ML

Change to best_tac required to prevent looping

Moved RSLIST here from ../Relation.ML

Removal of univ_cs

Reformatting

renamed cterm_lift_inst_rule to term_lift_inst_rule and made it take uncertified things, because they need to be recertified anyway.

Removed refs to clasets like rel_cs etc. Used implicit claset.

Converted proofs to use default clasets.

Added Auth to the test target

Now runs all Auth proofs

Now uses DB-ROOT.ML, which is separate from ROOT.ML

Dedicated root file for making the Auth database

Beefed-up auto-tactic: now repeatedly simplifies if needed

"bad" set simplifies statements of many theorems

added cterm_lift_inst_rule

Stronger proofs; work for Otway-Rees

Stronger proofs; work for Otway-Rees

These simpsets must not use miniscoping

Corrected associativity: must be to right, as the type dictatess

Removal of (EX x. P) <-> P and (ALL x. P) <-> P from ex_simps and all_simps. as they are already in quant_simps.

Improved error handling: if there are syntax or type-checking errors, prints the name of the offending axiom

Modified proof to work with miniscoping

Now uses thin_tac

Now uses thin_tac

Renaming of _rews to _simps

Added thin_tac to signature; previous change was useless

Some renaming. Note that this miniscoping is more general than that of ../simpdata.ML, as distributive laws are included. On this other hand this version is for NNF only.

Introduction of miniscoping for FOL

Pretty-printing change to emphasize the scope of assumptions

Declared thin_tac

Miniscoping rules are deleted, as these brittle proofs would otherwise have to be entirely redone

Simplified some proofs for compatibility with miniscoping

Added miniscoping to the simplifier: quantifiers are now pushed in

Fixed pretty-printing of {|...|}

New theorems for Fake case

A further tidying

ROOT file for Auth directory

Renaming and simplification

Renaming and simplification

Initial working proof of Otway-Rees protocol