| changeset 3445 | 96fcfbfa4fb5 |
| parent 3432 | 04412cfe6861 |
| child 3465 | e85c24717cad |
| 3444:919de2cb3487 | 3445:96fcfbfa4fb5 |
|---|---|
1 (* Title: HOL/Auth/Yahalom |
1 (* Title: HOL/Auth/Yahalom2 |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1996 University of Cambridge |
4 Copyright 1996 University of Cambridge |
5 |
5 |
6 Inductive relation "yahalom" for the Yahalom protocol, Variant 2. |
6 Inductive relation "yahalom" for the Yahalom protocol, Variant 2. |