src/HOL/Auth/ROOT.ML

T.end_position_of;
tuned;

(*  Title:      HOL/Auth/ROOT.ML
    ID:         $Id$
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1996  University of Cambridge

Root file for protocol proofs.
*)

no_document use_thy "NatPair";

use_thys [

(* Conventional protocols: rely on 
   conventional Message, Event and Public *)

(*Shared-key protocols*)
  "NS_Shared",
  "Kerberos_BAN",
  "Kerberos_BAN_Gets",
  "KerberosIV",
  "KerberosIV_Gets",
  "KerberosV",
  "OtwayRees",
  "OtwayRees_AN",
  "OtwayRees_Bad",
  "OtwayReesBella",
  "WooLam",
  "Recur",
  "Yahalom",
  "Yahalom2",
  "Yahalom_Bad",
  "ZhouGollmann",

(*Public-key protocols*)
  "NS_Public_Bad",
  "NS_Public",
  "TLS",
  "CertifiedEmail",

(*Smartcard protocols: rely on conventional Message and on new
  EventSC and Smartcard *)

  "Smartcard/ShoupRubin",
  "Smartcard/ShoupRubinBella",

(*Blanqui's "guard" concept: protocol-independent secrecy*)
  "Guard/P1",
  "Guard/P2",
  "Guard/Guard_NS_Public",
  "Guard/Guard_OtwayRees",
  "Guard/Guard_Yahalom",
  "Guard/Proto"
];