| Thu, 11 Sep 2014 19:32:36 +0200 |
blanchet |
updated news
|
file |
diff |
annotate
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:37:06 +0100 |
blanchet |
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
|
file |
diff |
annotate
|
| Sun, 20 Nov 2011 17:32:27 +0100 |
wenzelm |
updated comment;
|
file |
diff |
annotate
|
| Fri, 18 Feb 2011 15:46:13 +0100 |
wenzelm |
modernized specifications;
|
file |
diff |
annotate
|
| Wed, 29 Dec 2010 17:34:41 +0100 |
wenzelm |
explicit file specifications -- avoid secondary load path;
|
file |
diff |
annotate
|
| Thu, 22 Jul 2010 18:08:39 +0200 |
wenzelm |
updated some headers;
|
file |
diff |
annotate
|
| Wed, 10 Mar 2010 15:33:13 -0800 |
huffman |
convert TLS to use Nat_Bijection library
|
file |
diff |
annotate
|
| Mon, 01 Mar 2010 13:40:23 +0100 |
haftmann |
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 14:43:18 +0200 |
wenzelm |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
file |
diff |
annotate
|
| Fri, 13 Feb 2009 09:54:47 +0100 |
nipkow |
Moved Nat_Int_Bij into Library
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 22:37:20 +0200 |
nipkow |
Replaced Library/NatPair by Nat_Int_Bij.
|
file |
diff |
annotate
|
| Wed, 11 Jul 2007 11:14:51 +0200 |
berghofe |
Adapted to new inductive definition package.
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
| Thu, 28 Sep 2006 23:42:35 +0200 |
wenzelm |
replaced syntax/translations by abbreviation;
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
| Thu, 24 Jul 2003 16:36:29 +0200 |
paulson |
Tidying and replacement of some axioms by specifications
|
file |
diff |
annotate
|
| Mon, 05 May 2003 18:22:01 +0200 |
paulson |
improved presentation of HOL/Auth theories
|
file |
diff |
annotate
|
| Fri, 25 Apr 2003 11:18:14 +0200 |
paulson |
Changes required by the certified email protocol
|
file |
diff |
annotate
|
| Sat, 17 Aug 2002 14:55:08 +0200 |
paulson |
tidying of Isar scripts
|
file |
diff |
annotate
|
| Wed, 03 Oct 2001 20:54:16 +0200 |
wenzelm |
tuned parentheses in relational expressions;
|
file |
diff |
annotate
|
| Tue, 08 May 2001 15:56:57 +0200 |
paulson |
conversion of Auth/TLS to Isar script
|
file |
diff |
annotate
|
| Thu, 29 Mar 2001 10:44:37 +0200 |
paulson |
misc tidying; changing the predicate isSymKey to the set symKeys
|
file |
diff |
annotate
|
| Tue, 27 Feb 2001 16:13:23 +0100 |
paulson |
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
|
file |
diff |
annotate
|
| Tue, 16 Feb 1999 10:54:55 +0100 |
paulson |
tidying in conjuntion with the TISSEC paper; replaced (unit option)
|
file |
diff |
annotate
|
| Fri, 16 Oct 1998 12:23:07 +0200 |
paulson |
changed tags from 0, 1 to None, Some() to avoid special treatment of 0
|
file |
diff |
annotate
|
| Tue, 08 Sep 1998 15:17:11 +0200 |
paulson |
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
|
file |
diff |
annotate
|
| Fri, 21 Aug 1998 16:14:34 +0200 |
paulson |
Tidying
|
file |
diff |
annotate
|
| Wed, 24 Jun 1998 10:30:29 +0200 |
paulson |
Trivial change to be more like paper
|
file |
diff |
annotate
|
| Tue, 16 Dec 1997 15:15:38 +0100 |
paulson |
Simplified SpyKeys and ClientKeyExch as suggested by James Margetson
|
file |
diff |
annotate
|
| Tue, 11 Nov 1997 11:16:18 +0100 |
paulson |
Fixed spelling error
|
file |
diff |
annotate
|
| Wed, 01 Oct 1997 13:41:38 +0200 |
paulson |
Fixed ServerResume to check for ServerHello instead of making a new NB
|
file |
diff |
annotate
|
| Wed, 01 Oct 1997 12:07:07 +0200 |
paulson |
Exchanged the M and SID fields of the FINISHED messages to simplify proofs
|
file |
diff |
annotate
|
| Tue, 30 Sep 1997 11:03:55 +0200 |
paulson |
Client, Server certificates now sent using the separate Certificate rule,
|
file |
diff |
annotate
|
| Mon, 29 Sep 1997 11:46:33 +0200 |
paulson |
Renamed XA, XB to PA, PB and removed the certificate from Client Verify
|
file |
diff |
annotate
|
| Thu, 25 Sep 1997 12:19:41 +0200 |
paulson |
Deleted obsolete axioms inj_serverK and isSym_serverK
|
file |
diff |
annotate
|
| Wed, 24 Sep 1997 12:27:53 +0200 |
paulson |
sessionK now indexed by nat instead of bool.
|
file |
diff |
annotate
|
| Mon, 22 Sep 1997 13:17:29 +0200 |
paulson |
Simplified SpyKeys to use sessionK instead of clientK and serverK
|
file |
diff |
annotate
|
| Fri, 19 Sep 1997 18:27:31 +0200 |
paulson |
First working version with Oops event for session keys
|
file |
diff |
annotate
|
| Fri, 19 Sep 1997 16:12:21 +0200 |
paulson |
Full version of TLS including session resumption, but no Oops
|
file |
diff |
annotate
|
| Thu, 18 Sep 1997 13:24:04 +0200 |
paulson |
Global change: lost->bad and sees Spy->spies
|
file |
diff |
annotate
|
| Wed, 17 Sep 1997 16:37:21 +0200 |
paulson |
Now with the sessionK constant and new events ClientAccepts and ServerAccepts
|
file |
diff |
annotate
|
| Tue, 16 Sep 1997 14:40:01 +0200 |
paulson |
Addition of SessionIDs to the Hello and Finished messages
|
file |
diff |
annotate
|
| Tue, 16 Sep 1997 13:32:22 +0200 |
paulson |
TLS now with a distinction between premaster secret and master secret
|
file |
diff |
annotate
|
| Mon, 14 Jul 1997 12:47:21 +0200 |
paulson |
Changing "lost" from a parameter of protocol definitions to a constant.
|
file |
diff |
annotate
|
| Fri, 11 Jul 1997 13:30:01 +0200 |
paulson |
Now uses the Notes constructor to distinguish the Client (who has chosen M)
|
file |
diff |
annotate
|
| Mon, 07 Jul 1997 10:49:14 +0200 |
paulson |
New proofs involving CERTIFICATE VERIFY
|
file |
diff |
annotate
|
| Fri, 04 Jul 1997 17:34:55 +0200 |
paulson |
New constant "certificate"--just an abbreviation
|
file |
diff |
annotate
|
| Tue, 01 Jul 1997 17:37:42 +0200 |
paulson |
More realistic model: the Spy can compute clientK and serverK
|
file |
diff |
annotate
|
| Tue, 01 Jul 1997 11:11:42 +0200 |
paulson |
Baby TLS. Proofs work, but model seems unrealistic
|
file |
diff |
annotate
|