added session entry point theories
authorhaftmann
Mon Sep 21 15:33:40 2009 +0200 (2009-09-21)
changeset 326328ae912371831
parent 32631 2489e3c3562b
child 32633 4ba4bfa08749
child 32694 0264f360438d
added session entry point theories
src/HOL/Auth/Auth_Public.thy
src/HOL/Auth/Auth_Shared.thy
src/HOL/Auth/Guard/Auth_Guard_Public.thy
src/HOL/Auth/Guard/Auth_Guard_Shared.thy
src/HOL/Auth/ROOT.ML
src/HOL/Auth/Smartcard/Auth_Smartcard.thy
src/HOL/IsaMakefile
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Auth/Auth_Public.thy	Mon Sep 21 15:33:40 2009 +0200
     1.3 @@ -0,0 +1,15 @@
     1.4 +(*  Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.5 +    Copyright   1996  University of Cambridge
     1.6 +*)
     1.7 +
     1.8 +header {* Conventional protocols: rely on conventional Message, Event and Public -- Public-key protocols *}
     1.9 +
    1.10 +theory Auth_Public
    1.11 +imports
    1.12 +  "NS_Public_Bad"
    1.13 +  "NS_Public"
    1.14 +  "TLS"
    1.15 +  "CertifiedEmail"
    1.16 +begin
    1.17 +
    1.18 +end
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Auth/Auth_Shared.thy	Mon Sep 21 15:33:40 2009 +0200
     2.3 @@ -0,0 +1,27 @@
     2.4 +(*  Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.5 +    Copyright   1996  University of Cambridge
     2.6 +*)
     2.7 +
     2.8 +header {* Conventional protocols: rely on conventional Message, Event and Public -- Shared-key protocols *}
     2.9 +
    2.10 +theory Auth_Shared
    2.11 +imports
    2.12 +  "NS_Shared"
    2.13 +  "Kerberos_BAN"
    2.14 +  "Kerberos_BAN_Gets"
    2.15 +  "KerberosIV"
    2.16 +  "KerberosIV_Gets"
    2.17 +  "KerberosV"
    2.18 +  "OtwayRees"
    2.19 +  "OtwayRees_AN"
    2.20 +  "OtwayRees_Bad"
    2.21 +  "OtwayReesBella"
    2.22 +  "WooLam"
    2.23 +  "Recur"
    2.24 +  "Yahalom"
    2.25 +  "Yahalom2"
    2.26 +  "Yahalom_Bad"
    2.27 +  "ZhouGollmann"
    2.28 +begin
    2.29 +
    2.30 +end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Auth/Guard/Auth_Guard_Public.thy	Mon Sep 21 15:33:40 2009 +0200
     3.3 @@ -0,0 +1,15 @@
     3.4 +(*  Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.5 +    Copyright   1996  University of Cambridge
     3.6 +*)
     3.7 +
     3.8 +header {* Blanqui's "guard" concept: protocol-independent secrecy *}
     3.9 +
    3.10 +theory Auth_Guard_Public
    3.11 +imports
    3.12 +  "P1"
    3.13 +  "P2"
    3.14 +  "Guard_NS_Public"
    3.15 +  "Proto"
    3.16 +begin
    3.17 +
    3.18 +end
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Auth/Guard/Auth_Guard_Shared.thy	Mon Sep 21 15:33:40 2009 +0200
     4.3 @@ -0,0 +1,13 @@
     4.4 +(*  Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.5 +    Copyright   1996  University of Cambridge
     4.6 +*)
     4.7 +
     4.8 +header {* Blanqui's "guard" concept: protocol-independent secrecy *}
     4.9 +
    4.10 +theory Auth_Guard_Shared
    4.11 +imports
    4.12 +  "Guard_OtwayRees"
    4.13 +  "Guard_Yahalom"
    4.14 +begin
    4.15 +
    4.16 +end
     5.1 --- a/src/HOL/Auth/ROOT.ML	Mon Sep 21 15:33:40 2009 +0200
     5.2 +++ b/src/HOL/Auth/ROOT.ML	Mon Sep 21 15:33:40 2009 +0200
     5.3 @@ -1,51 +1,2 @@
     5.4 -(*  Title:      HOL/Auth/ROOT.ML
     5.5 -    ID:         $Id$
     5.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     5.7 -    Copyright   1996  University of Cambridge
     5.8  
     5.9 -Root file for protocol proofs.
    5.10 -*)
    5.11 -
    5.12 -use_thys [
    5.13 -
    5.14 -(* Conventional protocols: rely on 
    5.15 -   conventional Message, Event and Public *)
    5.16 -
    5.17 -(*Shared-key protocols*)
    5.18 -  "NS_Shared",
    5.19 -  "Kerberos_BAN",
    5.20 -  "Kerberos_BAN_Gets",
    5.21 -  "KerberosIV",
    5.22 -  "KerberosIV_Gets",
    5.23 -  "KerberosV",
    5.24 -  "OtwayRees",
    5.25 -  "OtwayRees_AN",
    5.26 -  "OtwayRees_Bad",
    5.27 -  "OtwayReesBella",
    5.28 -  "WooLam",
    5.29 -  "Recur",
    5.30 -  "Yahalom",
    5.31 -  "Yahalom2",
    5.32 -  "Yahalom_Bad",
    5.33 -  "ZhouGollmann",
    5.34 -
    5.35 -(*Public-key protocols*)
    5.36 -  "NS_Public_Bad",
    5.37 -  "NS_Public",
    5.38 -  "TLS",
    5.39 -  "CertifiedEmail",
    5.40 -
    5.41 -(*Smartcard protocols: rely on conventional Message and on new
    5.42 -  EventSC and Smartcard *)
    5.43 -
    5.44 -  "Smartcard/ShoupRubin",
    5.45 -  "Smartcard/ShoupRubinBella",
    5.46 -
    5.47 -(*Blanqui's "guard" concept: protocol-independent secrecy*)
    5.48 -  "Guard/P1",
    5.49 -  "Guard/P2",
    5.50 -  "Guard/Guard_NS_Public",
    5.51 -  "Guard/Guard_OtwayRees",
    5.52 -  "Guard/Guard_Yahalom",
    5.53 -  "Guard/Proto"
    5.54 -];
    5.55 +use_thys ["Auth_Shared", "Auth_Public", "Smartcard/Auth_Smartcard", "Guard/Auth_Guard_Shared", "Guard/Auth_Guard_Public"];
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Auth/Smartcard/Auth_Smartcard.thy	Mon Sep 21 15:33:40 2009 +0200
     6.3 @@ -0,0 +1,13 @@
     6.4 +(*  Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     6.5 +    Copyright   1996  University of Cambridge
     6.6 +*)
     6.7 +
     6.8 +header {* Smartcard protocols: rely on conventional Message and on new EventSC and Smartcard *}
     6.9 +
    6.10 +theory Auth_Smartcard
    6.11 +imports
    6.12 +  "ShoupRubin"
    6.13 +  "ShoupRubinBella"
    6.14 +begin
    6.15 +
    6.16 +end
     7.1 --- a/src/HOL/IsaMakefile	Mon Sep 21 15:33:40 2009 +0200
     7.2 +++ b/src/HOL/IsaMakefile	Mon Sep 21 15:33:40 2009 +0200
     7.3 @@ -619,6 +619,10 @@
     7.4  HOL-Auth: HOL $(LOG)/HOL-Auth.gz
     7.5  
     7.6  $(LOG)/HOL-Auth.gz: $(OUT)/HOL 						\
     7.7 +  Auth/Auth_Shared.thy Auth/Auth_Public.thy Auth/All_Symmetric.thy		\
     7.8 +  Auth/Guard/Auth_Guard_Shared.thy		\
     7.9 +  Auth/Guard/Auth_Guard_Public.thy		\
    7.10 +  Auth/Smartcard/Auth_Smartcard.thy Auth/All_Symmetric.thy		\
    7.11    Auth/CertifiedEmail.thy Auth/Event.thy Auth/Message.thy		\
    7.12    Auth/NS_Public.thy Auth/NS_Public_Bad.thy Auth/NS_Shared.thy		\
    7.13    Auth/OtwayRees.thy Auth/OtwayReesBella.thy Auth/OtwayRees_AN.thy	\