| Tue, 03 Sep 1996 18:24:42 +0200 |
paulson |
Renaming and simplification
|
changeset |
files
|
| Tue, 03 Sep 1996 17:54:39 +0200 |
paulson |
Renaming and simplification
|
changeset |
files
|
| Tue, 03 Sep 1996 16:43:31 +0200 |
paulson |
Initial working proof of Otway-Rees protocol
|
changeset |
files
|
| Fri, 23 Aug 1996 13:12:51 +0200 |
nipkow |
Swaped two conditions in the completeness statement.
|
changeset |
files
|
| Fri, 23 Aug 1996 13:03:02 +0200 |
nipkow |
Generalized my_lemma1: (c3,s3) |--> cs3
|
changeset |
files
|
| Thu, 22 Aug 1996 12:27:01 +0200 |
paulson |
Now deepen_tac can take advantage of wrappers --
|
changeset |
files
|
| Thu, 22 Aug 1996 12:24:58 +0200 |
paulson |
Proved mem_if
|
changeset |
files
|
| Thu, 22 Aug 1996 12:24:25 +0200 |
paulson |
Proved set_of_list_subset_Cons
|
changeset |
files
|
| Thu, 22 Aug 1996 12:18:21 +0200 |
paulson |
For building the security theory as a separate database
|
changeset |
files
|
| Wed, 21 Aug 1996 13:25:27 +0200 |
paulson |
Separation of theory Event into two parts:
|
changeset |
files
|
| Wed, 21 Aug 1996 13:22:23 +0200 |
paulson |
Addition of message NS5
|
changeset |
files
|
| Wed, 21 Aug 1996 11:43:37 +0200 |
paulson |
Tidying: removing redundant args in classical reasoner calls
|
changeset |
files
|
| Wed, 21 Aug 1996 11:00:04 +0200 |
paulson |
Added le_eq_less_Suc; fixed some comments;
|
changeset |
files
|
| Tue, 20 Aug 1996 18:53:17 +0200 |
paulson |
Working version of NS, messages 1-4!
|
changeset |
files
|