| changeset 7239 | 26685edee372 |
| parent 6452 | 6a1b393ccdc0 |
| child 7494 | 45905028bb1d |
| 7238:36e58620ffc8 | 7239:26685edee372 |
|---|---|
6 The Kerberos protocol, version IV. |
6 The Kerberos protocol, version IV. |
7 *) |
7 *) |
8 |
8 |
9 Pretty.setdepth 20; |
9 Pretty.setdepth 20; |
10 proof_timing:=true; |
10 proof_timing:=true; |
11 HOL_quantifiers := false; |
|
12 |
11 |
13 AddIffs [AuthLife_LB, ServLife_LB, AutcLife_LB, RespLife_LB, Tgs_not_bad]; |
12 AddIffs [AuthLife_LB, ServLife_LB, AutcLife_LB, RespLife_LB, Tgs_not_bad]; |
14 |
13 |
15 |
14 |
16 (** Reversed traces **) |
15 (** Reversed traces **) |