diff --git a/StatefulFW/FTP.thy b/StatefulFW/FTP.thy index c7005bc..83c19dc 100644 --- a/StatefulFW/FTP.thy +++ b/StatefulFW/FTP.thy @@ -38,8 +38,8 @@ subsection {* The File Transfer Prototol (ftp) *} theory FTP -imports - Stateful + imports + StatefulCore begin subsubsection{* The protocol syntax *} @@ -102,7 +102,7 @@ definition fun are_ftp_other where "are_ftp_other i (x#xs) = (is_ftp_other i x \ are_ftp_other i xs)" - |"are_ftp_other i [] = True" + |"are_ftp_other i [] = True" subsubsection{* The protocol policy specification *} text{* @@ -124,7 +124,7 @@ fun last_opened_port where | "last_opened_port x [] = undefined" fun FTP_STA :: "((adr\<^sub>i\<^sub>p,msg) history, adr\<^sub>i\<^sub>p, msg) FWStateTransition" -where + where (* FTP_PORT_REQUEST *) "FTP_STA ((i,s,d,ftp_port_request pr), (log, pol)) = (if before(Not o is_ftp_close i)(is_init i) log \ @@ -144,18 +144,18 @@ where fun FTP_STD :: "((adr\<^sub>i\<^sub>p,msg) history, adr\<^sub>i\<^sub>p, msg) FWStateTransition" -where "FTP_STD (p,s) = Some s" + where "FTP_STD (p,s) = Some s" definition TRPolicy ::" (adr\<^sub>i\<^sub>p,msg)packet \ (adr\<^sub>i\<^sub>p,msg)history \ ((adr\<^sub>i\<^sub>p,msg)packet \ unit) \ (unit \ (adr\<^sub>i\<^sub>p,msg)history \ ((adr\<^sub>i\<^sub>p,msg)packet \ unit))" -where "TRPolicy = ((FTP_STA,FTP_STD) \\<^sub>\ applyPolicy) o (\(x,(y,z)).((x,z),(x,(y,z))))" + where "TRPolicy = ((FTP_STA,FTP_STD) \\<^sub>\ applyPolicy) o (\(x,(y,z)).((x,z),(x,(y,z))))" definition TRPolicy\<^sub>M\<^sub>o\<^sub>n -where "TRPolicy\<^sub>M\<^sub>o\<^sub>n = policy2MON(TRPolicy)" + where "TRPolicy\<^sub>M\<^sub>o\<^sub>n = policy2MON(TRPolicy)" text{* If required to contain the policy in the output *} definition TRPolicy\<^sub>M\<^sub>o\<^sub>n' -where "TRPolicy\<^sub>M\<^sub>o\<^sub>n' = policy2MON (((\(x,y,z). (z,(y,z))) o_f TRPolicy ))" + where "TRPolicy\<^sub>M\<^sub>o\<^sub>n' = policy2MON (((\(x,y,z). (z,(y,z))) o_f TRPolicy ))" text{* Now we specify our test scenario in more detail. We could test: @@ -184,9 +184,9 @@ text{* fun is_ftp :: "ftp_states \ adr\<^sub>i\<^sub>p \ adr\<^sub>i\<^sub>p \ id \ port \ (adr\<^sub>i\<^sub>p,msg) history \ bool" -where - "is_ftp H c s i p [] = (H=S3)" -|"is_ftp H c s i p (x#InL) = (snd s = 21 \((\ (id,sr,de,co). (((id = i \ ( + where + "is_ftp H c s i p [] = (H=S3)" + |"is_ftp H c s i p (x#InL) = (snd s = 21 \((\ (id,sr,de,co). (((id = i \ ( (H=ftp_states.S2 \ sr = c \ de = s \ co = ftp_init \ is_ftp S3 c s i p InL) \ (H=ftp_states.S1 \ sr = c \ de = s \ co = ftp_port_request p \ is_ftp S2 c s i p InL) \ (H=ftp_states.S1 \ sr = s \ de = (fst c,p) \ co= ftp_data \ is_ftp S1 c s i p InL) \ @@ -195,7 +195,7 @@ where definition is_single_ftp_run :: "adr\<^sub>i\<^sub>p src \ adr\<^sub>i\<^sub>p dest \ id \ port \ (adr\<^sub>i\<^sub>p,msg) history set" -where "is_single_ftp_run s d i p = {x. (is_ftp S0 s d i p x)}" + where "is_single_ftp_run s d i p = {x. (is_ftp S0 s d i p x)}" text{* The following constant then returns a set of all the historys which denote such a normal @@ -213,28 +213,19 @@ definition (is_ftp S0 s2 d2 i2 p2 (packet_with_id x i2))}" lemma subnetOf_lemma: "(a::int) \ (c::int) \ \x\subnet_of (a, b::port). (c, d) \ x" -apply (rule ballI) -apply (simp add: subnet_of_int_def) -done + by (rule ballI, simp add: subnet_of_int_def) lemma subnetOf_lemma2: " \x\subnet_of (a::int, b::port). (a, b) \ x" -apply (rule ballI) -apply (simp add: subnet_of_int_def) -done + by (rule ballI, simp add: subnet_of_int_def) lemma subnetOf_lemma3: "(\x. x \ subnet_of (a::int, b::port))" -apply (rule exI) -apply (simp add: subnet_of_int_def) -done + by (rule exI, simp add: subnet_of_int_def) lemma subnetOf_lemma4: "\x\subnet_of (a::int, b::port). (a, c::port) \ x" -apply (rule bexI) -apply (simp_all add: subnet_of_int_def) -done + by (rule bexI, simp_all add: subnet_of_int_def) lemma port_open_lemma: "\ (Ex (port_open [] (x::port)))" -apply (simp add: port_open_def) -done + by (simp add: port_open_def) lemmas FTPLemmas = TRPolicy_def applyPolicy_def policy2MON_def Let_def in_subnet_def src_def @@ -244,5 +235,4 @@ lemmas FTPLemmas = TRPolicy_def applyPolicy_def policy2MON_def exI subnetOf_lemma subnetOf_lemma2 subnetOf_lemma3 subnetOf_lemma4 NetworkCore.id_def adr\<^sub>i\<^sub>pLemmas port_open_lemma bind_SE_def unit_SE_def valid_SE_def -end - +end \ No newline at end of file diff --git a/StatefulFW/FTPVOIP.thy b/StatefulFW/FTPVOIP.thy index bcd3ded..c60f489 100644 --- a/StatefulFW/FTPVOIP.thy +++ b/StatefulFW/FTPVOIP.thy @@ -38,8 +38,8 @@ subsection {* FTP and VoIP Protocol *} theory FTPVOIP -imports - FTP_WithPolicy VOIP + imports + FTP_WithPolicy VOIP begin datatype ftpvoip = ARQ @@ -166,7 +166,7 @@ definition FTPVOIP_subnet_of_adr :: "int \ adr\<^sub>i\<^sub>p net" fun FTPVOIP_VOIP_STA :: "((adr\<^sub>i\<^sub>p, ftpvoip) history, adr\<^sub>i\<^sub>p, ftpvoip) FWStateTransition" -where + where "FTPVOIP_VOIP_STA ((a,c,d,ARQ), (InL, policy)) = Some (((a,c,d, ARQ)#InL, (allow_from_to_port (1719::port)(subnet_of d) (subnet_of c)) \ policy))" @@ -219,17 +219,17 @@ where fun FTPVOIP_VOIP_STD :: "((adr\<^sub>i\<^sub>p, ftpvoip) history, adr\<^sub>i\<^sub>p, ftpvoip) FWStateTransition" -where - "FTPVOIP_VOIP_STD (p,s) = Some s" + where + "FTPVOIP_VOIP_STD (p,s) = Some s" definition FTP_VOIP_STA :: "((adr\<^sub>i\<^sub>p, ftpvoip) history, adr\<^sub>i\<^sub>p, ftpvoip) FWStateTransition" -where - "FTP_VOIP_STA = ((\(x,x). Some x) \\<^sub>m ((FTPVOIP_FTP_STA \\<^sub>S FTPVOIP_VOIP_STA o (\ (p,x). (p,x,x)))))" + where + "FTP_VOIP_STA = ((\(x,x). Some x) \\<^sub>m ((FTPVOIP_FTP_STA \\<^sub>S FTPVOIP_VOIP_STA o (\ (p,x). (p,x,x)))))" definition FTP_VOIP_STD :: "((adr\<^sub>i\<^sub>p, ftpvoip) history, adr\<^sub>i\<^sub>p, ftpvoip) FWStateTransition" -where - "FTP_VOIP_STD = (\(x,x). Some x) \\<^sub>m ((FTPVOIP_FTP_STD \\<^sub>S FTPVOIP_VOIP_STD o (\ (p,x). (p,x,x))))" + where + "FTP_VOIP_STD = (\(x,x). Some x) \\<^sub>m ((FTPVOIP_FTP_STD \\<^sub>S FTPVOIP_VOIP_STD o (\ (p,x). (p,x,x))))" definition FTPVOIP_TRPolicy where "FTPVOIP_TRPolicy = policy2MON ( diff --git a/StatefulFW/FTP_WithPolicy.thy b/StatefulFW/FTP_WithPolicy.thy index c828a57..9fc0f34 100644 --- a/StatefulFW/FTP_WithPolicy.thy +++ b/StatefulFW/FTP_WithPolicy.thy @@ -38,8 +38,8 @@ subsection {* FTP enriched with a security policy *} theory FTP_WithPolicy -imports - FTP + imports + FTP begin text{* FTP where the policy is part of the output. *} @@ -49,7 +49,7 @@ definition POL :: "'a \ 'a" where "POL x = x" text{* Variant 2 takes the policy into the output *} fun FTP_STP :: "((id \ port), adr\<^sub>i\<^sub>p, msg) FWStateTransitionP" -where + where (* FTP_PORT_REQUEST *) "FTP_STP (i,s,d,ftp_port_request pr) (ports, policy) = (if p_accept (i,s,d,ftp_port_request pr) policy then @@ -72,6 +72,4 @@ where |"FTP_STP p x = (if p_accept p (snd x) then Some (allow (POL (snd x)),((fst x),snd x)) else Some (deny (POL (snd x)),(fst x,snd x)))" -end - - +end \ No newline at end of file diff --git a/StatefulFW/LTL_alike.thy b/StatefulFW/LTL_alike.thy index 681ca87..20afe85 100644 --- a/StatefulFW/LTL_alike.thy +++ b/StatefulFW/LTL_alike.thy @@ -36,8 +36,10 @@ *****************************************************************************) subsection {* Termporal Combinators *} -theory LTL_alike -imports Main +theory + LTL_alike + imports + Main begin text{* @@ -61,7 +63,7 @@ where | "atom p (a # S) = (p a)" lemma holds_mono : "\q\ s \ \q\ (s @ t)" -by(cases s,simp_all) + by(cases s,simp_all) fun always :: "('\ list \ bool) \ '\ list \ bool" ("\") @@ -74,7 +76,7 @@ text{* locally, this paves the way to a wealth of library lemmas. *} lemma always_is_listall : "(\ \p\) (t) = list_all (p) (t)" -by(induct t, simp_all) + by(induct t, simp_all) fun eventually :: "('\ list \ bool) \ '\ list \ bool" ("\") where @@ -87,7 +89,7 @@ text{* locally, this paves the way to a wealth of library lemmas. *} lemma eventually_is_listex : "(\ \p\) (t) = list_ex (p) (t)" -by(induct t, simp_all) + by(induct t, simp_all) text{* The next two constants will help us later in defining the state transitions. The constant @@ -126,35 +128,35 @@ text{* This leads to this amazingly tricky proof:*} lemma before_vs_until: "(before p q) = ((\\p\) U \q\)" proof - - have A:"\a. q a \ (\s t. [a] = s @ t \ \ \p\ s \ \q\ t)" - apply(rule_tac x="[]" in exI) - apply(rule_tac x="[a]" in exI, simp) - done - have B:"\a. (\s t. [a] = s @ t \ \ \p\ s \ \q\ t) \ q a" - apply auto - apply(case_tac "t=[]", auto simp:List.neq_Nil_conv) - apply(case_tac "s=[]", auto simp:List.neq_Nil_conv) - done - have C:"\a aa list.(q a \ p a \ (\s t. aa # list = s @ t \ \ \p\ s \ \q\ t)) + have A:"\a. q a \ (\s t. [a] = s @ t \ \ \p\ s \ \q\ t)" + apply(rule_tac x="[]" in exI) + apply(rule_tac x="[a]" in exI, simp) + done + have B:"\a. (\s t. [a] = s @ t \ \ \p\ s \ \q\ t) \ q a" + apply auto + apply(case_tac "t=[]", auto simp:List.neq_Nil_conv) + apply(case_tac "s=[]", auto simp:List.neq_Nil_conv) + done + have C:"\a aa list.(q a \ p a \ (\s t. aa # list = s @ t \ \ \p\ s \ \q\ t)) \ (\s t. a # aa # list = s @ t \ \ \p\ s \ \q\ t)" - apply auto - apply(rule_tac x="[]" in exI) - apply(rule_tac x="a # aa # list" in exI, simp) - apply(rule_tac x="a # s" in exI) - apply(rule_tac x="t" in exI,simp) - done - have D:"\a aa list.(\s t. a # aa # list = s @ t \ \ \p\ s \ \q\ t) + apply auto + apply(rule_tac x="[]" in exI) + apply(rule_tac x="a # aa # list" in exI, simp) + apply(rule_tac x="a # s" in exI) + apply(rule_tac x="t" in exI,simp) + done + have D:"\a aa list.(\s t. a # aa # list = s @ t \ \ \p\ s \ \q\ t) \ (q a \ p a \ (\s t. aa # list = s @ t \ \ \p\ s \ \q\ t))" - apply auto - apply(case_tac "s", auto simp:List.neq_Nil_conv) - apply(case_tac "s", auto simp:List.neq_Nil_conv) - done - show ?thesis - apply(rule ext,induct_tac "x", simp, - case_tac "list",simp_all) - apply(rule iffI,erule A, erule B) - apply(rule iffI,erule C, erule D) - done + apply auto + apply(case_tac "s", auto simp:List.neq_Nil_conv) + apply(case_tac "s", auto simp:List.neq_Nil_conv) + done + show ?thesis + apply(rule ext,induct_tac "x", simp, + case_tac "list",simp_all) + apply(rule iffI,erule A, erule B) + apply(rule iffI,erule C, erule D) + done qed end diff --git a/StatefulFW/Stateful.thy b/StatefulFW/StatefulCore.thy similarity index 94% rename from StatefulFW/Stateful.thy rename to StatefulFW/StatefulCore.thy index 86a2b40..b92a676 100644 --- a/StatefulFW/Stateful.thy +++ b/StatefulFW/StatefulCore.thy @@ -37,10 +37,10 @@ section {* Stateful Protocols *} theory - Stateful -imports - "../PacketFilter/PacketFilter" - LTL_alike + StatefulCore + imports + "../PacketFilter/PacketFilter" + LTL_alike begin text{* @@ -66,7 +66,7 @@ text{* At first we hence need a state. It is a tuple from some memory to be refined later and the current policy. *} - + type_synonym ('\,'\,'\) FWState = "'\ \ (('\,'\) packet \ unit)" @@ -74,12 +74,12 @@ type_synonym ('\,'\,'\) FWState = "'\ \ (('\,'\,'\) FWStateTransitionP = "('\,'\) packet \ ((('\,'\) packet \ unit) decision, ('\,'\,'\) FWState) MON\<^sub>S\<^sub>E" - + type_synonym ('\,'\,'\) FWStateTransition = "(('\,'\) packet \ ('\,'\,'\) FWState) \ ('\,'\,'\) FWState" @@ -88,19 +88,19 @@ type_synonym ('\,'\) history = "('\,'\) packet list" fun packet_with_id where - "packet_with_id [] i = []" + "packet_with_id [] i = []" |"packet_with_id (x#xs) i = (if id x = i then (x#(packet_with_id xs i)) else (packet_with_id xs i))" fun ids1 where "ids1 i (x#xs) = (id x = i \ ids1 i xs)" |"ids1 i [] = True" - + fun ids where - "ids a (x#xs) = (NetworkCore.id x \ a \ ids a xs)" + "ids a (x#xs) = (NetworkCore.id x \ a \ ids a xs)" |"ids a [] = True" definition applyPolicy:: "('i \ ('i \ 'o)) \ 'o" -where "applyPolicy = (\ (x,z). z x)" + where "applyPolicy = (\ (x,z). z x)" -end +end \ No newline at end of file diff --git a/StatefulFW/StatefulFW.thy b/StatefulFW/StatefulFW.thy index 42235cf..9aaf7e4 100644 --- a/StatefulFW/StatefulFW.thy +++ b/StatefulFW/StatefulFW.thy @@ -38,7 +38,7 @@ subsection {* Stateful Network Protocols *} theory StatefulFW -imports - FTPVOIP + imports + FTPVOIP begin -end +end \ No newline at end of file diff --git a/StatefulFW/VOIP.thy b/StatefulFW/VOIP.thy index 5f523a5..f11eddb 100644 --- a/StatefulFW/VOIP.thy +++ b/StatefulFW/VOIP.thy @@ -37,7 +37,7 @@ subsection {* A simple voice-over-ip model *} theory VOIP -imports Stateful + imports StatefulCore begin text{* @@ -59,13 +59,6 @@ text{* \item Calls can be initiated from outside the firewall. \end{itemize} -% \begin{figure} -% \centering -% \includegraphics[scale=0.4]{voip} -% \caption {The modelled VoIP-Protocol} -% \label{voip} -% \end{figure} - Again we only consider a simplified VoIP scenario with the following seven messages which are grouped into four subprotocols (see Figure \ref{voip}): @@ -273,8 +266,6 @@ text{* *} datatype voip_states = S0 | S1 | S2 | S3 | S4 | S5 - - text{* The constant @{text "is_voip"} checks if a trace corresponds to a legal VoIP protocol, given the IP-addresses of the three entities,