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