paulson@1944: (* Title: HOL/Auth/ROOT paulson@1944: ID: $Id$ paulson@1944: Author: Lawrence C Paulson, Cambridge University Computer Laboratory paulson@1944: Copyright 1996 University of Cambridge paulson@1944: paulson@1971: Root file for protocol proofs. paulson@1944: *) paulson@1944: paulson@2123: goals_limit := 1; paulson@13550: set timing; paulson@1944: paulson@2325: (*Shared-key protocols*) paulson@2530: time_use_thy "NS_Shared"; paulson@5053: time_use_thy "Kerberos_BAN"; paulson@6452: time_use_thy "KerberosIV"; paulson@2530: time_use_thy "OtwayRees"; paulson@2530: time_use_thy "OtwayRees_AN"; paulson@2530: time_use_thy "OtwayRees_Bad"; paulson@2530: time_use_thy "WooLam"; paulson@2530: time_use_thy "Recur"; paulson@2530: time_use_thy "Yahalom"; paulson@2530: time_use_thy "Yahalom2"; paulson@6400: time_use_thy "Yahalom_Bad"; paulson@14145: time_use_thy "ZhouGollmann"; paulson@14145: paulson@1944: paulson@2325: (*Public-key protocols*) paulson@2530: time_use_thy "NS_Public_Bad"; paulson@2530: time_use_thy "NS_Public"; paulson@3475: time_use_thy "TLS"; paulson@13922: time_use_thy "CertifiedEmail"; paulson@13508: paulson@13508: (*Blanqui's "guard" concept: protocol-independent secrecy*) paulson@13508: time_use_thy "Guard/P1"; paulson@13508: time_use_thy "Guard/P2"; paulson@13508: time_use_thy "Guard/NS_Public"; paulson@13508: time_use_thy "Guard/OtwayRees"; paulson@13508: time_use_thy "Guard/Yahalom"; paulson@13508: time_use_thy "Guard/Proto";