1997-12-24 paulson 1997-12-24 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
1997-12-16 wenzelm 1997-12-16 expandshort;
1997-12-05 wenzelm 1997-12-05 adapted proofs to cope with simprocs nat_cancel (by Stefan Berghofer);
1997-11-18 paulson 1997-11-18 Crypt_imp_keysFor: version of Crypt_imp_invKey_keysFor for shared keys
1997-11-05 paulson 1997-11-05 Tidied Key_supply3
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-10-21 paulson 1997-10-21 Many minor speedups: 1. Some use of rewriting with expand_ifs instead of addsplits[expand_if] 2. Faster proof of new_keys_not_used 3. New version of shrK_neq (no longer refers to "range")
1997-10-17 nipkow 1997-10-17 setloop split_tac -> addsplits
1997-10-17 nipkow 1997-10-17 Removed image_eqI from simpset because of clash with neq_shrK.
1997-09-29 paulson 1997-09-29 Step_tac -> Safe_tac
1997-09-25 paulson 1997-09-25 Changed some proofs to use Clarify_tac
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-17 paulson 1997-09-17 Removed the simprule imp_disjL from the analz_image_..._ss to boost speed
1997-09-16 paulson 1997-09-16 Having "addcongs [if_weak_cong]" in analz_image_..._ss makes simplification faster
1997-09-11 paulson 1997-09-11 Now uses the generic induct_tac
1997-07-22 paulson 1997-07-22 Now possibility_tac and basic_possibility_tac are explicit functions, in order to delay the evaluation of \!simpset
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 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".
1997-07-01 paulson 1997-07-01 Reordered rules in analz_image_freshK_ss to improve clarity
1997-07-01 paulson 1997-07-01 Deleted the obsolete operators newK, newN and nPair
1997-06-26 nipkow 1997-06-26 set_of_list -> set
1997-06-19 paulson 1997-06-19 Made proofs more concise by replacing calls to spy_analz_tac by uses of analz_insert_eq in rewriting
1997-06-18 paulson 1997-06-18 Removed Says_Crypt_lost and Says_Crypt_not_lost. Installed not_lost_tac. Deleted unused theorems initState_subset and seesD
1997-06-05 nipkow 1997-06-05 Modified a few defs and proofs because of the changes to theory Finite.thy.
1997-05-15 oheimb 1997-05-15 renamed unsafe_addss to addss
1997-05-07 paulson 1997-05-07 Conversion to use blast_tac (with other improvements)
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-17 paulson 1997-01-17 Now with Andy Gordon's treatment of freshness to replace newN/K
1996-12-19 paulson 1996-12-19 Extensive tidying and simplification, largely stemming from changing newN and newK to take an integer argument
1996-12-13 paulson 1996-12-13 Temporary additions (random) for the nested Otway-Rees protocol They will need to be rationalized
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-28 paulson 1996-11-28 Weaking of injectivity assumptions for newK and newN: they are no longer assumed injective over all traces, merely over the length of a trace
1996-11-05 paulson 1996-11-05 Simplified new_keys_not_seen, etc.: replaced the union over all agents by the Spy alone. Proofs run faster and they do not have to be set up in terms of a previous lemma.
1996-10-28 paulson 1996-10-28 Tidied up a big mess in UN_parts_sees_Says
1996-10-24 paulson 1996-10-24 New theorem Crypt_Spy_analz_lost; improvements to spy_analz_tac; ex_strip_tac
1996-10-18 paulson 1996-10-18 Deleted obsolete rewrites (they are now in HOL/simpdata)
1996-10-09 paulson 1996-10-09 New version of axiom sees1_Says: Previously it only allowed the SENDER to see the content of messages... Now instead the RECIPIENT sees the messages. This change had no effect on subsequent proofs because protocol rules refer specifically to the relevant messages sent to an agent.
1996-10-08 paulson 1996-10-08 Put in the theorem Says_Crypt_not_lost
1996-10-07 paulson 1996-10-07 Simple tidying
1996-10-01 paulson 1996-10-01 Moved sees_lost_agent_subset_sees_Spy to common file
1996-09-30 paulson 1996-09-30 Removed some dead wood. Transferred lemmas used to prove analz_image_newK to Shared.ML
1996-09-26 paulson 1996-09-26 Introduction of "lost" argument Changed Enemy -> Spy Ran expandshort
1996-09-25 paulson 1996-09-25 Last working version prior to introduction of "lost"
1996-09-23 paulson 1996-09-23 Removal of the Notes constructor
1996-09-13 paulson 1996-09-13 Abstraction of enemy_analz_tac over its argument
1996-09-13 paulson 1996-09-13 Addition of enemy_analz_tac and safe_solver Use of AddIffs for theorems about keys
1996-09-09 paulson 1996-09-09 "bad" set simplifies statements of many theorems
1996-09-09 paulson 1996-09-09 Stronger proofs; work for Otway-Rees
1996-09-03 paulson 1996-09-03 Renaming and simplification
1996-08-21 paulson 1996-08-21 Separation of theory Event into two parts: Shared for general shared-key material NS_Shared for the Needham-Schroeder shared-key protocol