| 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
|