src/HOL/Auth/Shared.ML
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