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
wenzelm@24106
     1
(*  Title:      HOL/Auth/ROOT.ML
paulson@1944
     2
    ID:         $Id$
paulson@1944
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@1944
     4
    Copyright   1996  University of Cambridge
paulson@1944
     5
paulson@1971
     6
Root file for protocol proofs.
paulson@1944
     7
*)
paulson@1944
     8
wenzelm@24106
     9
use_thys [
wenzelm@17394
    10
paulson@18886
    11
(* Conventional protocols: rely on 
paulson@18886
    12
   conventional Message, Event and Public *)
paulson@1944
    13
paulson@2325
    14
(*Shared-key protocols*)
wenzelm@24106
    15
  "NS_Shared",
wenzelm@24106
    16
  "Kerberos_BAN",
wenzelm@24106
    17
  "Kerberos_BAN_Gets",
wenzelm@24106
    18
  "KerberosIV",
wenzelm@24106
    19
  "KerberosIV_Gets",
wenzelm@24106
    20
  "KerberosV",
wenzelm@24106
    21
  "OtwayRees",
wenzelm@24106
    22
  "OtwayRees_AN",
wenzelm@24106
    23
  "OtwayRees_Bad",
wenzelm@24106
    24
  "OtwayReesBella",
wenzelm@24106
    25
  "WooLam",
wenzelm@24106
    26
  "Recur",
wenzelm@24106
    27
  "Yahalom",
wenzelm@24106
    28
  "Yahalom2",
wenzelm@24106
    29
  "Yahalom_Bad",
wenzelm@24106
    30
  "ZhouGollmann",
paulson@14145
    31
paulson@2325
    32
(*Public-key protocols*)
wenzelm@24106
    33
  "NS_Public_Bad",
wenzelm@24106
    34
  "NS_Public",
wenzelm@24106
    35
  "TLS",
wenzelm@24106
    36
  "CertifiedEmail",
paulson@13508
    37
paulson@18886
    38
(*Smartcard protocols: rely on conventional Message and on new
paulson@18886
    39
  EventSC and Smartcard *)
paulson@18886
    40
wenzelm@24106
    41
  "Smartcard/ShoupRubin",
wenzelm@24106
    42
  "Smartcard/ShoupRubinBella",
paulson@18886
    43
paulson@13508
    44
(*Blanqui's "guard" concept: protocol-independent secrecy*)
wenzelm@24106
    45
  "Guard/P1",
wenzelm@24106
    46
  "Guard/P2",
wenzelm@24106
    47
  "Guard/Guard_NS_Public",
wenzelm@24106
    48
  "Guard/Guard_OtwayRees",
wenzelm@24106
    49
  "Guard/Guard_Yahalom",
wenzelm@24106
    50
  "Guard/Proto"
wenzelm@24106
    51
];