Checked style.
This commit is contained in:
parent
61cdc4efcf
commit
1ab1f96579
|
|
@ -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 \<and> 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 \<and>
|
||||
|
|
@ -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 \<times> (adr\<^sub>i\<^sub>p,msg)history \<times> ((adr\<^sub>i\<^sub>p,msg)packet \<mapsto> unit)
|
||||
\<mapsto> (unit \<times> (adr\<^sub>i\<^sub>p,msg)history \<times> ((adr\<^sub>i\<^sub>p,msg)packet \<mapsto> unit))"
|
||||
where "TRPolicy = ((FTP_STA,FTP_STD) \<Otimes>\<^sub>\<nabla> applyPolicy) o (\<lambda>(x,(y,z)).((x,z),(x,(y,z))))"
|
||||
where "TRPolicy = ((FTP_STA,FTP_STD) \<Otimes>\<^sub>\<nabla> applyPolicy) o (\<lambda>(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 (((\<lambda>(x,y,z). (z,(y,z))) o_f TRPolicy ))"
|
||||
where "TRPolicy\<^sub>M\<^sub>o\<^sub>n' = policy2MON (((\<lambda>(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 \<Rightarrow> adr\<^sub>i\<^sub>p \<Rightarrow> adr\<^sub>i\<^sub>p \<Rightarrow> id \<Rightarrow> port \<Rightarrow>
|
||||
(adr\<^sub>i\<^sub>p,msg) history \<Rightarrow> bool"
|
||||
where
|
||||
"is_ftp H c s i p [] = (H=S3)"
|
||||
|"is_ftp H c s i p (x#InL) = (snd s = 21 \<and>((\<lambda> (id,sr,de,co). (((id = i \<and> (
|
||||
where
|
||||
"is_ftp H c s i p [] = (H=S3)"
|
||||
|"is_ftp H c s i p (x#InL) = (snd s = 21 \<and>((\<lambda> (id,sr,de,co). (((id = i \<and> (
|
||||
(H=ftp_states.S2 \<and> sr = c \<and> de = s \<and> co = ftp_init \<and> is_ftp S3 c s i p InL) \<or>
|
||||
(H=ftp_states.S1 \<and> sr = c \<and> de = s \<and> co = ftp_port_request p \<and> is_ftp S2 c s i p InL) \<or>
|
||||
(H=ftp_states.S1 \<and> sr = s \<and> de = (fst c,p) \<and> co= ftp_data \<and> is_ftp S1 c s i p InL) \<or>
|
||||
|
|
@ -195,7 +195,7 @@ where
|
|||
|
||||
|
||||
definition is_single_ftp_run :: "adr\<^sub>i\<^sub>p src \<Rightarrow> adr\<^sub>i\<^sub>p dest \<Rightarrow> id \<Rightarrow> port \<Rightarrow> (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) \<noteq> (c::int) \<Longrightarrow> \<forall>x\<in>subnet_of (a, b::port). (c, d) \<notin> x"
|
||||
apply (rule ballI)
|
||||
apply (simp add: subnet_of_int_def)
|
||||
done
|
||||
by (rule ballI, simp add: subnet_of_int_def)
|
||||
|
||||
lemma subnetOf_lemma2: " \<forall>x\<in>subnet_of (a::int, b::port). (a, b) \<in> x"
|
||||
apply (rule ballI)
|
||||
apply (simp add: subnet_of_int_def)
|
||||
done
|
||||
by (rule ballI, simp add: subnet_of_int_def)
|
||||
|
||||
lemma subnetOf_lemma3: "(\<exists>x. x \<in> 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: "\<exists>x\<in>subnet_of (a::int, b::port). (a, c::port) \<in> 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: "\<not> (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
|
||||
|
|
@ -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 \<Rightarrow> 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)) \<Oplus> 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 = ((\<lambda>(x,x). Some x) \<circ>\<^sub>m ((FTPVOIP_FTP_STA \<Otimes>\<^sub>S FTPVOIP_VOIP_STA o (\<lambda> (p,x). (p,x,x)))))"
|
||||
where
|
||||
"FTP_VOIP_STA = ((\<lambda>(x,x). Some x) \<circ>\<^sub>m ((FTPVOIP_FTP_STA \<Otimes>\<^sub>S FTPVOIP_VOIP_STA o (\<lambda> (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 = (\<lambda>(x,x). Some x) \<circ>\<^sub>m ((FTPVOIP_FTP_STD \<Otimes>\<^sub>S FTPVOIP_VOIP_STD o (\<lambda> (p,x). (p,x,x))))"
|
||||
where
|
||||
"FTP_VOIP_STD = (\<lambda>(x,x). Some x) \<circ>\<^sub>m ((FTPVOIP_FTP_STD \<Otimes>\<^sub>S FTPVOIP_VOIP_STD o (\<lambda> (p,x). (p,x,x))))"
|
||||
|
||||
definition FTPVOIP_TRPolicy where
|
||||
"FTPVOIP_TRPolicy = policy2MON (
|
||||
|
|
|
|||
|
|
@ -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 \<Rightarrow> 'a" where "POL x = x"
|
|||
text{* Variant 2 takes the policy into the output *}
|
||||
fun FTP_STP ::
|
||||
"((id \<rightharpoonup> 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
|
||||
|
|
@ -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 : "\<guillemotleft>q\<guillemotright> s \<Longrightarrow> \<guillemotleft>q\<guillemotright> (s @ t)"
|
||||
by(cases s,simp_all)
|
||||
by(cases s,simp_all)
|
||||
|
||||
|
||||
fun always :: "('\<alpha> list \<Rightarrow> bool) \<Rightarrow> '\<alpha> list \<Rightarrow> bool" ("\<box>")
|
||||
|
|
@ -74,7 +76,7 @@ text{*
|
|||
locally, this paves the way to a wealth of library lemmas.
|
||||
*}
|
||||
lemma always_is_listall : "(\<box> \<guillemotleft>p\<guillemotright>) (t) = list_all (p) (t)"
|
||||
by(induct t, simp_all)
|
||||
by(induct t, simp_all)
|
||||
|
||||
fun eventually :: "('\<alpha> list \<Rightarrow> bool) \<Rightarrow> '\<alpha> list \<Rightarrow> bool" ("\<diamondsuit>")
|
||||
where
|
||||
|
|
@ -87,7 +89,7 @@ text{*
|
|||
locally, this paves the way to a wealth of library lemmas.
|
||||
*}
|
||||
lemma eventually_is_listex : "(\<diamondsuit> \<guillemotleft>p\<guillemotright>) (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) = ((\<box>\<guillemotleft>p\<guillemotright>) U \<guillemotleft>q\<guillemotright>)"
|
||||
proof -
|
||||
have A:"\<And>a. q a \<Longrightarrow> (\<exists>s t. [a] = s @ t \<and> \<box> \<guillemotleft>p\<guillemotright> s \<and> \<guillemotleft>q\<guillemotright> t)"
|
||||
apply(rule_tac x="[]" in exI)
|
||||
apply(rule_tac x="[a]" in exI, simp)
|
||||
done
|
||||
have B:"\<And>a. (\<exists>s t. [a] = s @ t \<and> \<box> \<guillemotleft>p\<guillemotright> s \<and> \<guillemotleft>q\<guillemotright> t) \<Longrightarrow> 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:"\<And>a aa list.(q a \<or> p a \<and> (\<exists>s t. aa # list = s @ t \<and> \<box> \<guillemotleft>p\<guillemotright> s \<and> \<guillemotleft>q\<guillemotright> t))
|
||||
have A:"\<And>a. q a \<Longrightarrow> (\<exists>s t. [a] = s @ t \<and> \<box> \<guillemotleft>p\<guillemotright> s \<and> \<guillemotleft>q\<guillemotright> t)"
|
||||
apply(rule_tac x="[]" in exI)
|
||||
apply(rule_tac x="[a]" in exI, simp)
|
||||
done
|
||||
have B:"\<And>a. (\<exists>s t. [a] = s @ t \<and> \<box> \<guillemotleft>p\<guillemotright> s \<and> \<guillemotleft>q\<guillemotright> t) \<Longrightarrow> 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:"\<And>a aa list.(q a \<or> p a \<and> (\<exists>s t. aa # list = s @ t \<and> \<box> \<guillemotleft>p\<guillemotright> s \<and> \<guillemotleft>q\<guillemotright> t))
|
||||
\<Longrightarrow> (\<exists>s t. a # aa # list = s @ t \<and> \<box> \<guillemotleft>p\<guillemotright> s \<and> \<guillemotleft>q\<guillemotright> 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:"\<And>a aa list.(\<exists>s t. a # aa # list = s @ t \<and> \<box> \<guillemotleft>p\<guillemotright> s \<and> \<guillemotleft>q\<guillemotright> 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:"\<And>a aa list.(\<exists>s t. a # aa # list = s @ t \<and> \<box> \<guillemotleft>p\<guillemotright> s \<and> \<guillemotleft>q\<guillemotright> t)
|
||||
\<Longrightarrow> (q a \<or> p a \<and> (\<exists>s t. aa # list = s @ t \<and> \<box> \<guillemotleft>p\<guillemotright> s \<and> \<guillemotleft>q\<guillemotright> 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
|
||||
|
|
|
|||
|
|
@ -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 ('\<alpha>,'\<beta>,'\<gamma>) FWState = "'\<alpha> \<times> (('\<beta>,'\<gamma>) packet \<mapsto> unit)"
|
||||
|
||||
|
||||
|
|
@ -74,12 +74,12 @@ type_synonym ('\<alpha>,'\<beta>,'\<gamma>) FWState = "'\<alpha> \<times> (('\<b
|
|||
text{* Having a state, we need of course some state transitions. Such
|
||||
a transition can happen every time a new packet arrives. State
|
||||
transitions can be modelled using a state-exception monad.
|
||||
We provide two types of firewall monads: one *}
|
||||
*}
|
||||
|
||||
|
||||
type_synonym ('\<alpha>,'\<beta>,'\<gamma>) FWStateTransitionP =
|
||||
"('\<beta>,'\<gamma>) packet \<Rightarrow> ((('\<beta>,'\<gamma>) packet \<mapsto> unit) decision, ('\<alpha>,'\<beta>,'\<gamma>) FWState) MON\<^sub>S\<^sub>E"
|
||||
|
||||
|
||||
type_synonym ('\<alpha>,'\<beta>,'\<gamma>) FWStateTransition =
|
||||
"(('\<beta>,'\<gamma>) packet \<times> ('\<alpha>,'\<beta>,'\<gamma>) FWState) \<rightharpoonup> ('\<alpha>,'\<beta>,'\<gamma>) FWState"
|
||||
|
||||
|
|
@ -88,19 +88,19 @@ type_synonym ('\<beta>,'\<gamma>) history = "('\<beta>,'\<gamma>) 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 \<and> ids1 i xs)"
|
||||
|"ids1 i [] = True"
|
||||
|
||||
|
||||
fun ids where
|
||||
"ids a (x#xs) = (NetworkCore.id x \<in> a \<and> ids a xs)"
|
||||
"ids a (x#xs) = (NetworkCore.id x \<in> a \<and> ids a xs)"
|
||||
|"ids a [] = True"
|
||||
|
||||
definition applyPolicy:: "('i \<times> ('i \<mapsto> 'o)) \<mapsto> 'o"
|
||||
where "applyPolicy = (\<lambda> (x,z). z x)"
|
||||
where "applyPolicy = (\<lambda> (x,z). z x)"
|
||||
|
||||
end
|
||||
end
|
||||
|
|
@ -38,7 +38,7 @@
|
|||
subsection {* Stateful Network Protocols *}
|
||||
theory
|
||||
StatefulFW
|
||||
imports
|
||||
FTPVOIP
|
||||
imports
|
||||
FTPVOIP
|
||||
begin
|
||||
end
|
||||
end
|
||||
|
|
@ -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,
|
||||
|
|
|
|||
Loading…
Reference in New Issue