src/HOL/Auth/ROOT.ML
author haftmann
Fri Apr 20 11:21:42 2007 +0200 (2007-04-20)
changeset 22744 5cbe966d67a2
parent 18886 9f27383426db
child 24106 f2965bf954dc
permissions -rw-r--r--
Isar definitions are now added explicitly to code theorem table
     1 (*  Title:      HOL/Auth/ROOT
     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 no_document use_thy "NatPair";
    10 
    11 set timing;
    12 
    13 (* Conventional protocols: rely on 
    14    conventional Message, Event and Public *)
    15 
    16 (*Shared-key protocols*)
    17 time_use_thy "NS_Shared";
    18 time_use_thy "Kerberos_BAN";
    19 time_use_thy "Kerberos_BAN_Gets";
    20 time_use_thy "KerberosIV";
    21 time_use_thy "KerberosIV_Gets";
    22 time_use_thy "KerberosV";
    23 time_use_thy "OtwayRees";
    24 time_use_thy "OtwayRees_AN";
    25 time_use_thy "OtwayRees_Bad";
    26 time_use_thy "OtwayReesBella";
    27 time_use_thy "WooLam";
    28 time_use_thy "Recur";
    29 time_use_thy "Yahalom";
    30 time_use_thy "Yahalom2";
    31 time_use_thy "Yahalom_Bad";
    32 time_use_thy "ZhouGollmann";
    33 
    34 (*Public-key protocols*)
    35 time_use_thy "NS_Public_Bad";
    36 time_use_thy "NS_Public";
    37 time_use_thy "TLS";
    38 time_use_thy "CertifiedEmail";
    39 
    40 (*Smartcard protocols: rely on conventional Message and on new
    41   EventSC and Smartcard *)
    42 
    43 with_path "Smartcard" time_use_thy "ShoupRubin";
    44 with_path "Smartcard" time_use_thy "ShoupRubinBella";
    45 
    46 (*Blanqui's "guard" concept: protocol-independent secrecy*)
    47 with_path "Guard" (app time_use_thy)
    48   ["P1", "P2", "Guard_NS_Public", "Guard_OtwayRees", "Guard_Yahalom", "Proto"];