src/HOL/Auth/ROOT.ML

 HOL_quantifiers := false;
 
 (*Shared-key protocols*)
 time_use_thy "NS_Shared";
 time_use_thy "Kerberos_BAN";
+time_use_thy "KerberosIV";
 time_use_thy "OtwayRees";
 time_use_thy "OtwayRees_AN";
 time_use_thy "OtwayRees_Bad";
 time_use_thy "WooLam";
 time_use_thy "Recur";