diff --git a/UPF_Firewall/Examples/NAT-FW/NAT-FW.thy b/UPF_Firewall/Examples/NAT-FW/NAT-FW.thy index 7d48110..b915cdc 100644 --- a/UPF_Firewall/Examples/NAT-FW/NAT-FW.thy +++ b/UPF_Firewall/Examples/NAT-FW/NAT-FW.thy @@ -222,4 +222,4 @@ definition policy_10 where lemmas UnfoldPolicy10 = UnfoldPolicy9 nat_10_def Adr110_def Adr210_def policy_10_def -end \ No newline at end of file +end diff --git a/UPF_Firewall/Examples/PersonalFirewall/PersonalFirewallDatatype.thy b/UPF_Firewall/Examples/PersonalFirewall/PersonalFirewallDatatype.thy index 62fd5a2..c78aa87 100644 --- a/UPF_Firewall/Examples/PersonalFirewall/PersonalFirewallDatatype.thy +++ b/UPF_Firewall/Examples/PersonalFirewall/PersonalFirewallDatatype.thy @@ -94,4 +94,4 @@ definition lemmas policyLemmas = strictPolicy_def PortPolicy_def PC_def Internet_def PortPolicyBig_def src_def PolicyCombinators PortCombinators in_subnet_def -end \ No newline at end of file +end diff --git a/UPF_Firewall/Examples/PersonalFirewall/PersonalFirewallInt.thy b/UPF_Firewall/Examples/PersonalFirewall/PersonalFirewallInt.thy index d3de5ae..2db371a 100644 --- a/UPF_Firewall/Examples/PersonalFirewall/PersonalFirewallInt.thy +++ b/UPF_Firewall/Examples/PersonalFirewall/PersonalFirewallInt.thy @@ -95,4 +95,4 @@ declare Ports [simp add] definition wellformed_packet::"(adr\<^sub>i\<^sub>p,DummyContent) packet \ bool" where "wellformed_packet p = (content p = data)" -end \ No newline at end of file +end diff --git a/UPF_Firewall/Examples/Transformation/Transformation.thy b/UPF_Firewall/Examples/Transformation/Transformation.thy index 5c3093e..e75e3a2 100644 --- a/UPF_Firewall/Examples/Transformation/Transformation.thy +++ b/UPF_Firewall/Examples/Transformation/Transformation.thy @@ -43,4 +43,4 @@ theory Transformation02 begin end - \ No newline at end of file + diff --git a/UPF_Firewall/Examples/Transformation/Transformation01.thy b/UPF_Firewall/Examples/Transformation/Transformation01.thy index 2b8cb8c..77ec562 100644 --- a/UPF_Firewall/Examples/Transformation/Transformation01.thy +++ b/UPF_Firewall/Examples/Transformation/Transformation01.thy @@ -192,4 +192,4 @@ lemma all_in_list: "all_in_list (policy2list Policy) (Nets_List Policy)" lemmas normalizeUnfold = normalize_def Policy_def Nets_List_def bothNets_def aux aux2 bothNets_def -end \ No newline at end of file +end diff --git a/UPF_Firewall/Examples/Transformation/Transformation02.thy b/UPF_Firewall/Examples/Transformation/Transformation02.thy index 1517bdc..70c36ce 100644 --- a/UPF_Firewall/Examples/Transformation/Transformation02.thy +++ b/UPF_Firewall/Examples/Transformation/Transformation02.thy @@ -177,4 +177,4 @@ lemma all_in_list: "all_in_list (policy2list Policy) (Nets_List Policy)" lemmas normalizeUnfold = normalize_def PolicyL Nets_List_def bothNets_def aux aux2 bothNets_def sets_distinct1 sets_distinct2 sets_distinct3 sets_distinct4 sets_distinct5 sets_distinct6 aux5 aux2 -end \ No newline at end of file +end diff --git a/UPF_Firewall/FWNormalisation/NormalisationGenericProofs.thy b/UPF_Firewall/FWNormalisation/NormalisationGenericProofs.thy index 1720566..0a9bb28 100644 --- a/UPF_Firewall/FWNormalisation/NormalisationGenericProofs.thy +++ b/UPF_Firewall/FWNormalisation/NormalisationGenericProofs.thy @@ -652,13 +652,13 @@ lemma in_set_in_list[rule_format]: "a \ set p \ all_in_list lemma sorted_Consb[rule_format]: "all_in_list (x#xs) l \ singleCombinators (x#xs) \ - (sorted xs l & (ALL y:set xs. smaller x y l)) \ (sorted (x#xs) l) " + (sorted xs l & (\y\set xs. smaller x y l)) \ (sorted (x#xs) l) " apply(induct xs arbitrary: x) apply (auto simp: order_trans) done lemma sorted_Cons: "\all_in_list (x#xs) l; singleCombinators (x#xs)\ \ - (sorted xs l & (ALL y:set xs. smaller x y l)) = (sorted (x#xs) l)" + (sorted xs l & (\y\set xs. smaller x y l)) = (sorted (x#xs) l)" apply auto apply (rule sorted_Consb, simp_all) apply (metis singleCombinatorsConc singleCombinatorsStart sortedConcEnd) @@ -702,7 +702,7 @@ lemma all_in_list_insort: "\all_in_list xs l; singleCombinators (x#xs); done lemma sorted_ConsA:"\all_in_list (x#xs) l; singleCombinators (x#xs)\ \ - (sorted (x#xs) l) = (sorted xs l & (ALL y:set xs. smaller x y l))" + (sorted (x#xs) l) = (sorted xs l & (\y\set xs. smaller x y l))" by (metis sorted_Cons) lemma is_in_insort: "y \ set xs \ y \ set (insort x xs l)" @@ -2331,4 +2331,4 @@ lemma sets_distinct5: "(n::int) < m \ {(a,b). a = n} \ {( lemma sets_distinct6: "(m::int) < n \ {(a,b). a = n} \ {(a,b). a = m}" by auto end - \ No newline at end of file + diff --git a/UPF_Firewall/FWNormalisation/NormalisationIPPProofs.thy b/UPF_Firewall/FWNormalisation/NormalisationIPPProofs.thy index 4359abc..aface81 100644 --- a/UPF_Firewall/FWNormalisation/NormalisationIPPProofs.thy +++ b/UPF_Firewall/FWNormalisation/NormalisationIPPProofs.thy @@ -563,7 +563,7 @@ lemma nMTSort: "none_MT_rules Cp p \ none_MT_rules Cp (sort p l) lemma nMTSortQ: "none_MT_rules Cp p \ none_MT_rules Cp (qsort p l)" by (metis set_sortQ nMTeqSet) -lemma wp3char[rule_format]: "none_MT_rules Cp xs \ Cp (AllowPortFromTo a b po) = empty \ +lemma wp3char[rule_format]: "none_MT_rules Cp xs \ Cp (AllowPortFromTo a b po) = Map.empty \ wellformed_policy3Pr (xs @ [DenyAllFromTo a b]) \ AllowPortFromTo a b po \ set xs" by (induct xs, simp_all) (metis domNMT wp3Conc) @@ -881,7 +881,7 @@ lemma DARS3[rule_format]:"DenyAll \ set p\DenyAll \ {}" by (simp add: dom_def Cp.simps PolicyCombinators.PolicyCombinators) -lemma DAnMT2: "Cp DenyAll \ empty" +lemma DAnMT2: "Cp DenyAll \ Map.empty" by (metis DAAux dom_eq_empty_conv empty_iff) lemma wp1n_RS3[rule_format,simp]: @@ -1782,13 +1782,13 @@ lemma list2listNMT[rule_format]: "x \ [] \map sem x \\<^sub>2 (list2policy Q)) o d) = - (list2policy ((P \\<^sub>L Q) (op \\<^sub>2) r d))" + (list2policy ((P \\<^sub>L Q) (\\<^sub>2) r d))" by (rule ext, rule Norm_Distr_2) lemma NATDistr: "N \ [] \ F = Cp (list2policyR N) \ ((\ (x,y). x) o_f ((NAT \\<^sub>2 F) o (\ x. (x,x))) = - (list2policy ( ((NAT \\<^sub>L (map Cp N)) (op \\<^sub>2) + (list2policy ( ((NAT \\<^sub>L (map Cp N)) (\\<^sub>2) (\ (x,y). x) (\ x. (x,x))))))" by (simp add: l2polR_eq) (rule ext,rule Norm_Distr_2) @@ -1833,10 +1833,10 @@ lemma normalizePrNAT: allNetsDistinct (policy2list Filter) \ all_in_list (policy2list Filter) (Nets_List Filter) \ ((\ (x,y). x) o_f (((NAT \\<^sub>2 Cp Filter) o (\x. (x,x))))) = - list2policy ((NAT \\<^sub>L (map Cp (rev (normalizePr Filter)))) (op \\<^sub>2) (\ (x,y). x) (\ x. (x,x)))" + list2policy ((NAT \\<^sub>L (map Cp (rev (normalizePr Filter)))) (\\<^sub>2) (\ (x,y). x) (\ x. (x,x)))" by (simp add: C_eq_normalizePr NATDistr list2FWpolicys_eq_sym norm_notMT) lemma domSimpl[simp]: "dom (Cp (A \ DenyAll)) = dom (Cp (DenyAll))" by (simp add: PLemmas) -end \ No newline at end of file +end diff --git a/UPF_Firewall/FWNormalisation/NormalisationIntegerPortProof.thy b/UPF_Firewall/FWNormalisation/NormalisationIntegerPortProof.thy index 868daac..3952f95 100644 --- a/UPF_Firewall/FWNormalisation/NormalisationIntegerPortProof.thy +++ b/UPF_Firewall/FWNormalisation/NormalisationIntegerPortProof.thy @@ -870,7 +870,7 @@ lemma DARS3[rule_format]: lemma DAnMT: "dom (C DenyAll) \ {}" by (simp add: dom_def C.simps PolicyCombinators.PolicyCombinators) -lemma DAnMT2: "C DenyAll \ empty" +lemma DAnMT2: "C DenyAll \ Map.empty" by (metis DAAux dom_eq_empty_conv empty_iff) lemma wp1n_RS3[rule_format,simp]: @@ -1760,13 +1760,13 @@ lemma list2listNMT[rule_format]: "x \ [] \map sem x \\<^sub>2 (list2policy Q)) o d) = (list2policy ((P \\<^sub>L Q) (op \\<^sub>2) r d))" + "r o_f ((P \\<^sub>2 (list2policy Q)) o d) = (list2policy ((P \\<^sub>L Q) (\\<^sub>2) r d))" by (rule ext, rule Norm_Distr_2) lemma NATDistr: "N \ [] \ F = C (list2policyR N) \ (\(x, y). x) o\<^sub>f (NAT \\<^sub>2 F \ (\x. (x, x))) = - list2policy ((NAT \\<^sub>L map C N) op \\<^sub>2 (\(x, y). x) (\x. (x, x)))" + list2policy ((NAT \\<^sub>L map C N) (\\<^sub>2) (\(x, y). x) (\x. (x, x)))" apply (simp add: l2polR_eq) apply (rule ext) apply (rule Norm_Distr_2) @@ -1806,7 +1806,7 @@ lemma normalizeNAT: "DenyAll \ set (policy2list Filter) \ allNetsDistinct (policy2list Filter) \ all_in_list (policy2list Filter) (Nets_List Filter) \ (\(x, y). x) o\<^sub>f (NAT \\<^sub>2 C Filter \ (\x. (x, x))) = - list2policy ((NAT \\<^sub>L map C (rev (FWNormalisationCore.normalize Filter))) op \\<^sub>2 + list2policy ((NAT \\<^sub>L map C (rev (FWNormalisationCore.normalize Filter))) (\\<^sub>2) (\(x, y). x) (\x. (x, x)))" by (simp add: C_eq_normalize NATDistr list2FWpolicys_eq_sym norm_notMT) @@ -1858,4 +1858,4 @@ lemma C_eq_normalizeRotate2: C (list2FWpolicy (FWNormalisationCore.normalize (rotatePolicy p))) = CRotate p" by (simp add: normalize_def, erule C_eq_normalizeRotate,simp_all) -end \ No newline at end of file +end diff --git a/UPF_Firewall/NAT/NAT.thy b/UPF_Firewall/NAT/NAT.thy index c0ec57e..bd06401 100644 --- a/UPF_Firewall/NAT/NAT.thy +++ b/UPF_Firewall/NAT/NAT.thy @@ -166,4 +166,4 @@ lemmas NATLemmas = src2pool_def src2poolPort_def srcNat2pool_IntProtocolPort_def srcNat2pool_IntPort_def srcPat2poolPort_t_def srcPat2poolPort_Protocol_t_def srcPat2pool_IntPort_def srcPat2pool_IntProtocol_def -end \ No newline at end of file +end diff --git a/UPF_Firewall/PacketFilter/PolicyCombinators.thy b/UPF_Firewall/PacketFilter/PolicyCombinators.thy index 3017476..674aeba 100644 --- a/UPF_Firewall/PacketFilter/PolicyCombinators.thy +++ b/UPF_Firewall/PacketFilter/PolicyCombinators.thy @@ -82,4 +82,4 @@ lemmas PolicyCombinators = allow_all_from_def deny_all_from_def allow_all_to_def deny_all_to_def allow_all_from_to_def deny_all_from_to_def UPFDefs -end \ No newline at end of file +end diff --git a/UPF_Firewall/PacketFilter/PortCombinators.thy b/UPF_Firewall/PacketFilter/PortCombinators.thy index 2f900c0..fb71df1 100644 --- a/UPF_Firewall/PacketFilter/PortCombinators.thy +++ b/UPF_Firewall/PacketFilter/PortCombinators.thy @@ -176,4 +176,4 @@ lemmas PortCombinatorsCore = lemmas PortCombinators = PortCombinatorsCore PolicyCombinators -end \ No newline at end of file +end diff --git a/UPF_Firewall/PacketFilter/ProtocolPortCombinators.thy b/UPF_Firewall/PacketFilter/ProtocolPortCombinators.thy index 3af0099..f6eac1e 100644 --- a/UPF_Firewall/PacketFilter/ProtocolPortCombinators.thy +++ b/UPF_Firewall/PacketFilter/ProtocolPortCombinators.thy @@ -173,4 +173,4 @@ lemmas ProtocolCombinatorsCore = lemmas ProtocolCombinators = PortCombinators.PortCombinators ProtocolCombinatorsCore -end \ No newline at end of file +end diff --git a/UPF_Firewall/ROOT b/UPF_Firewall/ROOT index 6416d72..293e622 100644 --- a/UPF_Firewall/ROOT +++ b/UPF_Firewall/ROOT @@ -2,7 +2,7 @@ chapter AFP session "UPF_Firewall" (AFP) = UPF + description {* Formal Network Models and Their Application to Firewall Policies *} - options [timeout=600] + options [timeout = 600] theories "Examples/Examples" document_files diff --git a/UPF_Firewall/StatefulFW/FTP.thy b/UPF_Firewall/StatefulFW/FTP.thy index 881d9eb..88c46b1 100644 --- a/UPF_Firewall/StatefulFW/FTP.thy +++ b/UPF_Firewall/StatefulFW/FTP.thy @@ -235,4 +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 \ No newline at end of file +end diff --git a/UPF_Firewall/StatefulFW/FTP_WithPolicy.thy b/UPF_Firewall/StatefulFW/FTP_WithPolicy.thy index 9fc0f34..6e3bdf8 100644 --- a/UPF_Firewall/StatefulFW/FTP_WithPolicy.thy +++ b/UPF_Firewall/StatefulFW/FTP_WithPolicy.thy @@ -72,4 +72,4 @@ fun FTP_STP :: |"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 \ No newline at end of file +end