src/HOL/Auth/ROOT.ML
author haftmann
Fri Jan 02 08:12:46 2009 +0100 (2009-01-02)
changeset 29332 edc1e2a56398
parent 28098 c92850d2d16c
child 32632 8ae912371831
permissions -rw-r--r--
named code theorem for Fract_norm
     1 (*  Title:      HOL/Auth/ROOT.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1996  University of Cambridge
     5 
     6 Root file for protocol proofs.
     7 *)
     8 
     9 use_thys [
    10 
    11 (* Conventional protocols: rely on 
    12    conventional Message, Event and Public *)
    13 
    14 (*Shared-key protocols*)
    15   "NS_Shared",
    16   "Kerberos_BAN",
    17   "Kerberos_BAN_Gets",
    18   "KerberosIV",
    19   "KerberosIV_Gets",
    20   "KerberosV",
    21   "OtwayRees",
    22   "OtwayRees_AN",
    23   "OtwayRees_Bad",
    24   "OtwayReesBella",
    25   "WooLam",
    26   "Recur",
    27   "Yahalom",
    28   "Yahalom2",
    29   "Yahalom_Bad",
    30   "ZhouGollmann",
    31 
    32 (*Public-key protocols*)
    33   "NS_Public_Bad",
    34   "NS_Public",
    35   "TLS",
    36   "CertifiedEmail",
    37 
    38 (*Smartcard protocols: rely on conventional Message and on new
    39   EventSC and Smartcard *)
    40 
    41   "Smartcard/ShoupRubin",
    42   "Smartcard/ShoupRubinBella",
    43 
    44 (*Blanqui's "guard" concept: protocol-independent secrecy*)
    45   "Guard/P1",
    46   "Guard/P2",
    47   "Guard/Guard_NS_Public",
    48   "Guard/Guard_OtwayRees",
    49   "Guard/Guard_Yahalom",
    50   "Guard/Proto"
    51 ];