| changeset 16417 | 9bc16273c2d4 |
| parent 14945 | 7bfe4fa8a88f |
| child 16796 | 140f1e0ea846 |
| 16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
|---|---|
4 Copyright 1998 University of Cambridge |
4 Copyright 1998 University of Cambridge |
5 *) |
5 *) |
6 |
6 |
7 header{*The Kerberos Protocol, Version IV*} |
7 header{*The Kerberos Protocol, Version IV*} |
8 |
8 |
9 theory KerberosIV = Public: |
9 theory KerberosIV imports Public begin |
10 |
10 |
11 syntax |
11 syntax |
12 Kas :: agent |
12 Kas :: agent |
13 Tgs :: agent --{*the two servers are translations...*} |
13 Tgs :: agent --{*the two servers are translations...*} |
14 |
14 |