src/HOL/Auth/Yahalom.thy
Wed, 11 Jul 2007 11:14:51 +0200 berghofe Adapted to new inductive definition package.
Wed, 04 Jan 2006 16:13:53 +0100 paulson a few more named lemmas
Fri, 07 Oct 2005 20:41:10 +0200 nipkow changes due to new neq_simproc in simpdata.ML
Thu, 15 Sep 2005 17:16:55 +0200 wenzelm fixed document;
Fri, 17 Jun 2005 16:12:49 +0200 haftmann migrated theory headers to new format
Fri, 26 Sep 2003 10:34:28 +0200 paulson Conversion of all main protocols from "Shared" to "Public".
Tue, 23 Sep 2003 15:41:33 +0200 paulson Removal of the Key_supply axiom (affects many possbility proofs) and minor
Mon, 05 May 2003 18:22:01 +0200 paulson improved presentation of HOL/Auth theories
Sat, 26 Apr 2003 12:38:42 +0200 paulson converting more HOL-Auth to new-style theories
Sat, 17 Aug 2002 14:55:08 +0200 paulson tidying of Isar scripts
Wed, 03 Oct 2001 20:54:16 +0200 wenzelm tuned parentheses in relational expressions;
Thu, 12 Apr 2001 12:45:05 +0200 paulson converted many HOL/Auth theories to Isar scripts
Tue, 27 Feb 2001 16:13:23 +0100 paulson Some X-symbols for <notin>, <noteq>, <forall>, <exists>
Wed, 10 Mar 1999 10:42:57 +0100 paulson updating both Yahalom protocols to the Gets model
Tue, 08 Sep 1998 15:17:11 +0200 paulson Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
Fri, 21 Aug 1998 16:14:34 +0200 paulson Tidying
Thu, 08 Jan 1998 18:10:34 +0100 paulson Expressed most Oops rules using Notes instead of Says, and other tidying
Tue, 21 Oct 1997 10:39:27 +0200 paulson Many minor speedups:
Thu, 18 Sep 1997 13:24:04 +0200 paulson Global change: lost->bad and sees Spy->spies
Fri, 05 Sep 1997 12:24:13 +0200 paulson Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
Mon, 14 Jul 1997 12:47:21 +0200 paulson Changing "lost" from a parameter of protocol definitions to a constant.
Tue, 01 Jul 1997 17:38:49 +0200 paulson Deleted a redundant A~=B in rules that refer to a previous event
Thu, 26 Jun 1997 13:20:50 +0200 nipkow set_of_list -> set
Wed, 18 Jun 1997 15:38:35 +0200 paulson Defines KeyWithNonce, which is used to prove the secrecy of NB
Fri, 17 Jan 1997 12:49:31 +0100 paulson Now with Andy Gordon's treatment of freshness to replace newN/K
Thu, 19 Dec 1996 11:58:39 +0100 paulson Extensive tidying and simplification, largely stemming from
Fri, 13 Dec 1996 11:00:44 +0100 paulson Removed needless quotation marks
Fri, 29 Nov 1996 18:03:21 +0100 paulson Swapped arguments of Crypt (for clarity and because it is conventional)
Fri, 01 Nov 1996 18:34:34 +0100 paulson Minor changes to comments
Thu, 24 Oct 1996 10:38:35 +0200 paulson New Oops message, with Server as source to ensure
Fri, 18 Oct 1996 11:42:41 +0200 paulson Addition of Reveal message
Thu, 26 Sep 1996 12:50:48 +0200 paulson Introduction of "lost" argument
Fri, 13 Sep 1996 13:16:57 +0200 paulson Addition of Yahalom protocol
Thu, 12 Sep 1996 10:40:05 +0200 paulson Tidied many proofs, using AddIffs to let equivalences take
less more (0) tip