src/HOL/Auth/Message.thy
2004-07-11 wenzelm 2004-07-11 local_cla/simpset_of;
2003-09-23 paulson 2003-09-23 Removal of the Key_supply axiom (affects many possbility proofs) and minor changes
2003-09-04 paulson 2003-09-04 new, separate specifications
2003-08-12 paulson 2003-08-12 ZhouGollmann: new example (fair non-repudiation protocol)
2003-07-24 paulson 2003-07-24 Tidying and replacement of some axioms by specifications
2003-05-05 paulson 2003-05-05 improved presentation of HOL/Auth theories
2003-04-26 paulson 2003-04-26 converting more HOL-Auth to new-style theories
2003-04-25 paulson 2003-04-25 Changes required by the certified email protocol Public-key model now provides separate signature/encryption keys and also long-term symmetric keys.
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-04-24 paulson 2001-04-24 (rough) conversion of Auth/Recur to Isar format
2001-04-12 paulson 2001-04-12 converted many HOL/Auth theories to Isar scripts
2001-04-09 paulson 2001-04-09 new theorem Fake_parts_insert_in_Un
2001-03-29 paulson 2001-03-29 misc tidying; changing the predicate isSymKey to the set symKeys
2001-03-05 paulson 2001-03-05 a few basic X-symbols
2001-03-02 paulson 2001-03-02 conversion of Message.thy to Isar format
2001-01-09 nipkow 2001-01-09 `` -> ` and ``` -> ``
2000-08-24 paulson 2000-08-24 xsymbols for {| and |}
1999-07-21 paulson 1999-07-21 tweaked proofs to handle new freeness reasoning for data c onstructors
1999-06-10 paulson 1999-06-10 new translation to allow images over Nonce
1998-10-16 paulson 1998-10-16 parent is Main
1998-08-03 paulson 1998-08-03 Better comments
1998-07-24 berghofe 1998-07-24 Adapted to new datatype package.
1998-06-30 berghofe 1998-06-30 Adapted to new inductive definition package.
1997-09-11 paulson 1997-09-11 Split base cases from "msg" to "atomic" in order to reduce the number of freeness theorems
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-13 paulson 1996-12-13 Addition of the Hash constructor Strengthening spy_analz_tac
1996-11-29 paulson 1996-11-29 Swapped arguments of Crypt (for clarity and because it is conventional)
1996-10-24 paulson 1996-10-24 Removal of unused predicate isSpy
1996-09-26 paulson 1996-09-26 Introduction of "lost" argument Changed Enemy -> Spy Ran expandshort
1996-09-23 paulson 1996-09-23 Simplification of definition of synth
1996-09-03 paulson 1996-09-03 Fixed pretty-printing of {|...|}
1996-08-19 paulson 1996-08-19 Renaming of functions, and tidying
1996-06-28 paulson 1996-06-28 Proving safety properties of authentication protocols