2002-08-17 paulson 2002-08-17 tidying of Isar scripts
2001-12-07 paulson 2001-12-07 Slightly generalized the agents' knowledge theorems
2001-04-27 paulson 2001-04-27 better treatment of methods: uses Method.ctxt_args to refer to current simpset and claset. Needed to fix problems with Recur.thy
2001-03-29 paulson 2001-03-29 misc tidying; changing the predicate isSymKey to the set symKeys
2001-02-13 paulson 2001-02-13 partial conversion to Isar script style simplified unicity proofs
2001-01-09 nipkow 2001-01-09 `` -> ` and ``` -> ``
1998-07-24 berghofe 1998-07-24 Adapted to new datatype package.
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-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 Deleted the obsolete operators newK, newN and nPair
1997-06-05 nipkow 1997-06-05 Modified a few defs and proofs because of the changes to theory Finite.thy.
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 Updating of comments
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-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-07 paulson 1996-10-07 Simple tidying
1996-09-26 paulson 1996-09-26 Introduction of "lost" argument Changed Enemy -> Spy Ran expandshort
1996-09-23 paulson 1996-09-23 Removal of the Notes constructor
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