# HG changeset patch # User haftmann # Date 1253540020 -7200 # Node ID 8ae912371831115099f7b65082c7203adef13c3c # Parent 2489e3c3562bc16ce5213392183929cfb10d765d added session entry point theories diff -r 2489e3c3562b -r 8ae912371831 src/HOL/Auth/Auth_Public.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Auth/Auth_Public.thy Mon Sep 21 15:33:40 2009 +0200 @@ -0,0 +1,15 @@ +(* Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1996 University of Cambridge +*) + +header {* Conventional protocols: rely on conventional Message, Event and Public -- Public-key protocols *} + +theory Auth_Public +imports + "NS_Public_Bad" + "NS_Public" + "TLS" + "CertifiedEmail" +begin + +end diff -r 2489e3c3562b -r 8ae912371831 src/HOL/Auth/Auth_Shared.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Auth/Auth_Shared.thy Mon Sep 21 15:33:40 2009 +0200 @@ -0,0 +1,27 @@ +(* Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1996 University of Cambridge +*) + +header {* Conventional protocols: rely on conventional Message, Event and Public -- Shared-key protocols *} + +theory Auth_Shared +imports + "NS_Shared" + "Kerberos_BAN" + "Kerberos_BAN_Gets" + "KerberosIV" + "KerberosIV_Gets" + "KerberosV" + "OtwayRees" + "OtwayRees_AN" + "OtwayRees_Bad" + "OtwayReesBella" + "WooLam" + "Recur" + "Yahalom" + "Yahalom2" + "Yahalom_Bad" + "ZhouGollmann" +begin + +end diff -r 2489e3c3562b -r 8ae912371831 src/HOL/Auth/Guard/Auth_Guard_Public.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Auth/Guard/Auth_Guard_Public.thy Mon Sep 21 15:33:40 2009 +0200 @@ -0,0 +1,15 @@ +(* Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1996 University of Cambridge +*) + +header {* Blanqui's "guard" concept: protocol-independent secrecy *} + +theory Auth_Guard_Public +imports + "P1" + "P2" + "Guard_NS_Public" + "Proto" +begin + +end diff -r 2489e3c3562b -r 8ae912371831 src/HOL/Auth/Guard/Auth_Guard_Shared.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Auth/Guard/Auth_Guard_Shared.thy Mon Sep 21 15:33:40 2009 +0200 @@ -0,0 +1,13 @@ +(* Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1996 University of Cambridge +*) + +header {* Blanqui's "guard" concept: protocol-independent secrecy *} + +theory Auth_Guard_Shared +imports + "Guard_OtwayRees" + "Guard_Yahalom" +begin + +end diff -r 2489e3c3562b -r 8ae912371831 src/HOL/Auth/ROOT.ML --- a/src/HOL/Auth/ROOT.ML Mon Sep 21 15:33:40 2009 +0200 +++ b/src/HOL/Auth/ROOT.ML Mon Sep 21 15:33:40 2009 +0200 @@ -1,51 +1,2 @@ -(* 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. -*) - -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" -]; +use_thys ["Auth_Shared", "Auth_Public", "Smartcard/Auth_Smartcard", "Guard/Auth_Guard_Shared", "Guard/Auth_Guard_Public"]; diff -r 2489e3c3562b -r 8ae912371831 src/HOL/Auth/Smartcard/Auth_Smartcard.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Auth/Smartcard/Auth_Smartcard.thy Mon Sep 21 15:33:40 2009 +0200 @@ -0,0 +1,13 @@ +(* Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1996 University of Cambridge +*) + +header {* Smartcard protocols: rely on conventional Message and on new EventSC and Smartcard *} + +theory Auth_Smartcard +imports + "ShoupRubin" + "ShoupRubinBella" +begin + +end diff -r 2489e3c3562b -r 8ae912371831 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Mon Sep 21 15:33:40 2009 +0200 +++ b/src/HOL/IsaMakefile Mon Sep 21 15:33:40 2009 +0200 @@ -619,6 +619,10 @@ HOL-Auth: HOL $(LOG)/HOL-Auth.gz $(LOG)/HOL-Auth.gz: $(OUT)/HOL \ + Auth/Auth_Shared.thy Auth/Auth_Public.thy Auth/All_Symmetric.thy \ + Auth/Guard/Auth_Guard_Shared.thy \ + Auth/Guard/Auth_Guard_Public.thy \ + Auth/Smartcard/Auth_Smartcard.thy Auth/All_Symmetric.thy \ Auth/CertifiedEmail.thy Auth/Event.thy Auth/Message.thy \ Auth/NS_Public.thy Auth/NS_Public_Bad.thy Auth/NS_Shared.thy \ Auth/OtwayRees.thy Auth/OtwayReesBella.thy Auth/OtwayRees_AN.thy \