src/HOL/Auth/KerberosIV.ML
changeset 9000 c20d58286a51
parent 8954 4fbdda40bb5f
child 10833 c0844a30ea4e
equal deleted inserted replaced
8999:ad8260dc6e4a 9000:c20d58286a51
     5 
     5 
     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 set timing;
    11 
    11 
    12 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];
    13 
    13 
    14 
    14 
    15 (** Reversed traces **)
    15 (** Reversed traces **)