Cosmetic changes: margins, indentation, ...

Now possibility_tac and basic_possibility_tac are explicit functions, in order to delay the evaluation of \!simpset

Deleted the superfluous assumption A ~= B, which must hold anyway by induction

Fixed the spelling of AUTH_NAMES--it could not have worked before\!

Option is a synonym for General because MLWorks does not yet provide Option as a separate structure

Removal of the tactical STATE

Removal of the tactical STATE

tuned error propagation msg;

defs may now be conditional; improved output of warnings / errors;

renamed |-> <-| <-> to Parse/PrintRule;

tuned warning;

tuned warnings; print_current_goals_fn, result_error_fn hooks replace print_goals_ref;

considered removal of print_goals_ref;

defs: allow conditions;

tuned warning; improved comments;

renamed |-> <-| <-> to Parse/PrintRule;

tuned warning;

tuned warning; renamed |-> <-| <-> to Parse/PrintRule;

improved output channels: normal, warning, error;

fixed EqI meta rule;

changes needed for introducing fairness

changes neede for introducing fairness

changes needed for adding fairness

fixed merge of internal simprocs;

Changing "lost" from a parameter of protocol definitions to a constant. Advantages: no "lost" argument everywhere; fewer Vars in subgoals; less need for specially instantiated rules Disadvantage: can no longer prove "Agent_not_see_encrypted_key", but this theorem was never used, and its original proof was also broken the introduction of the "Notes" constructor.

Fixed delIffs to deal correctly with the D-rule

Removed redundant addsimps of Un_insert_left, which is now a default simprule

Removal of monotonicity reasoning involving "lost" and the theorem Agent_not_see_encrypted_key, which (a) is never used and (b) becomes harder to prove when Notes is available.

Now uses the Notes constructor to distinguish the Client (who has chosen M) from the Spy (who may have replayed her messages)

Moved some declarations to Message from Public and Shared

Now loads theory Event, which contains common declarations

Moving common declarations and proofs from theories "Shared" and "Public" to "Event". NB the original "Event" theory was later renamed "Shared". Addition of the Notes constructor to datatype "event".

removed obsolete init_pps and init_thy_reader;

improved type checking errors;

removed init_pps;

removed init_database;

Improved length = size translation.

New proofs involving CERTIFICATE VERIFY

eliminated chmod -w;

-w option;

NOWRITE;

added -w option;

Changed some variables of type msg to lower case (e.g. from NB to nb

New constant "certificate"--just an abbreviation

Reduced priority of postfix ^* etc operators such that they are the same as application. Eg wf r^* now needs to be written wf(r^*).

Automatic update

Now catches the error of calling tgoalw when there are no goals to prove, instead of just letting USyntax.list_mk_conj raise an exception

Simplified the new proofs about division

New comments on how to deal with unproved termination conditions

Fixed comments

Moved MLWorks.ML to its proper place, directory ML-Systems. Note that MLWorks does not quite work yet, especially top-level pretty printing

Automatic update

Modified the \tydx command to set types in italics instead of \tt

Some LaTeX-2e primitives such as \texttt A bit of material on theories Primes and Primrec

Added documentation for recdef, and tidied some other material

Updated references

set_of_list -> set

Now there are TWO spaces after each full stop, so that the Emacs sentence primitives work

Now there are TWO spaces after each full stop, so that the Emacs sentence primitives work

Added the following lemmas tp Divides and a few others to Arith and NatDef: div_le_mono, div_le_mono2, div_le_dividend, div_less_dividend Fixed a broken proof in WF_Rel.ML. No idea what caused this.

Tidying; also simplified the lemma Says_Server_not

New theory TLS

Deleted a redundant A~=B in rules that refer to a previous event

More realistic model: the Spy can compute clientK and serverK

Reordered rules in analz_image_freshK_ss to improve clarity

Removal of the obsolete newN function

New theorem priK_inj_eq, injectivity of priK

spy_analz_tac: Restored iffI to the list of rules used to break down the subgoal

New theory TLS

Baby TLS. Proofs work, but model seems unrealistic

New and stronger lemmas; more default simp/cla rules

Deleted the obsolete operators newK, newN and nPair

Now the possibility proof calls the appropriate tactic

Added a comment

Now Collect_mem_eq is a default simprule (how could it have ever been omitted?

New laws for the "lists" operator

More concat lemmas.

Corrected indentations and margins after the renaming of "set_of_list"

set_of_list -> set

Trivial changes in connection with the Yahalom paper. Changed the order of the premises in no_nonce_YM1_YM2. Installed B_trusts_YM4_newK using bind_thm. Improved some comments.

oops;

rearrange pages of ps file to be printed as booklet (duplex);

amdI -> admI2

Tuned Franz's proofs.

Removal of structure Context and its replacement by a theorem list of congruence rules for use in CONTEXT_REWRITE_RULE (where definitions are processed)

Removal of COND_CONG, which is just if_cong RS eq_reflection

Ran expandshort

New "congs" keyword for recdef theory section

removed old Makefile;

removed;

removed old Makefile;

removed old Makefile and compat files;

Made proofs more concise by replacing calls to spy_analz_tac by uses of analz_insert_eq in rewriting

Proof tidying and variable renaming (NA->na, NB->nb when of type msg)

New comments; a tidied proof

Two new rewrite rules--NOT included by default\!

Defines KeyWithNonce, which is used to prove the secrecy of NB

Addition of not_imp (which pushes negation into implication) as a default simprule

Corrected Title in header lines

Streamlined proofs of the secrecy of NB and added authentication of A and B

Removed Says_Crypt_lost and Says_Crypt_not_lost. Installed not_lost_tac. Deleted unused theorems initState_subset and seesD

Removed Says_Crypt_lost and Says_Crypt_not_lost. Installed not_lost_tac

Adapted proofs to the removal of Says_Crypt_lost and Says_Crypt_not_lost

Deleted spurious reference to Spy_not_see_NB, which by chance was defined in Yahalom.ML\!

converse -> ^-1

Type constraint added to ensure that "length" refers to lists. Maybe should not be needed, but the translation length->size happens irrespective of types

Replacing the primrec definition of "length" by a translation to the built-in "size" function

Tuned wf_iff_no_infinite_down_chain proof, based on Konrads ideas. Added selectI2EX.

changed compatible definition;

added deadlock

added deadlock freedom, polished definitions and proofs

Strengthened and streamlined the Yahalom proofs