src/HOL/Auth/Message.ML
1997-09-19 paulson 1997-09-19 Deleted the obsolete theorem analz_UN1_synth
1997-09-18 paulson 1997-09-18 Global change: lost->bad and sees Spy->spies First change just gives a more sensible name. Second change eliminates the agent parameter of "sees" to simplify definitions and theorems
1997-09-11 paulson 1997-09-11 Split base cases from "msg" to "atomic" in order to reduce the number of freeness theorems
1997-08-21 paulson 1997-08-21 Replacing impOfSubs analz_mono by analz_insertI should improve convergence of spy_analz_tac
1997-08-01 nipkow 1997-08-01 Had to remove {x.x=a} = a from !simpset in one proof.
1997-07-14 paulson 1997-07-14 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.
1997-07-11 paulson 1997-07-11 Moved some declarations to Message from Public and Shared
1997-07-01 paulson 1997-07-01 spy_analz_tac: Restored iffI to the list of rules used to break down the subgoal
1997-07-01 paulson 1997-07-01 Added a comment
1997-06-19 paulson 1997-06-19 New comments; a tidied proof
1997-06-09 paulson 1997-06-09 Useful new lemma
1997-05-07 paulson 1997-05-07 Conversion to use blast_tac (with other improvements)
1997-05-05 paulson 1997-05-05 Some blast_tac calls; more needed
1997-04-15 paulson 1997-04-15 Moved expand_case_tac from Auth/Message.ML to simpdata.ML
1997-04-09 paulson 1997-04-09 Using Blast_tac
1997-04-04 paulson 1997-04-04 Calls Blast_tac
1997-02-15 oheimb 1997-02-15 reflecting my recent changes of the simplifier and classical reasoner
1997-01-27 paulson 1997-01-27 deepen_tac is NOT complete when made to apply "spec" as a safe rule\!\!
1997-01-17 paulson 1997-01-17 Now with Andy Gordon's treatment of freshness to replace newN/K
1997-01-07 paulson 1997-01-07 Incorporation of HPair into Message
1996-12-16 paulson 1996-12-16 New tactic: prove_unique_tac
1996-12-13 paulson 1996-12-13 Addition of the Hash constructor Strengthening spy_analz_tac
1996-12-05 paulson 1996-12-05 Moved much common material to Message.ML
1996-11-29 paulson 1996-11-29 Swapped arguments of Crypt (for clarity and because it is conventional)
1996-11-08 paulson 1996-11-08 Ran expandshort
1996-11-01 paulson 1996-11-01 New, purely illustrative result Crypt_synth_analz
1996-10-18 paulson 1996-10-18 Replaced excluded_middle_tac by case_tac
1996-10-08 paulson 1996-10-08 New theorem Crypt_imp_invKey_keysFor
1996-10-07 paulson 1996-10-07 New theorem Crypt_Fake_parts_insert
1996-09-26 paulson 1996-09-26 Introduction of "lost" argument Changed Enemy -> Spy Ran expandshort
1996-09-26 paulson 1996-09-26 Last working version prior to addition of "lost" component
1996-09-25 paulson 1996-09-25 Last working version prior to introduction of "lost"
1996-09-23 paulson 1996-09-23 New laws for messages
1996-09-13 paulson 1996-09-13 Reordering of premises for cut theorems, and new law MPair_synth_analz
1996-09-13 paulson 1996-09-13 Removal of obsolete thm Fake_parts_insert
1996-09-09 paulson 1996-09-09 Stronger proofs; work for Otway-Rees
1996-09-03 paulson 1996-09-03 New theorems for Fake case
1996-08-20 paulson 1996-08-20 Working version of NS, messages 1-3, WITH INTERLEAVING
1996-08-19 paulson 1996-08-19 Renaming of functions, and tidying
1996-07-29 paulson 1996-07-29 Works up to main theorem, then XXX...X
1996-07-26 paulson 1996-07-26 Auth proofs work up to the XXX...
1996-07-11 paulson 1996-07-11 Added Msg 3; works up to Says_Server_imp_Key_newK
1996-06-28 paulson 1996-06-28 Proving safety properties of authentication protocols