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