From ea91410aec9355707e85a488f8c2b4eb559ee6d8 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Sat, 22 Jun 2019 23:31:30 +0100 Subject: [PATCH] Import of official AFP entry for Isabelle 2019. --- .ci/Jenkinsfile | 2 +- UPF_Firewall/Examples/DMZ/DMZ.thy | 2 +- UPF_Firewall/Examples/DMZ/DMZDatatype.thy | 10 +- UPF_Firewall/Examples/DMZ/DMZInteger.thy | 10 +- UPF_Firewall/Examples/Examples.thy | 4 +- UPF_Firewall/Examples/NAT-FW/NAT-FW.thy | 2 +- .../PersonalFirewall/PersonalFirewall.thy | 2 +- .../PersonalFirewallDatatype.thy | 10 +- .../PersonalFirewall/PersonalFirewallInt.thy | 14 +-- .../PersonalFirewall/PersonalFirewallIpv4.thy | 14 +-- .../Transformation/Transformation.thy | 2 +- .../Transformation/Transformation01.thy | 2 +- .../Transformation/Transformation02.thy | 2 +- .../Voice_over_IP.thy} | 24 ++-- .../FWNormalisation/ElementaryRules.thy | 6 +- .../FWNormalisation/FWNormalisation.thy | 2 +- .../FWNormalisation/FWNormalisationCore.thy | 104 +++++++++--------- .../NormalisationGenericProofs.thy | 30 ++--- .../NormalisationIPPProofs.thy | 16 +-- .../NormalisationIntegerPortProof.thy | 18 +-- UPF_Firewall/NAT/NAT.thy | 6 +- UPF_Firewall/PacketFilter/DatatypeAddress.thy | 6 +- UPF_Firewall/PacketFilter/DatatypePort.thy | 6 +- UPF_Firewall/PacketFilter/IPv4.thy | 6 +- UPF_Firewall/PacketFilter/IPv4_TCPUDP.thy | 2 +- UPF_Firewall/PacketFilter/IntegerAddress.thy | 4 +- UPF_Firewall/PacketFilter/IntegerPort.thy | 6 +- .../PacketFilter/IntegerPort_TCPUDP.thy | 8 +- UPF_Firewall/PacketFilter/NetworkCore.thy | 48 ++++---- UPF_Firewall/PacketFilter/NetworkModels.thy | 6 +- UPF_Firewall/PacketFilter/PacketFilter.thy | 2 +- .../PacketFilter/PolicyCombinators.thy | 12 +- UPF_Firewall/PacketFilter/PolicyCore.thy | 20 ++-- UPF_Firewall/PacketFilter/PortCombinators.thy | 10 +- UPF_Firewall/PacketFilter/Ports.thy | 10 +- .../PacketFilter/ProtocolPortCombinators.thy | 8 +- UPF_Firewall/ROOT | 2 +- UPF_Firewall/StatefulFW/FTP.thy | 46 ++++---- UPF_Firewall/StatefulFW/FTPVOIP.thy | 28 ++--- UPF_Firewall/StatefulFW/FTP_WithPolicy.thy | 6 +- UPF_Firewall/StatefulFW/LTL_alike.thy | 38 +++---- UPF_Firewall/StatefulFW/StatefulCore.thy | 12 +- UPF_Firewall/StatefulFW/StatefulFW.thy | 2 +- UPF_Firewall/StatefulFW/VOIP.thy | 50 ++++----- UPF_Firewall/UPF-Firewall.thy | 6 +- UPF_Firewall/document/root.bib | 2 +- UPF_Firewall/document/root.tex | 2 +- 47 files changed, 315 insertions(+), 315 deletions(-) rename UPF_Firewall/Examples/{VoIP/VoIP.thy => Voice_over_IP/Voice_over_IP.thy} (96%) diff --git a/.ci/Jenkinsfile b/.ci/Jenkinsfile index c419550..45b2528 100644 --- a/.ci/Jenkinsfile +++ b/.ci/Jenkinsfile @@ -3,7 +3,7 @@ pipeline { stages { stage('Build') { steps { - sh 'docker run -v $PWD/UPF_Firewall:/UPF_Firewall logicalhacking:isabelle2018 isabelle build -D /UPF_Firewall' + sh 'docker run -v $PWD/UPF_Firewall:/UPF_Firewall logicalhacking:isabelle2019 isabelle build -D /UPF_Firewall' } } } diff --git a/UPF_Firewall/Examples/DMZ/DMZ.thy b/UPF_Firewall/Examples/DMZ/DMZ.thy index d804cee..4bb1531 100644 --- a/UPF_Firewall/Examples/DMZ/DMZ.thy +++ b/UPF_Firewall/Examples/DMZ/DMZ.thy @@ -35,7 +35,7 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *****************************************************************************) -section {* A Simple DMZ Setup *} +section \A Simple DMZ Setup\ theory DMZ imports diff --git a/UPF_Firewall/Examples/DMZ/DMZDatatype.thy b/UPF_Firewall/Examples/DMZ/DMZDatatype.thy index 26a5e14..77caa8d 100644 --- a/UPF_Firewall/Examples/DMZ/DMZDatatype.thy +++ b/UPF_Firewall/Examples/DMZ/DMZDatatype.thy @@ -35,14 +35,14 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *****************************************************************************) -subsection {* DMZ Datatype *} +subsection \DMZ Datatype\ theory DMZDatatype imports "../../UPF-Firewall" begin -text{* +text\ This is the fourth scenario, slightly more complicated than the previous one, as we now also model specific servers within one network. Therefore, we could not use anymore the modelling using datatype synonym, but only use the one where an address is modelled as an @@ -51,7 +51,7 @@ text{* Just for comparison, this theory is the same scenario with datatype synonym anyway, but with four distinct networks instead of one contained in another. As there is no corresponding network model included, we need to define a custom one. -*} +\ datatype Adr = Intranet | Internet | Mail | Web | DMZ instance Adr::adr .. @@ -98,10 +98,10 @@ definition Internet_mail_port ++ Internet_web_port" -text {* +text \ We only want to create test cases which are sent between the three main networks: e.g. not between the mailserver and the dmz. Therefore, the constraint looks as follows. \ -*} +\ definition not_in_same_net :: "(Networks,DummyContent) packet \ bool" where diff --git a/UPF_Firewall/Examples/DMZ/DMZInteger.thy b/UPF_Firewall/Examples/DMZ/DMZInteger.thy index b78e1a3..eb99d4e 100644 --- a/UPF_Firewall/Examples/DMZ/DMZInteger.thy +++ b/UPF_Firewall/Examples/DMZ/DMZInteger.thy @@ -35,14 +35,14 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *****************************************************************************) -subsection {* DMZ: Integer *} +subsection \DMZ: Integer\ theory DMZInteger imports "../../UPF-Firewall" begin -text{* This scenario is slightly more complicated than the SimpleDMZ +text\This scenario is slightly more complicated than the SimpleDMZ one, as we now also model specific servers within one network. Therefore, we cannot use anymore the modelling using datatype synonym, but only use the one where an address is modelled as an @@ -69,7 +69,7 @@ The scenario is the following: \end{itemize} \end{labeling} -*} +\ definition intranet::"adr\<^sub>i\<^sub>p net" where @@ -111,10 +111,10 @@ definition Internet_mail_port ++ Internet_web_port" -text {* +text \ We only want to create test cases which are sent between the three main networks: e.g. not between the mailserver and the dmz. Therefore, the constraint looks as follows. -*} +\ definition not_in_same_net :: "(adr\<^sub>i\<^sub>p,DummyContent) packet \ bool" where diff --git a/UPF_Firewall/Examples/Examples.thy b/UPF_Firewall/Examples/Examples.thy index 68d0893..b050a60 100644 --- a/UPF_Firewall/Examples/Examples.thy +++ b/UPF_Firewall/Examples/Examples.thy @@ -35,12 +35,12 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *****************************************************************************) -chapter {* Examples *} +chapter \Examples\ theory Examples imports "DMZ/DMZ" - "VoIP/VoIP" + "Voice_over_IP/Voice_over_IP" "Transformation/Transformation" "NAT-FW/NAT-FW" "PersonalFirewall/PersonalFirewall" diff --git a/UPF_Firewall/Examples/NAT-FW/NAT-FW.thy b/UPF_Firewall/Examples/NAT-FW/NAT-FW.thy index b915cdc..4d4f4fe 100644 --- a/UPF_Firewall/Examples/NAT-FW/NAT-FW.thy +++ b/UPF_Firewall/Examples/NAT-FW/NAT-FW.thy @@ -35,7 +35,7 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *****************************************************************************) -section {* Example: NAT *} +section \Example: NAT\ theory "NAT-FW" imports diff --git a/UPF_Firewall/Examples/PersonalFirewall/PersonalFirewall.thy b/UPF_Firewall/Examples/PersonalFirewall/PersonalFirewall.thy index b4b5db6..d4bb605 100644 --- a/UPF_Firewall/Examples/PersonalFirewall/PersonalFirewall.thy +++ b/UPF_Firewall/Examples/PersonalFirewall/PersonalFirewall.thy @@ -35,7 +35,7 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *****************************************************************************) -section {* Personal Firewall *} +section \Personal Firewall\ theory PersonalFirewall imports diff --git a/UPF_Firewall/Examples/PersonalFirewall/PersonalFirewallDatatype.thy b/UPF_Firewall/Examples/PersonalFirewall/PersonalFirewallDatatype.thy index c78aa87..62db928 100644 --- a/UPF_Firewall/Examples/PersonalFirewall/PersonalFirewallDatatype.thy +++ b/UPF_Firewall/Examples/PersonalFirewall/PersonalFirewallDatatype.thy @@ -35,20 +35,20 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *****************************************************************************) -subsection {* Personal Firewall: Datatype *} +subsection \Personal Firewall: Datatype\ theory PersonalFirewallDatatype imports "../../UPF-Firewall" begin -text{* +text\ The most basic firewall scenario; there is a personal PC on one side and the Internet on the other. There are two policies: the first one allows all traffic from the PC to the Internet and denies all coming into the PC. The second policy only allows specific ports from the PC. This scenario comes in three variants: the first one specifies the allowed protocols directly, the second together with their respective port numbers, the third one only with the port numbers. -*} +\ datatype Adr = pc | internet @@ -68,12 +68,12 @@ definition not_in_same_net :: "(DatatypeTwoNets,DummyContent) packet \ bool" where "not_in_same_net x = ((src x \ PC \ dest x \ Internet) \ (src x \ Internet \ dest x \ PC))" -text {* +text \ Definitions of the policies In fact, the short definitions wouldn't have to be written down - they are the automatically simplified versions of their big counterparts. -*} +\ definition strictPolicy :: "(DatatypeTwoNets,DummyContent) FWPolicy" where diff --git a/UPF_Firewall/Examples/PersonalFirewall/PersonalFirewallInt.thy b/UPF_Firewall/Examples/PersonalFirewall/PersonalFirewallInt.thy index 2db371a..a612960 100644 --- a/UPF_Firewall/Examples/PersonalFirewall/PersonalFirewallInt.thy +++ b/UPF_Firewall/Examples/PersonalFirewall/PersonalFirewallInt.thy @@ -35,24 +35,24 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *****************************************************************************) -subsection{* Personal Firewall: Integer *} +subsection\Personal Firewall: Integer\ theory PersonalFirewallInt imports "../../UPF-Firewall" begin -text{* +text\ The most basic firewall scenario; there is a personal PC on one side and the Internet on the other. There are two policies: the first one allows all traffic from the PC to the Internet and denies all coming into the PC. The second policy only allows specific ports from the PC. This scenario comes in three variants: the first one specifies the allowed protocols directly, the second together with their respective port numbers, the third one only with the port numbers. -*} +\ -text{* +text\ Definitions of the subnets -*} +\ definition PC :: "(adr\<^sub>i\<^sub>p net)" where @@ -66,9 +66,9 @@ definition not_in_same_net :: "(adr\<^sub>i\<^sub>p,DummyContent) packet \ bool" where "not_in_same_net x = ((src x \ PC \ dest x \ Internet) \ (src x \ Internet \ dest x \ PC))" -text {* +text \ Definitions of the policies -*} +\ definition strictPolicy :: "(adr\<^sub>i\<^sub>p,DummyContent) FWPolicy" where diff --git a/UPF_Firewall/Examples/PersonalFirewall/PersonalFirewallIpv4.thy b/UPF_Firewall/Examples/PersonalFirewall/PersonalFirewallIpv4.thy index f1f5c0d..db4c57a 100644 --- a/UPF_Firewall/Examples/PersonalFirewall/PersonalFirewallIpv4.thy +++ b/UPF_Firewall/Examples/PersonalFirewall/PersonalFirewallIpv4.thy @@ -35,24 +35,24 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *****************************************************************************) -subsection {* Personal Firewall IPv4 *} +subsection \Personal Firewall IPv4\ theory PersonalFirewallIpv4 imports "../../UPF-Firewall" begin -text{* +text\ The most basic firewall scenario; there is a personal PC on one side and the Internet on the other. There are two policies: the first one allows all traffic from the PC to the Internet and denies all coming into the PC. The second policy only allows specific ports from the PC. This scenario comes in three variants: the first one specifies the allowed protocols directly, the second together with their respective port numbers, the third one only with the port numbers. -*} +\ -text{* +text\ Definitions of the subnets -*} +\ definition PC :: "(ipv4 net)" where @@ -66,9 +66,9 @@ definition not_in_same_net :: "(ipv4,DummyContent) packet \ bool" where "not_in_same_net x = ((src x \ PC \ dest x \ Internet) \ (src x \ Internet \ dest x \ PC))" -text {* +text \ Definitions of the policies -*} +\ definition strictPolicy :: "(ipv4,DummyContent) FWPolicy" where "strictPolicy = deny_all ++ allow_all_from_to PC Internet" diff --git a/UPF_Firewall/Examples/Transformation/Transformation.thy b/UPF_Firewall/Examples/Transformation/Transformation.thy index e75e3a2..dd33361 100644 --- a/UPF_Firewall/Examples/Transformation/Transformation.thy +++ b/UPF_Firewall/Examples/Transformation/Transformation.thy @@ -35,7 +35,7 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *****************************************************************************) -section {* Demonstrating Policy Transformations *} +section \Demonstrating Policy Transformations\ theory Transformation imports diff --git a/UPF_Firewall/Examples/Transformation/Transformation01.thy b/UPF_Firewall/Examples/Transformation/Transformation01.thy index 77ec562..d1d946d 100644 --- a/UPF_Firewall/Examples/Transformation/Transformation01.thy +++ b/UPF_Firewall/Examples/Transformation/Transformation01.thy @@ -35,7 +35,7 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *****************************************************************************) -subsection {* Transformation Example 1 *} +subsection \Transformation Example 1\ theory Transformation01 imports diff --git a/UPF_Firewall/Examples/Transformation/Transformation02.thy b/UPF_Firewall/Examples/Transformation/Transformation02.thy index 70c36ce..4be9cf6 100644 --- a/UPF_Firewall/Examples/Transformation/Transformation02.thy +++ b/UPF_Firewall/Examples/Transformation/Transformation02.thy @@ -35,7 +35,7 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *****************************************************************************) -subsection {* Transforamtion Example 2 *} +subsection \Transforamtion Example 2\ theory Transformation02 imports diff --git a/UPF_Firewall/Examples/VoIP/VoIP.thy b/UPF_Firewall/Examples/Voice_over_IP/Voice_over_IP.thy similarity index 96% rename from UPF_Firewall/Examples/VoIP/VoIP.thy rename to UPF_Firewall/Examples/Voice_over_IP/Voice_over_IP.thy index 907ab3c..ac75889 100644 --- a/UPF_Firewall/Examples/VoIP/VoIP.thy +++ b/UPF_Firewall/Examples/Voice_over_IP/Voice_over_IP.thy @@ -35,20 +35,20 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *****************************************************************************) -section {* Voice over IP *} +section \Voice over IP\ theory - VoIP + Voice_over_IP imports "../../UPF-Firewall" begin -text{* +text\ In this theory we generate the test data for correct runs of the FTP protocol. As usual, we start with definining the networks and the policy. We use a rather simple policy which allows only FTP connections starting from the Intranet and going to the Internet, and deny everything else. -*} +\ definition intranet :: "adr\<^sub>i\<^sub>p net" where @@ -66,9 +66,9 @@ definition voip_policy :: "(adr\<^sub>i\<^sub>p,address voip_msg) FWPolicy" where "voip_policy = A\<^sub>U" -text{* +text\ The next two constants check if an address is in the Intranet or in the Internet respectively. -*} +\ definition is_in_intranet :: "address \ bool" where @@ -82,9 +82,9 @@ definition is_in_internet :: "address \ bool" where "is_in_internet a = (a > 4)" -text{* +text\ The next definition is our starting state: an empty trace and the just defined policy. -*} +\ definition "\_0_voip" :: "(adr\<^sub>i\<^sub>p, address voip_msg) history \ @@ -92,10 +92,10 @@ definition where "\_0_voip = ([],voip_policy)" -text{* +text\ Next we state the conditions we have on our trace: a normal behaviour FTP run from the intranet to some server in the internet on port 21. -*} +\ definition "accept_voip" :: "(adr\<^sub>i\<^sub>p, address voip_msg) history \ bool" where "accept_voip t = (\ c s g i p1 p2. t \ NB_voip c s g i p1 p2 \ is_in_intranet c @@ -107,10 +107,10 @@ fun packet_with_id where |"packet_with_id (x#xs) i = (if id x = i then (x#(packet_with_id xs i)) else (packet_with_id xs i))" -text{* +text\ The depth of the test case generation corresponds to the maximal length of generated traces, 4 is the minimum to get a full FTP protocol run. -*} +\ fun ids1 where "ids1 i (x#xs) = (id x = i \ ids1 i xs)" diff --git a/UPF_Firewall/FWNormalisation/ElementaryRules.thy b/UPF_Firewall/FWNormalisation/ElementaryRules.thy index 5a849ca..bd5ac85 100644 --- a/UPF_Firewall/FWNormalisation/ElementaryRules.thy +++ b/UPF_Firewall/FWNormalisation/ElementaryRules.thy @@ -35,7 +35,7 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *****************************************************************************) -subsection {* Elementary Firewall Policy Transformation Rules *} +subsection \Elementary Firewall Policy Transformation Rules\ theory ElementaryRules imports @@ -43,10 +43,10 @@ theory begin -text{* +text\ This theory contains those elementary transformation rules which are presented in the ICST 2010 paper~\cite{brucker.ea:firewall:2010}. They are not used elsewhere. -*} +\ lemma elem1: "C (AllowPortFromTo x y p \ DenyAllFromTo x y) = C (DenyAllFromTo x y)" diff --git a/UPF_Firewall/FWNormalisation/FWNormalisation.thy b/UPF_Firewall/FWNormalisation/FWNormalisation.thy index 59575fd..833d13a 100644 --- a/UPF_Firewall/FWNormalisation/FWNormalisation.thy +++ b/UPF_Firewall/FWNormalisation/FWNormalisation.thy @@ -34,7 +34,7 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *****************************************************************************) -section {* Firewall Policy Normalisation *} +section \Firewall Policy Normalisation\ theory FWNormalisation imports diff --git a/UPF_Firewall/FWNormalisation/FWNormalisationCore.thy b/UPF_Firewall/FWNormalisation/FWNormalisationCore.thy index 04cfca2..7f62e65 100644 --- a/UPF_Firewall/FWNormalisation/FWNormalisationCore.thy +++ b/UPF_Firewall/FWNormalisation/FWNormalisationCore.thy @@ -35,14 +35,14 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *****************************************************************************) -subsection {* Policy Normalisation: Core Definitions *} +subsection \Policy Normalisation: Core Definitions\ theory FWNormalisationCore imports "../PacketFilter/PacketFilter" begin -text{* +text\ This theory contains all the definitions used for policy normalisation as described in~\cite{brucker.ea:icst:2010,brucker.ea:formal-fw-testing:2014}. @@ -71,17 +71,17 @@ text{* normalization procedure does not aim to minimize the number of rules. While it does remove unnecessary ones, it also adds new ones, enabling a policy to be split into several independent parts. -*} +\ -text{* +text\ Policy transformations are functions that map policies to policies. We decided to represent policy transformations as \emph{syntactic rules}; this choice paves the way for expressing the entire normalisation process inside HOL by functions manipulating abstract policy syntax. -*} +\ -subsubsection{* Basics *} -text{* We define a very simple policy language: *} +subsubsection\Basics\ +text\We define a very simple policy language:\ datatype ('\,'\) Combinators = DenyAll @@ -89,18 +89,18 @@ datatype ('\,'\) Combinators = | AllowPortFromTo '\ '\ '\ | Conc "(('\,'\) Combinators)" "(('\,'\) Combinators)" (infixr "\" 80) -text{* +text\ And define the semantic interpretation of it. For technical reasons, we fix here the type to policies over IntegerPort addresses. However, we could easily provide definitions for other address types as well, using a generic constants for the type definition and a primitive recursive definition for each desired address model. -*} +\ -subsubsection{* Auxiliary definitions and functions. *} -text{* +subsubsection\Auxiliary definitions and functions.\ +text\ This section defines several functions which are useful later for the combinators, invariants, and proofs. -*} +\ fun srcNet where "srcNet (DenyAllFromTo x y) = x" @@ -153,10 +153,10 @@ fun bothNet where |"bothNet (AllowPortFromTo a b p) = {a,b}" |"bothNet (v \ va) = undefined " -text{* +text\ $Nets\_List$ provides from a list of rules a list where the entries are the appearing sets of source and destination network of each rule. -*} +\ definition Nets_List where @@ -209,21 +209,21 @@ fun firstList where "firstList (x#xs) = (first_bothNet x)" |"firstList [] = {}" -subsubsection{* Invariants *} +subsubsection\Invariants\ -text{* If there is a DenyAll, it is at the first position *} +text\If there is a DenyAll, it is at the first position\ fun wellformed_policy1:: "(('\, '\) Combinators) list \ bool" where "wellformed_policy1 [] = True" | "wellformed_policy1 (x#xs) = (DenyAll \ (set xs))" -text{* There is a DenyAll at the first position *} +text\There is a DenyAll at the first position\ fun wellformed_policy1_strong:: "(('\, '\) Combinators) list \ bool" where "wellformed_policy1_strong [] = False" | "wellformed_policy1_strong (x#xs) = (x=DenyAll \ (DenyAll \ (set xs)))" -text{* All two networks are either disjoint or equal. *} +text\All two networks are either disjoint or equal.\ definition netsDistinct where "netsDistinct a b = (\ (\ x. x \ a \ x \ b))" definition twoNetsDistinct where @@ -237,7 +237,7 @@ definition disjSD_2 where "disjSD_2 x y = (\ a b c d. ((a,b)\sdnets x \ (c,d) \sdnets y \ (twoNetsDistinct a b c d \ twoNetsDistinct a b d c)))" -text{* The policy is given as a list of single rules. *} +text\The policy is given as a list of single rules.\ fun singleCombinators where "singleCombinators [] = True" |"singleCombinators ((x\y)#xs) = False" @@ -246,7 +246,7 @@ fun singleCombinators where definition onlyTwoNets where "onlyTwoNets x = ((\ a b. (sdnets x = {(a,b)})) \ (\ a b. sdnets x = {(a,b),(b,a)}))" -text{* Each entry of the list contains rules between two networks only. *} +text\Each entry of the list contains rules between two networks only.\ fun OnlyTwoNets where "OnlyTwoNets (DenyAll#xs) = OnlyTwoNets xs" |"OnlyTwoNets (x#xs) = (onlyTwoNets x \ OnlyTwoNets xs)" @@ -274,12 +274,12 @@ fun NetsCollected2 where NetsCollected2 xs))" |"NetsCollected2 [] = True" -subsubsection{* Transformations *} +subsubsection\Transformations\ -text {* +text \ The following two functions transform a policy into a list of single rules and vice-versa (by staying on the combinator level). -*} +\ fun policy2list::"('\, '\) Combinators \ (('\, '\) Combinators) list" where @@ -292,7 +292,7 @@ fun list2FWpolicy::"(('\, '\) Combinators) list \ |"list2FWpolicy (x#[]) = x" |"list2FWpolicy (x#y) = x \ (list2FWpolicy y)" -text{* Remove all the rules appearing before a DenyAll. There are two alternative versions. *} +text\Remove all the rules appearing before a DenyAll. There are two alternative versions.\ fun removeShadowRules1 where "removeShadowRules1 (x#xs) = (if (DenyAll \ set xs) @@ -311,9 +311,9 @@ definition removeShadowRules1_alternative where "removeShadowRules1_alternative p = rev (removeShadowRules1_alternative_rev (rev p))" -text{* +text\ Remove all the rules which allow a port, but are shadowed by a deny between these subnets. - *} +\ fun removeShadowRules2:: "(('\, '\) Combinators) list \ (('\, '\) Combinators) list" @@ -325,10 +325,10 @@ where | "removeShadowRules2 (x#y) = x#(removeShadowRules2 y)" | "removeShadowRules2 [] = []" -text{* +text\ Sorting a policies: We first need to define an ordering on rules. This ordering depends on the $Nets\_List$ of a policy. -*} +\ fun smaller :: "('\, '\) Combinators \ ('\, '\) Combinators \ @@ -343,7 +343,7 @@ where else (position (bothNet x) l <= position (bothNet y) l)))" -text{* We provide two different sorting algorithms: Quick Sort (qsort) and Insertion Sort (sort) *} +text\We provide two different sorting algorithms: Quick Sort (qsort) and Insertion Sort (sort)\ fun qsort where "qsort [] l = []" @@ -377,10 +377,10 @@ fun separate where else (x#(separate(y#z))))" |"separate x = x" -text {* +text \ Insert the DenyAllFromTo rules, such that traffic between two networks can be tested individually. -*} +\ fun insertDenies where "insertDenies (x#xs) = (case x of DenyAll \ (DenyAll#(insertDenies xs)) @@ -389,11 +389,11 @@ fun insertDenies where (insertDenies xs))" | "insertDenies [] = []" -text{* +text\ Remove duplicate rules. This is especially necessary as insertDenies might have inserted duplicate rules. The second function is supposed to work on a list of policies. Only rules which are duplicated within the same policy are removed. -*} +\ fun removeDuplicates where @@ -405,7 +405,7 @@ fun removeAllDuplicates where "removeAllDuplicates (x#xs) = ((removeDuplicates (x))#(removeAllDuplicates xs))" |"removeAllDuplicates x = x" -text {* Insert a DenyAll at the beginning of a policy. *} +text \Insert a DenyAll at the beginning of a policy.\ fun insertDeny where "insertDeny (DenyAll#xs) = DenyAll#xs" |"insertDeny xs = DenyAll#xs" @@ -423,12 +423,12 @@ fun list2policyR::"(('\, '\) Combinators) list \ |"list2policyR [] = undefined " -text{* +text\ We provide the definitions for two address representations. -*} +\ -subsubsection{* IntPort *} +subsubsection\IntPort\ fun C :: "(adr\<^sub>i\<^sub>p net, port) Combinators \ (adr\<^sub>i\<^sub>p,DummyContent) packet \ unit" where @@ -455,20 +455,20 @@ lemma check: "rev (policy2list (rotatePolicy p)) = policy2list p" by (simp_all) -text{* +text\ All rules appearing at the left of a DenyAllFromTo, have disjunct domains from it (except DenyAll). -*} +\ fun (sequential) wellformed_policy2 where "wellformed_policy2 [] = True" | "wellformed_policy2 (DenyAll#xs) = wellformed_policy2 xs" | "wellformed_policy2 (x#xs) = ((\ c a b. c = DenyAllFromTo a b \ c \ set xs \ Map.dom (C x) \ Map.dom (C c) = {}) \ wellformed_policy2 xs)" -text{* +text\ An allow rule is disjunct with all rules appearing at the right of it. This invariant is not necessary as it is a consequence from others, but facilitates some proofs. -*} +\ fun (sequential) wellformed_policy3::"((adr\<^sub>i\<^sub>p net,port) Combinators) list \ bool" where "wellformed_policy3 [] = True" @@ -515,16 +515,16 @@ definition (qsort (removeShadowRules2 (remdups ((rm_MT_rules C) (insertDeny (removeShadowRules1 (policy2list p)))))) ((l)))))" -text{* +text\ Of course, normalize is equal to normalize', the latter looks nicer though. -*} +\ lemma "normalize = normalize'" by (rule ext, simp add: normalize_def normalize'_def sort'_def) declare C.simps [simp del] -subsubsection{* TCP\_UDP\_IntegerPort *} +subsubsection\TCP\_UDP\_IntegerPort\ fun Cp :: "(adr\<^sub>i\<^sub>p\<^sub>p net, protocol \ port) Combinators \ (adr\<^sub>i\<^sub>p\<^sub>p,DummyContent) packet \ unit" @@ -543,20 +543,20 @@ where |"Dp (AllowPortFromTo x y p) = Cp (AllowPortFromTo x y p)" |"Dp (x \ y) = Cp (y \ x)" -text{* +text\ All rules appearing at the left of a DenyAllFromTo, have disjunct domains from it (except DenyAll). -*} +\ fun (sequential) wellformed_policy2Pr where "wellformed_policy2Pr [] = True" | "wellformed_policy2Pr (DenyAll#xs) = wellformed_policy2Pr xs" | "wellformed_policy2Pr (x#xs) = ((\ c a b. c = DenyAllFromTo a b \ c \ set xs \ Map.dom (Cp x) \ Map.dom (Cp c) = {}) \ wellformed_policy2Pr xs)" -text{* +text\ An allow rule is disjunct with all rules appearing at the right of it. This invariant is not necessary as it is a consequence from others, but facilitates some proofs. -*} +\ fun (sequential) wellformed_policy3Pr::"((adr\<^sub>i\<^sub>p\<^sub>p net, protocol \ port) Combinators) list \ bool" where "wellformed_policy3Pr [] = True" @@ -605,17 +605,17 @@ definition (qsort (removeShadowRules2 (remdups ((rm_MT_rules Cp) (insertDeny (removeShadowRules1 (policy2list p)))))) ((l)))))" -text{* +text\ Of course, normalize is equal to normalize', the latter looks nicer though. -*} +\ lemma "normalizePr = normalizePr'" by (rule ext, simp add: normalizePr_def normalizePr'_def sort'_def) -text{* +text\ The following definition helps in creating the test specification for the individual parts of a normalized policy. -*} +\ definition makeFUTPr where "makeFUTPr FUT p x n = (packet_Nets x (fst (normBothNets (bothNets p)!n)) diff --git a/UPF_Firewall/FWNormalisation/NormalisationGenericProofs.thy b/UPF_Firewall/FWNormalisation/NormalisationGenericProofs.thy index 0a9bb28..b4a2f43 100644 --- a/UPF_Firewall/FWNormalisation/NormalisationGenericProofs.thy +++ b/UPF_Firewall/FWNormalisation/NormalisationGenericProofs.thy @@ -35,17 +35,17 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *****************************************************************************) -subsection{* Normalisation Proofs (Generic) *} +subsection\Normalisation Proofs (Generic)\ theory NormalisationGenericProofs imports FWNormalisationCore begin -text {* +text \ This theory contains the generic proofs of the normalisation procedure, i.e. those which are independent from the concrete semantical interpretation function. -*} +\ lemma domNMT: "dom X \ {} \ X \ \" by auto @@ -1631,7 +1631,7 @@ next case DenyAll thus ?thesis using assms DenyAll DenyAllFromTo by simp next case (DenyAllFromTo e f) thus ?thesis using assms DenyAllFromTo - by (metis DenyAllFromTo `a = DenyAllFromTo c d` bothNet.simps(2) smalleraux2) + by (metis DenyAllFromTo \a = DenyAllFromTo c d\ bothNet.simps(2) smalleraux2) next case (AllowPortFromTo e f g) thus ?thesis using assms DenyAllFromTo AllowPortFromTo by simp (metis eq_imp_le pos_noteq) @@ -1647,7 +1647,7 @@ next using assms by simp (metis AllowPortFromTo DenyAllFromTo bothNet.simps(3) smalleraux2a) next case (AllowPortFromTo e f g) thus ?thesis - using assms by(simp)(metis AllowPortFromTo `a = AllowPortFromTo c d p` + using assms by(simp)(metis AllowPortFromTo \a = AllowPortFromTo c d p\ bothNet.simps(3) smalleraux2c) next case (Conc e f) thus ?thesis using assms by simp @@ -1747,11 +1747,11 @@ next case DenyAll thus ?thesis by simp next case (DenyAllFromTo e f) thus ?thesis using DenyAllFromTo - by (auto simp: eq_imp_le `a = DenyAllFromTo c d`) + by (auto simp: eq_imp_le \a = DenyAllFromTo c d\) next - case (AllowPortFromTo e f p) thus ?thesis using `a = DenyAllFromTo c d` by simp + case (AllowPortFromTo e f p) thus ?thesis using \a = DenyAllFromTo c d\ by simp next - case (Conc e f) thus ?thesis using Conc `a = DenyAllFromTo c d` by simp + case (Conc e f) thus ?thesis using Conc \a = DenyAllFromTo c d\ by simp qed next case (AllowPortFromTo c d p) thus ?thesis @@ -1760,7 +1760,7 @@ next next case (DenyAllFromTo e f) thus ?thesis using AllowPortFromTo by simp next - case (AllowPortFromTo e f p2) thus ?thesis using `a = AllowPortFromTo c d p` by simp + case (AllowPortFromTo e f p2) thus ?thesis using \a = AllowPortFromTo c d p\ by simp next case (Conc e f) thus ?thesis using AllowPortFromTo by simp qed @@ -1913,14 +1913,14 @@ proof - fix aa::"('a, 'b) Combinators" assume 6: "aa \ set p" show "first_bothNet a \ first_bothNet aa" - apply(insert 1 2 3 4 5 6 `a = DenyAll`, simp_all) + apply(insert 1 2 3 4 5 6 \a = DenyAll\, simp_all) using fMTaux noDA by blast next case (DenyAllFromTo x21 x22) fix aa::"('a, 'b) Combinators" assume 6: "first_bothNet a \ firstList p" and 7 :"aa \ set p" show "first_bothNet a \ first_bothNet aa" - apply(insert 1 2 3 4 5 6 7 `a = DenyAllFromTo x21 x22`) + apply(insert 1 2 3 4 5 6 7 \a = DenyAllFromTo x21 x22\) apply(case_tac aa, simp_all) apply (meson NCSaux1) apply (meson NCSaux2) @@ -1930,7 +1930,7 @@ proof - fix aa::"('a, 'b) Combinators" assume 6: "first_bothNet a \ firstList p" and 7 :"aa \ set p" show "first_bothNet a \ first_bothNet aa" - apply(insert 1 2 3 4 6 7 `a = AllowPortFromTo x31 x32 x33`) + apply(insert 1 2 3 4 6 7 \a = AllowPortFromTo x31 x32 x33\) apply(case_tac aa, simp_all) apply (meson NCSaux3) apply (meson NCSaux4) @@ -1939,7 +1939,7 @@ proof - case (Conc x41 x42) fix aa::"('a, 'b) Combinators" show "first_bothNet a \ first_bothNet aa" - by(insert 3 4 `a = x41 \ x42`,simp) + by(insert 3 4 \a = x41 \ x42\,simp) qed qed @@ -2271,7 +2271,7 @@ next (\aa\set p. first_bothNet a \ first_bothNet aa) \ NetsCollected p \ noDenyAll1 (a # p) \ allNetsDistinct (a # p) \ (\s. s \ set p \ disjSD_2 a s) \ separated p" - apply(insert Cons.hyps `a = DenyAll`) + apply(insert Cons.hyps \a = DenyAll\) apply (intro impI,drule mp, erule OTNConc,drule mp) apply (case_tac p, simp_all) apply (case_tac a, simp_all) @@ -2283,7 +2283,7 @@ next (\aa\set p. first_bothNet a \ first_bothNet aa) \ NetsCollected p \ noDenyAll1 (a # p) \ allNetsDistinct (a # p) \ (\s. s \ set p \ disjSD_2 a s) \ separated p" - apply(insert Cons.hyps `a \ DenyAll`) + apply(insert Cons.hyps \a \ DenyAll\) by (metis NetsCollected.simps(1) NetsCollected2.simps(1) separated.simps(1) separatedNC) qed qed diff --git a/UPF_Firewall/FWNormalisation/NormalisationIPPProofs.thy b/UPF_Firewall/FWNormalisation/NormalisationIPPProofs.thy index aface81..4c86dd1 100644 --- a/UPF_Firewall/FWNormalisation/NormalisationIPPProofs.thy +++ b/UPF_Firewall/FWNormalisation/NormalisationIPPProofs.thy @@ -35,16 +35,16 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *****************************************************************************) -subsection {* Normalisation Proofs: Integer Protocol *} +subsection \Normalisation Proofs: Integer Protocol\ theory NormalisationIPPProofs imports NormalisationIntegerPortProof begin -text{* +text\ Normalisation proofs which are specific to the IntegerProtocol address representation. -*} +\ lemma ConcAssoc: "Cp((A \ B) \ D) = Cp(A \ (B \ D))" by (simp add: Cp.simps) @@ -980,7 +980,7 @@ next case True thus ?thesis using Cons by (simp) (rule impI, simp) next case False thus ?thesis - using Cons False `\ not_MT Cp ys` apply (simp) + using Cons False \\ not_MT Cp ys\ apply (simp) apply (intro conjI impI| simp)+ apply (subgoal_tac "rm_MT_rules Cp ys = []") apply (subgoal_tac "x \ dom (Cp (list2FWpolicy ys))") @@ -1547,7 +1547,7 @@ proof (cases "p") case Nil then show ?thesis by simp next case (Cons a list) show ?thesis - apply (insert `p = a # list`, simp_all) + apply (insert \p = a # list\, simp_all) proof (cases "a = DenyAll") case True assume * : "a = DenyAll" @@ -1706,7 +1706,7 @@ lemmas domain_reasoningPr = domDA ConcAssoc2 domSubset1 domSubset2 domSubsetDistr2 domSubsetDistrA domSubsetDistrD coerc_assoc ConcAssoc ConcAssoc3 -text {* The following lemmas help with the normalisation *} +text \The following lemmas help with the normalisation\ lemma list2policyR_Start[rule_format]: "p \ dom (Cp a) \ Cp (list2policyR (a # list)) p = Cp a p" by (induct "a # list" rule:list2policyR.induct) @@ -1824,9 +1824,9 @@ lemma norm_notMT_manual: "DenyAll \ set (policy2list p) \ no unfolding normalize_manual_orderPr_def by (simp add: idNMT rADnMT wellformed1_alternative_sorted wp1ID wp1_alternativesep wp1n_RS2) -text{* +text\ As an example, how this theorems can be used for a concrete normalisation instantiation. -*} +\ lemma normalizePrNAT: "DenyAll \ set (policy2list Filter) \ diff --git a/UPF_Firewall/FWNormalisation/NormalisationIntegerPortProof.thy b/UPF_Firewall/FWNormalisation/NormalisationIntegerPortProof.thy index 3952f95..c06e525 100644 --- a/UPF_Firewall/FWNormalisation/NormalisationIntegerPortProof.thy +++ b/UPF_Firewall/FWNormalisation/NormalisationIntegerPortProof.thy @@ -35,16 +35,16 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *****************************************************************************) -subsection {* Normalisation Proofs: Integer Port *} +subsection \Normalisation Proofs: Integer Port\ theory NormalisationIntegerPortProof imports NormalisationGenericProofs begin -text{* +text\ Normalisation proofs which are specific to the IntegerPort address representation. -*} +\ lemma ConcAssoc: "C((A \ B) \ D) = C(A \ (B \ D))" by (simp add: C.simps) @@ -967,7 +967,7 @@ next case True thus ?thesis using Cons by (simp) (rule impI, simp) next case False thus ?thesis - using Cons False `\ not_MT C ys` apply (simp) + using Cons False \\ not_MT C ys\ apply (simp) by (metis SR3nMT l2p_aux list2FWpolicy.simps(2) nMT_domMT nlpaux) qed qed @@ -1693,7 +1693,7 @@ lemmas domain_reasoning = domDA ConcAssoc2 domSubset1 domSubset2 domSubsetDistr2 domSubsetDistrA domSubsetDistrD coerc_assoc ConcAssoc ConcAssoc3 -text {* The following lemmas help with the normalisation *} +text \The following lemmas help with the normalisation\ lemma list2policyR_Start[rule_format]: "p \ dom (C a) \ C (list2policyR (a # list)) p = C a p" by (induct "a # list" rule:list2policyR.induct) (auto simp: C.simps dom_def map_add_def) @@ -1798,9 +1798,9 @@ lemma p_eq2_manual[rule_format]: lemma norm_notMT_manual: "DenyAll \ set (policy2list p) \ normalize_manual_order p l \ []" by (simp add: RS2_NMT idNMT normalize_manual_order_def rADnMT sepnMT sortnMT wp1ID) -text{* +text\ As an example, how this theorems can be used for a concrete normalisation instantiation. -*} +\ lemma normalizeNAT: "DenyAll \ set (policy2list Filter) \ allNetsDistinct (policy2list Filter) \ @@ -1813,11 +1813,11 @@ lemma normalizeNAT: lemma domSimpl[simp]: "dom (C (A \ DenyAll)) = dom (C (DenyAll))" by (simp add: PLemmas) -text {* +text \ The followin theorems can be applied when prepending the usual normalisation with an additional step and using another semantical interpretation function. This is a general recipe which can be applied whenever one nees to combine several normalisation strategies. -*} +\ lemma CRotate_eq_rotateC: "CRotate p = C (rotatePolicy p)" by (induct p rule: rotatePolicy.induct) (simp_all add: C.simps map_add_def) diff --git a/UPF_Firewall/NAT/NAT.thy b/UPF_Firewall/NAT/NAT.thy index bd06401..0ee2cd2 100644 --- a/UPF_Firewall/NAT/NAT.thy +++ b/UPF_Firewall/NAT/NAT.thy @@ -35,7 +35,7 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *****************************************************************************) -subsection{* Network Address Translation *} +subsection\Network Address Translation\ theory NAT imports @@ -91,10 +91,10 @@ definition srcPat2pool_IntProtocol :: "srcPat2pool_IntProtocol srcs transl = {x. (fst (src x)) \ srcs} \ (A\<^sub>f (srcPat2poolPort_Protocol_t transl))" -text{* +text\ The following lemmas are used for achieving a normalized output format of packages after applying NAT. This is used, e.g., by our firewall execution tool. -*} +\ lemma datasimp: "{(i, (s1, s2, s3), aba). \a aa b ba. aba = ((a, aa, b), ba) \ i = i1 \ s1 = i101 \ diff --git a/UPF_Firewall/PacketFilter/DatatypeAddress.thy b/UPF_Firewall/PacketFilter/DatatypeAddress.thy index 5b1f9a6..21186bd 100644 --- a/UPF_Firewall/PacketFilter/DatatypeAddress.thy +++ b/UPF_Firewall/PacketFilter/DatatypeAddress.thy @@ -35,17 +35,17 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *****************************************************************************) -subsection {* Datatype Addresses *} +subsection \Datatype Addresses\ theory DatatypeAddress imports NetworkCore begin -text{* +text\ A theory describing a network consisting of three subnetworks. Hosts within a network are not distinguished. -*} +\ datatype DatatypeAddress = dmz_adr | intranet_adr | internet_adr diff --git a/UPF_Firewall/PacketFilter/DatatypePort.thy b/UPF_Firewall/PacketFilter/DatatypePort.thy index 7498326..0c6406a 100644 --- a/UPF_Firewall/PacketFilter/DatatypePort.thy +++ b/UPF_Firewall/PacketFilter/DatatypePort.thy @@ -35,17 +35,17 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *****************************************************************************) -subsection {* Datatype Addresses with Ports *} +subsection \Datatype Addresses with Ports\ theory DatatypePort imports NetworkCore begin -text{* +text\ A theory describing a network consisting of three subnetworks, including port numbers modelled as Integers. Hosts within a network are not distinguished. -*} +\ datatype DatatypeAddress = dmz_adr | intranet_adr | internet_adr diff --git a/UPF_Firewall/PacketFilter/IPv4.thy b/UPF_Firewall/PacketFilter/IPv4.thy index 908f7b9..f1c139b 100644 --- a/UPF_Firewall/PacketFilter/IPv4.thy +++ b/UPF_Firewall/PacketFilter/IPv4.thy @@ -35,16 +35,16 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *****************************************************************************) -subsection {* Formalizing IPv4 Addresses *} +subsection \Formalizing IPv4 Addresses\ theory IPv4 imports NetworkCore begin -text{* +text\ A theory describing IPv4 addresses with ports. The host address is a four-tuple of Integers, the port number is a single Integer. -*} +\ type_synonym ipv4_ip = "(int \ int \ int \ int)" diff --git a/UPF_Firewall/PacketFilter/IPv4_TCPUDP.thy b/UPF_Firewall/PacketFilter/IPv4_TCPUDP.thy index b0a5ba5..1957073 100644 --- a/UPF_Firewall/PacketFilter/IPv4_TCPUDP.thy +++ b/UPF_Firewall/PacketFilter/IPv4_TCPUDP.thy @@ -35,7 +35,7 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *****************************************************************************) -subsection {* IPv4 with Ports and Protocols *} +subsection \IPv4 with Ports and Protocols\ theory IPv4_TCPUDP imports IPv4 diff --git a/UPF_Firewall/PacketFilter/IntegerAddress.thy b/UPF_Firewall/PacketFilter/IntegerAddress.thy index 8f2ff6b..224e90b 100644 --- a/UPF_Firewall/PacketFilter/IntegerAddress.thy +++ b/UPF_Firewall/PacketFilter/IntegerAddress.thy @@ -35,14 +35,14 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *****************************************************************************) -subsection {* Integer Addresses *} +subsection \Integer Addresses\ theory IntegerAddress imports NetworkCore begin -text{* A theory where addresses are modelled as Integers.*} +text\A theory where addresses are modelled as Integers.\ type_synonym adr\<^sub>i = "int" diff --git a/UPF_Firewall/PacketFilter/IntegerPort.thy b/UPF_Firewall/PacketFilter/IntegerPort.thy index ec0a97e..2b94d5b 100644 --- a/UPF_Firewall/PacketFilter/IntegerPort.thy +++ b/UPF_Firewall/PacketFilter/IntegerPort.thy @@ -35,17 +35,17 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *****************************************************************************) -subsection{* Integer Addresses with Ports *} +subsection\Integer Addresses with Ports\ theory IntegerPort imports NetworkCore begin -text{* +text\ A theory describing addresses which are modelled as a pair of Integers - the first being the host address, the second the port number. -*} +\ type_synonym address = int diff --git a/UPF_Firewall/PacketFilter/IntegerPort_TCPUDP.thy b/UPF_Firewall/PacketFilter/IntegerPort_TCPUDP.thy index efae0a0..bfbea89 100644 --- a/UPF_Firewall/PacketFilter/IntegerPort_TCPUDP.thy +++ b/UPF_Firewall/PacketFilter/IntegerPort_TCPUDP.thy @@ -35,15 +35,15 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *****************************************************************************) -subsection {* Integer Addresses with Ports and Protocols *} +subsection \Integer Addresses with Ports and Protocols\ theory IntegerPort_TCPUDP imports NetworkCore begin -text{* A theory describing addresses which are modelled as a pair of Integers - the first being - the host address, the second the port number.*} +text\A theory describing addresses which are modelled as a pair of Integers - the first being + the host address, the second the port number.\ type_synonym address = int @@ -92,7 +92,7 @@ lemma src_port: "src_port (a,x::adr\<^sub>i\<^sub>p\<^sub>p,d,e) = fst (snd x)" lemma dest_port: "dest_port (a,d,x::adr\<^sub>i\<^sub>p\<^sub>p,e) = fst (snd x)" by (simp add: dest_port_int_TCPUDP_def in_subnet) -text {* Common test constraints: *} +text \Common test constraints:\ definition port_positive :: "(adr\<^sub>i\<^sub>p\<^sub>p,'b) packet \ bool" where "port_positive x = (dest_port x > (0::port))" diff --git a/UPF_Firewall/PacketFilter/NetworkCore.thy b/UPF_Firewall/PacketFilter/NetworkCore.thy index ba6e261..a8181a1 100644 --- a/UPF_Firewall/PacketFilter/NetworkCore.thy +++ b/UPF_Firewall/PacketFilter/NetworkCore.thy @@ -35,14 +35,14 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *****************************************************************************) -subsection{* Packets and Networks *} +subsection\Packets and Networks\ theory NetworkCore imports Main begin -text{* +text\ In networks based e.g. on TCP/IP, a message from A to B is encapsulated in \emph{packets}, which contain the content of the message and routing information. The routing information mainly contains its source and its destination address. @@ -50,15 +50,15 @@ text{* In the case of stateless packet filters, a firewall bases its decision upon this routing information and, in the stateful case, on the content. Thus, we model a packet as a four-tuple of the mentioned elements, together with an id field. -*} +\ -text{* The ID is an integer: *} +text\The ID is an integer:\ type_synonym id = int -text{* +text\ To enable different representations of addresses (e.g. IPv4 and IPv6, with or without ports), we model them as an unconstrained type class and directly provide several instances: -*} +\ class adr type_synonym '\ src = "'\" @@ -70,36 +70,36 @@ instance nat ::adr .. instance "fun" :: (adr,adr) adr .. instance prod :: (adr,adr) adr .. -text{* +text\ The content is also specified with an unconstrained generic type: -*} +\ type_synonym '\ content = "'\" -text {* +text \ For applications where the concrete representation of the content field does not matter (usually the case for stateless packet filters), we provide a default type which can be used in those cases: -*} +\ datatype DummyContent = data -text{* Finally, a packet is:*} +text\Finally, a packet is:\ type_synonym ('\,'\) packet = "id \ '\ src \ '\ dest \ '\ content" -text{* +text\ Protocols (e.g. http) are not modelled explicitly. In the case of stateless packet filters, they are only visible by the destination port of a packet, which are modelled as part of the address. Additionally, stateful firewalls often determine the protocol by the content of a packet. -*} +\ definition src :: "('\::adr,'\) packet \ '\" where "src = fst o snd " -text{* +text\ Port numbers (which are part of an address) are also modelled in a generic way. The integers and the naturals are typical representations of port numbers. -*} +\ class port @@ -108,13 +108,13 @@ instance nat :: port .. instance "fun" :: (port,port) port .. instance "prod" :: (port,port) port .. -text{* +text\ A packet therefore has two parameters, the first being the address, the second the content. For the sake of simplicity, we do not allow to have a different address representation format for the source and the destination of a packet. To access the different parts of a packet directly, we define a couple of projectors: -*} +\ definition id :: "('\::adr,'\) packet \ id" where "id = fst" @@ -135,28 +135,28 @@ lemma either2[simp]: "(a \ tcp) = (a = udp)" lemma either3[simp]: "(a \ udp) = (a = tcp)" by (case_tac "a",simp_all) -text{* +text\ The following two constants give the source and destination port number of a packet. Address representations using port numbers need to provide a definition for these types. -*} +\ consts src_port :: "('\::adr,'\) packet \ '\::port" consts dest_port :: "('\::adr,'\) packet \ '\::port" consts src_protocol :: "('\::adr,'\) packet \ protocol" consts dest_protocol :: "('\::adr,'\) packet \ protocol" -text{* A subnetwork (or simply a network) is a set of sets of addresses.*} +text\A subnetwork (or simply a network) is a set of sets of addresses.\ type_synonym '\ net = "'\ set set" -text{* The relation {in\_subnet} (@{text "\"}) checks if an address is in a specific network. *} +text\The relation {in\_subnet} (\\\) checks if an address is in a specific network.\ definition in_subnet :: "'\::adr \ '\ net \ bool" (infixl "\" 100) where "in_subnet a S = (\ s \ S. a \ s)" -text{* The following lemmas will be useful later. *} +text\The following lemmas will be useful later.\ lemma in_subnet: "(a, e) \ {{(x1,y). P x1 y}} = P a e" @@ -170,10 +170,10 @@ lemma dest_in_subnet: "dest (q,r,((a),e),t) \ {{(x1,y). P x1 y}} = P a e" by (simp add: in_subnet_def in_subnet dest_def) -text{* +text\ Address models should provide a definition for the following constant, returning a network consisting of the input address only. -*} +\ consts subnet_of :: "'\::adr \ '\ net" diff --git a/UPF_Firewall/PacketFilter/NetworkModels.thy b/UPF_Firewall/PacketFilter/NetworkModels.thy index cb5b3e9..04f0b9c 100644 --- a/UPF_Firewall/PacketFilter/NetworkModels.thy +++ b/UPF_Firewall/PacketFilter/NetworkModels.thy @@ -35,7 +35,7 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *****************************************************************************) -section{* Network Models *} +section\Network Models\ theory NetworkModels imports @@ -50,7 +50,7 @@ theory IPv4_TCPUDP begin -text{* +text\ One can think of many different possible address representations. In this distribution, we include seven different variants: \begin{itemize} @@ -74,6 +74,6 @@ text{* The theories of each pf the networks are relatively small. It suffices to provide the required types, a couple of lemmas, and - if required - a definition for the source and destination ports of a packet. -*} +\ end diff --git a/UPF_Firewall/PacketFilter/PacketFilter.thy b/UPF_Firewall/PacketFilter/PacketFilter.thy index 42cbf0c..a801c7b 100644 --- a/UPF_Firewall/PacketFilter/PacketFilter.thy +++ b/UPF_Firewall/PacketFilter/PacketFilter.thy @@ -34,7 +34,7 @@ * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *****************************************************************************) -section {* Network Policies: Packet Filter *} +section \Network Policies: Packet Filter\ theory PacketFilter imports diff --git a/UPF_Firewall/PacketFilter/PolicyCombinators.thy b/UPF_Firewall/PacketFilter/PolicyCombinators.thy index 674aeba..e591df3 100644 --- a/UPF_Firewall/PacketFilter/PolicyCombinators.thy +++ b/UPF_Firewall/PacketFilter/PolicyCombinators.thy @@ -35,17 +35,17 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *****************************************************************************) -subsection {* Policy Combinators *} +subsection \Policy Combinators\ theory PolicyCombinators imports PolicyCore begin -text{* In order to ease the specification of a concrete policy, we +text\In order to ease the specification of a concrete policy, we define some combinators. Using these combinators, the specification of a policy gets very easy, and can be done similarly as in tools - like IPTables. *} + like IPTables.\ definition allow_all_from :: "'\::adr net \ (('\,'\) packet \ unit)" where @@ -73,9 +73,9 @@ definition "deny_all_from_to src_net dest_net = {pa. src pa \ src_net \ dest pa \ dest_net} \ D\<^sub>U" -text{* All these combinators and the default rules are put into one - single lemma called @{text PolicyCombinators} to facilitate proving - over policies. *} +text\All these combinators and the default rules are put into one + single lemma called \PolicyCombinators\ to facilitate proving + over policies.\ lemmas PolicyCombinators = allow_all_from_def deny_all_from_def diff --git a/UPF_Firewall/PacketFilter/PolicyCore.thy b/UPF_Firewall/PacketFilter/PolicyCore.thy index d0b55f7..4633d5c 100644 --- a/UPF_Firewall/PacketFilter/PolicyCore.thy +++ b/UPF_Firewall/PacketFilter/PolicyCore.thy @@ -35,7 +35,7 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *****************************************************************************) -subsection {* Policy Core *} +subsection \Policy Core\ theory PolicyCore imports @@ -44,25 +44,25 @@ theory begin -text{* A policy is seen as a partial mapping from packet to packet out. *} +text\A policy is seen as a partial mapping from packet to packet out.\ type_synonym ('\, '\) FWPolicy = "('\, '\) packet \ unit" -text{* +text\ When combining several rules, the firewall is supposed to apply the first matching one. In our setting this means the first rule which - maps the packet in question to @{text "Some (packet out)"}. This is - exactly what happens when using the map-add operator (@{text "rule1 - ++ rule2"}). The only difference is that the rules must be given in + maps the packet in question to \Some (packet out)\. This is + exactly what happens when using the map-add operator (\rule1 + ++ rule2\). The only difference is that the rules must be given in reverse order. -*} +\ -text{* - The constant @{text p_accept} is @{text "True"} iff the policy +text\ + The constant \p_accept\ is \True\ iff the policy accepts the packet. -*} +\ definition p_accept :: "('\, '\) packet \ ('\, '\) FWPolicy \ bool" where diff --git a/UPF_Firewall/PacketFilter/PortCombinators.thy b/UPF_Firewall/PacketFilter/PortCombinators.thy index fb71df1..643c71d 100644 --- a/UPF_Firewall/PacketFilter/PortCombinators.thy +++ b/UPF_Firewall/PacketFilter/PortCombinators.thy @@ -35,14 +35,14 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *****************************************************************************) -subsection {* Policy Combinators with Ports *} +subsection \Policy Combinators with Ports\ theory PortCombinators imports PolicyCombinators begin -text{* +text\ This theory defines policy combinators for those network models which have ports. They are provided in addition to the the ones defined in the PolicyCombinators theory. @@ -52,7 +52,7 @@ text{* \item $src\_port :: ('\alpha,'\beta) packet \Rightarrow ('\gamma::port)$ \item $dest\_port :: ('\alpha,'\beta) packet \Rightarrow ('\gamma::port)$ \end{itemize} -*} +\ definition allow_all_from_port :: "'\::adr net \ ('\::port) \ (('\,'\) packet \ unit)" where @@ -160,9 +160,9 @@ definition "allow_all_from_port_tos src_net s_port dest_net = {pa. dest_port pa \ s_port} \ allow_all_from_to src_net dest_net" -text{* +text\ As before, we put all the rules into one lemma called PortCombinators to ease writing later. -*} +\ lemmas PortCombinatorsCore = allow_all_from_port_def deny_all_from_port_def allow_all_to_port_def diff --git a/UPF_Firewall/PacketFilter/Ports.thy b/UPF_Firewall/PacketFilter/Ports.thy index fa60be2..dec2577 100644 --- a/UPF_Firewall/PacketFilter/Ports.thy +++ b/UPF_Firewall/PacketFilter/Ports.thy @@ -35,16 +35,16 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *****************************************************************************) -subsection {* Ports *} +subsection \Ports\ theory Ports imports Main begin -text{* +text\ This theory can be used if we want to specify the port numbers by names denoting their default - Integer values. If you want to use them, please add @{text Ports} to the simplifier. -*} + Integer values. If you want to use them, please add \Ports\ to the simplifier. +\ definition http::int where "http = 80" @@ -70,7 +70,7 @@ lemma ftp1: "x \ 21 \ x \ ftp" lemma ftp2: "x \ 21 \ ftp \ x" by (simp add: ftp_def) -text{* And so on for all desired port numbers. *} +text\And so on for all desired port numbers.\ lemmas Ports = http1 http2 ftp1 ftp2 smtp1 smtp2 diff --git a/UPF_Firewall/PacketFilter/ProtocolPortCombinators.thy b/UPF_Firewall/PacketFilter/ProtocolPortCombinators.thy index f6eac1e..f7733bf 100644 --- a/UPF_Firewall/PacketFilter/ProtocolPortCombinators.thy +++ b/UPF_Firewall/PacketFilter/ProtocolPortCombinators.thy @@ -35,7 +35,7 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *****************************************************************************) -subsection {* Policy Combinators with Ports and Protocols *} +subsection \Policy Combinators with Ports and Protocols\ theory ProtocolPortCombinators @@ -43,7 +43,7 @@ theory PortCombinators begin -text{* +text\ This theory defines policy combinators for those network models which have ports. They are provided in addition to the the ones defined in the PolicyCombinators theory. @@ -53,7 +53,7 @@ text{* \item $src\_port :: ('\alpha,'\beta) packet \Rightarrow ('\gamma::port)$ \item $dest\_port :: ('\alpha,'\beta) packet \Rightarrow ('\gamma::port)$ \end{itemize} -*} +\ definition allow_all_from_port_prot :: "protocol \ '\::adr net \ ('\::port) \ (('\,'\) packet \ unit)" where @@ -159,7 +159,7 @@ definition "deny_from_to_ports_prot p ports src_net dest_net = {pa. dest_protocol pa = p} \ deny_from_to_ports ports src_net dest_net" -text{* As before, we put all the rules into one lemma to ease writing later. *} +text\As before, we put all the rules into one lemma to ease writing later.\ lemmas ProtocolCombinatorsCore = allow_all_from_port_prot_def deny_all_from_port_prot_def allow_all_to_port_prot_def diff --git a/UPF_Firewall/ROOT b/UPF_Firewall/ROOT index d5e9353..cedf6ab 100644 --- a/UPF_Firewall/ROOT +++ b/UPF_Firewall/ROOT @@ -1,7 +1,7 @@ chapter AFP session "UPF_Firewall-devel" (AFP) = UPF + - description {* Formal Network Models and Their Application to Firewall Policies *} + description "Formal Network Models and Their Application to Firewall Policies" options [timeout = 600] theories "Examples/Examples" diff --git a/UPF_Firewall/StatefulFW/FTP.thy b/UPF_Firewall/StatefulFW/FTP.thy index 88c46b1..1b7044c 100644 --- a/UPF_Firewall/StatefulFW/FTP.thy +++ b/UPF_Firewall/StatefulFW/FTP.thy @@ -35,46 +35,46 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *****************************************************************************) -subsection {* The File Transfer Protocol (ftp) *} +subsection \The File Transfer Protocol (ftp)\ theory FTP imports StatefulCore begin -subsubsection{* The protocol syntax *} -text{* +subsubsection\The protocol syntax\ +text\ The File Transfer Protocol FTP is a well known example of a protocol which uses dynamic ports and is therefore a natural choice to use as an example for our model. We model only a simplified version of the FTP protocol over IntegerPort addresses, still containing all messages that matter for our purposes. It consists of the following four messages: \begin{enumerate} - \item @{text "init"}: The client contacts the server indicating + \item \init\: The client contacts the server indicating his wish to get some data. - \item @{text "ftp_port_request p"}: The client, usually after having + \item \ftp_port_request p\: The client, usually after having received an acknowledgement of the server, indicates a port number on which he wants to receive the data. - \item @{text "ftp_ftp_data"}: The server sends the requested data over + \item \ftp_ftp_data\: The server sends the requested data over the new channel. There might be an arbitrary number of such messages, including zero. - \item @{text "ftp_close"}: The client closes the connection. The + \item \ftp_close\: The client closes the connection. The dynamic port gets closed again. \end{enumerate} The content field of a packet therefore now consists of either one of those four messages or a default one. -*} +\ datatype msg = ftp_init | ftp_port_request port | ftp_data | ftp_close | ftp_other -text{* +text\ We now also make use of the ID field of a packet. It is used as session ID and we make the assumption that they are all unique among different protocol runs. At first, we need some predicates which check if a packet is a specific FTP message and has the correct session ID. -*} +\ definition is_init :: "id \ (adr\<^sub>i\<^sub>p, msg)packet \ bool" where @@ -104,8 +104,8 @@ 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" -subsubsection{* The protocol policy specification *} -text{* +subsubsection\The protocol policy specification\ +text\ We now have to model the respective state transitions. It is important to note that state transitions themselves allow all packets which are allowed by the policy, not only those which are allowed by the protocol. Their only task is to change the policy. As an alternative, we could @@ -116,7 +116,7 @@ text{* cases, one is enough. In our example, only messages 2 and 4 need special transitions. The default says that if the policy accepts the packet, it is added to the history, otherwise it is simply dropped. The policy remains the same in both cases. -*} +\ fun last_opened_port where "last_opened_port i ((j,s,d,ftp_port_request p)#xs) = (if i=j then p else last_opened_port i xs)" @@ -153,11 +153,11 @@ definition TRPolicy ::" (adr\<^sub>i\<^sub>p,msg)packet \ (adr\<^sub>i definition TRPolicy\<^sub>M\<^sub>o\<^sub>n where "TRPolicy\<^sub>M\<^sub>o\<^sub>n = policy2MON(TRPolicy)" -text{* If required to contain the policy in the output *} +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 ))" -text{* +text\ Now we specify our test scenario in more detail. We could test: \begin{itemize} \item one correct FTP-Protocol run, @@ -168,17 +168,17 @@ text{* \end{itemize} We only do the the simplest case here: one correct protocol run. -*} +\ -text{* +text\ There are four different states which are modelled as a datatype. -*} +\ datatype ftp_states = S0 | S1 | S2 | S3 -text{* - The following constant is @{text "True"} for all sets which are correct FTP runs for a given +text\ + The following constant is \True\ for all sets which are correct FTP runs for a given source and destination address, ID, and data-port number. -*} +\ fun @@ -197,13 +197,13 @@ fun 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)}" -text{* +text\ The following constant then returns a set of all the historys which denote such a normal behaviour FTP run, again for a given source and destination address, ID, and data-port. The following definition returns the set of all possible interleaving of two correct FTP protocol runs. -*} +\ definition ftp_2_interleaved :: "adr\<^sub>i\<^sub>p src \ adr\<^sub>i\<^sub>p dest \ id \ port \ adr\<^sub>i\<^sub>p src \ adr\<^sub>i\<^sub>p dest \ id \ port \ diff --git a/UPF_Firewall/StatefulFW/FTPVOIP.thy b/UPF_Firewall/StatefulFW/FTPVOIP.thy index c60f489..b613bb0 100644 --- a/UPF_Firewall/StatefulFW/FTPVOIP.thy +++ b/UPF_Firewall/StatefulFW/FTPVOIP.thy @@ -35,7 +35,7 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *****************************************************************************) -subsection {* FTP and VoIP Protocol *} +subsection \FTP and VoIP Protocol\ theory FTPVOIP imports @@ -56,13 +56,13 @@ datatype ftpvoip = ARQ | other -text{* +text\ We now also make use of the ID field of a packet. It is used as session ID and we make the assumption that they are all unique among different protocol runs. At first, we need some predicates which check if a packet is a specific FTP message and has the correct session ID. -*} +\ definition FTPVOIP_is_init :: "id \ (adr\<^sub>i\<^sub>p, ftpvoip ) packet \ bool" where @@ -140,19 +140,19 @@ definition "FTPVOIP_is_setup i port p = (id p = i \ content p = Setup port)" -text{* - We need also an operator @{text ports_open} to get access to the two +text\ + We need also an operator \ports_open\ to get access to the two dynamic ports. -*} +\ definition FTPVOIP_ports_open :: "id \ port \ port \ (adr\<^sub>i\<^sub>p, ftpvoip) history \ bool" where "FTPVOIP_ports_open i p L = ((not_before (FTPVOIP_is_fin i) (FTPVOIP_is_setup i (fst p)) L) \ not_before (FTPVOIP_is_fin i) (FTPVOIP_is_connect i (snd p)) L)" -text{* +text\ As we do not know which entity closes the connection, we define an operator which checks if the closer is the caller. -*} +\ fun FTPVOIP_src_is_initiator :: "id \ adr\<^sub>i\<^sub>p \ (adr\<^sub>i\<^sub>p,ftpvoip) history \ bool" where "FTPVOIP_src_is_initiator i a [] = False" @@ -243,11 +243,11 @@ subnet_of_int_def id_def FTPVOIP_port_open_def datatype ftp_states2 = FS0 | FS1 | FS2 | FS3 datatype voip_states2 = V0 | V1 | V2 | V3 | V4 | V5 -text{* - The constant @{text "is_voip"} checks if a trace corresponds to a +text\ + The constant \is_voip\ checks if a trace corresponds to a legal VoIP protocol, given the IP-addresses of the three entities, the ID, and the two dynamic ports. -*} +\ fun FTPVOIP_is_voip :: "voip_states2 \ address \ address \ address \ id \ port \ port \ (adr\<^sub>i\<^sub>p, ftpvoip) history \ bool" @@ -276,11 +276,11 @@ where FTPVOIP_is_voip V1 s d g i p1 p2 InL)))))) x)" -text{* - Finally, @{text "NB_voip"} returns the set of protocol traces which +text\ + Finally, \NB_voip\ returns the set of protocol traces which correspond to a correct protocol run given the three addresses, the ID, and the two dynamic ports. -*} +\ definition FTPVOIP_NB_voip :: "address \ address \ address \ id \ port \ port \ (adr\<^sub>i\<^sub>p, ftpvoip) history set" where diff --git a/UPF_Firewall/StatefulFW/FTP_WithPolicy.thy b/UPF_Firewall/StatefulFW/FTP_WithPolicy.thy index 6e3bdf8..827a34a 100644 --- a/UPF_Firewall/StatefulFW/FTP_WithPolicy.thy +++ b/UPF_Firewall/StatefulFW/FTP_WithPolicy.thy @@ -35,18 +35,18 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *****************************************************************************) -subsection {* FTP enriched with a security policy *} +subsection \FTP enriched with a security policy\ theory FTP_WithPolicy imports FTP begin -text{* FTP where the policy is part of the output. *} +text\FTP where the policy is part of the output.\ definition POL :: "'a \ 'a" where "POL x = x" -text{* Variant 2 takes the policy into the output *} +text\Variant 2 takes the policy into the output\ fun FTP_STP :: "((id \ port), adr\<^sub>i\<^sub>p, msg) FWStateTransitionP" where diff --git a/UPF_Firewall/StatefulFW/LTL_alike.thy b/UPF_Firewall/StatefulFW/LTL_alike.thy index ace3a79..97af265 100644 --- a/UPF_Firewall/StatefulFW/LTL_alike.thy +++ b/UPF_Firewall/StatefulFW/LTL_alike.thy @@ -35,27 +35,27 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *****************************************************************************) -subsection {* Termporal Combinators *} +subsection \Termporal Combinators\ theory LTL_alike imports Main begin -text{* +text\ In the following, we present a small embbeding of temporal combinators, that may help to formulate typical temporal properties in traces and protocols concisely. It is based on \emph{finite} lists, therefore the properties of this logic are not fully compatible with LTL based on Kripke-structures. For the purpose of this demonstration, however, the difference does not matter. -*} +\ fun nxt :: "('\ list \ bool) \ '\ list \ bool" ("N") where "nxt p [] = False" | "nxt p (a # S) = (p S)" -text{* Predicate $p$ holds at first position. *} +text\Predicate $p$ holds at first position.\ fun atom :: "('\ \ bool) \ '\ list \ bool" ("\_\") where @@ -71,10 +71,10 @@ where "always p [] = True" | "always p (a # S) = ((p (a # S)) \ always p S)" -text{* +text\ Always is a generalization of the \verb+list_all+ combinator from the List-library; if arguing 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) @@ -84,29 +84,29 @@ where | "eventually p (a # S) = ((p (a # S)) \ eventually p S)" -text{* +text\ Eventually is a generalization of the \verb+list_ex+ combinator from the List-library; if arguing 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) -text{* +text\ The next two constants will help us later in defining the state transitions. The constant - @{text "before"} is @{text "True"} if for all elements which appear before the first element - for which @{text q} holds, @{text p} must hold. -*} + \before\ is \True\ if for all elements which appear before the first element + for which \q\ holds, \p\ must hold. +\ fun before :: "('\ \ bool) \ ('\ \ bool) \ '\ list \ bool" where "before p q [] = False" | "before p q (a # S) = (q a \ (p a \ (before p q S)))" -text{* - Analogously there is an operator @{text not_before} which returns - @{text "True"} if for all elements which appear before the first - element for which @{text q} holds, @{text p} must not hold. -*} +text\ + Analogously there is an operator \not_before\ which returns + \True\ if for all elements which appear before the first + element for which \q\ holds, \p\ must not hold. +\ fun not_before :: "('\ \ bool) \ ('\ \ bool) \ '\ list \ bool" where @@ -122,13 +122,13 @@ lemma not_before_superfluous: done done -text{*General "before":*} +text\General "before":\ fun until :: "('\ list \ bool) \ ('\ list \ bool) \ '\ list \ bool" (infixl "U" 66) where "until p q [] = False" | "until p q (a # S) = (\ s t. a # S= s @ t \ p s \ q t)" -text{* This leads to this amazingly tricky proof:*} +text\This leads to this amazingly tricky proof:\ lemma before_vs_until: "(before p q) = ((\\p\) U \q\)" proof - diff --git a/UPF_Firewall/StatefulFW/StatefulCore.thy b/UPF_Firewall/StatefulFW/StatefulCore.thy index 384fe76..484257e 100644 --- a/UPF_Firewall/StatefulFW/StatefulCore.thy +++ b/UPF_Firewall/StatefulFW/StatefulCore.thy @@ -35,7 +35,7 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *****************************************************************************) -subsection {* Stateful Protocols: Foundations *} +subsection \Stateful Protocols: Foundations\ theory StatefulCore imports @@ -43,7 +43,7 @@ theory LTL_alike begin -text{* +text\ The simple system of a stateless packet filter is not enough to model all common real-world scenarios. Some protocols need further actions in order to be secured. A prominent example is the File Transfer Protocol (FTP), which is a popular means to move files across the Internet. @@ -65,16 +65,16 @@ 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)" -text{* Having a state, we need of course some state transitions. Such +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. -*} +\ type_synonym ('\,'\,'\) FWStateTransitionP = @@ -83,7 +83,7 @@ type_synonym ('\,'\,'\) FWStateTransitionP = type_synonym ('\,'\,'\) FWStateTransition = "(('\,'\) packet \ ('\,'\,'\) FWState) \ ('\,'\,'\) FWState" -text{* The memory could be modelled as a list of accepted packets. *} +text\The memory could be modelled as a list of accepted packets.\ type_synonym ('\,'\) history = "('\,'\) packet list" diff --git a/UPF_Firewall/StatefulFW/StatefulFW.thy b/UPF_Firewall/StatefulFW/StatefulFW.thy index 9596bac..94b927c 100644 --- a/UPF_Firewall/StatefulFW/StatefulFW.thy +++ b/UPF_Firewall/StatefulFW/StatefulFW.thy @@ -35,7 +35,7 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *****************************************************************************) -section {* Stateful Network Protocols *} +section \Stateful Network Protocols\ theory StatefulFW imports diff --git a/UPF_Firewall/StatefulFW/VOIP.thy b/UPF_Firewall/StatefulFW/VOIP.thy index 1940e77..be29d2e 100644 --- a/UPF_Firewall/StatefulFW/VOIP.thy +++ b/UPF_Firewall/StatefulFW/VOIP.thy @@ -35,12 +35,12 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *****************************************************************************) -subsection {* A simple voice-over-ip model *} +subsection \A simple voice-over-ip model\ theory VOIP imports StatefulCore begin -text{* +text\ After the FTP-Protocol which was rather simple we show the strength of the model with a more current and especially much more @@ -69,14 +69,14 @@ text{* \begin{itemize} \item Admission Request (ARQ) \item Admission Reject (ARJ) - \item Admission Confirm (ACF) @{text "'a"} + \item Admission Confirm (ACF) \'a\ \end{itemize} \item Call Signaling (Q.931, port 1720) The caller and the callee agree on the dynamic ports over which the call will take place. \begin{itemize} - \item Setup @{text "port"} - \item Connect @{text "port"} + \item Setup \port\ + \item Connect \port\ \end{itemize} \item Stream (dynamic ports). The call itself. In reality, several connections are used here. @@ -96,14 +96,14 @@ text{* we are not interested in the messages from the callee to its gatekeeper. Incoming calls are not modelled either, they would require a different set of state transitions. -*} +\ -text{* +text\ The content of a packet now consists of one of the seven messages or a default one. It is parameterized with the type of the address that the gatekeeper returns. -*} +\ datatype 'a voip_msg = ARQ @@ -114,11 +114,11 @@ datatype 'a voip_msg = ARQ | Stream | Fin | other -text{* +text\ As before, we need operators which check if a packet contains a specific content and ID, respectively if such a packet has appeared in the trace. -*} +\ definition @@ -139,10 +139,10 @@ definition "is_setup i port p = (id p = i \ content p = Setup port)" -text{* - We need also an operator @{text ports_open} to get access to the two +text\ + We need also an operator \ports_open\ to get access to the two dynamic ports. -*} +\ definition ports_open :: "id \ port \ port \ (adr\<^sub>i\<^sub>p, 'a voip_msg) history \ bool" where "ports_open i p L = ((not_before (is_fin i) (is_setup i (fst p)) L) \ @@ -151,10 +151,10 @@ definition -text{* +text\ As we do not know which entity closes the connection, we define an operator which checks if the closer is the caller. -*} +\ fun src_is_initiator :: "id \ adr\<^sub>i\<^sub>p \ (adr\<^sub>i\<^sub>p,'b voip_msg) history \ bool" where "src_is_initiator i a [] = False" @@ -165,11 +165,11 @@ fun -text{* +text\ The first state transition is for those messages which do not change the policy. In this scenario, this only happens for the Stream messages. -*} +\ definition subnet_of_adr where "subnet_of_adr x = {{(a,b). a = x}}" @@ -259,16 +259,16 @@ definition VOIP_TRPolicy where "VOIP_TRPolicy = policy2MON ( ((VOIP_STA,VOIP_STD) \\<^sub>\ applyPolicy) o (\ (x,(y,z)). ((x,z),(x,(y,z)))))" -text{* +text\ For a full protocol run, six states are needed. -*} +\ datatype voip_states = S0 | S1 | S2 | S3 | S4 | S5 -text{* - The constant @{text "is_voip"} checks if a trace corresponds to a +text\ + The constant \is_voip\ checks if a trace corresponds to a legal VoIP protocol, given the IP-addresses of the three entities, the ID, and the two dynamic ports. -*} +\ fun is_voip :: "voip_states \ address \ address \ address \ id \ port \ port \ (adr\<^sub>i\<^sub>p, address voip_msg) history \ bool" @@ -297,11 +297,11 @@ where is_voip S1 s d g i p1 p2 InL)))))) x)" -text{* - Finally, @{text "NB_voip"} returns the set of protocol traces which +text\ + Finally, \NB_voip\ returns the set of protocol traces which correspond to a correct protocol run given the three addresses, the ID, and the two dynamic ports. -*} +\ definition NB_voip :: "address \ address \ address \ id \ port \ port \ (adr\<^sub>i\<^sub>p, address voip_msg) history set" where diff --git a/UPF_Firewall/UPF-Firewall.thy b/UPF_Firewall/UPF-Firewall.thy index 878797f..de10992 100644 --- a/UPF_Firewall/UPF-Firewall.thy +++ b/UPF_Firewall/UPF-Firewall.thy @@ -35,7 +35,7 @@ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *****************************************************************************) -chapter {* UPF Firewall *} +chapter \UPF Firewall\ theory "UPF-Firewall" imports @@ -44,7 +44,7 @@ theory "FWNormalisation/FWNormalisation" "StatefulFW/StatefulFW" begin -text{* +text\ This is the main entry point for specifications of firewall policies. -*} +\ end diff --git a/UPF_Firewall/document/root.bib b/UPF_Firewall/document/root.bib index 4c125f6..5d5f9e7 100644 --- a/UPF_Firewall/document/root.bib +++ b/UPF_Firewall/document/root.bib @@ -9,7 +9,7 @@ # {\providecommand{\isbn}{\textsc{isbn}} } # {\providecommand{\Cpp}{C++} } # {\providecommand{\Specsharp}{Spec\#} } - # {\providecommand{\doi}[1]{\href{http://dx.doi.org/#1}{doi: + # {\providecommand{\doi}[1]{\href{https://doi.org/#1}{doi: {\urlstyle{rm}\nolinkurl{#1}}}}} } @STRING{conf-tphols="\acs{tphols}" } @STRING{iso = {International Organization for Standardization} } diff --git a/UPF_Firewall/document/root.tex b/UPF_Firewall/document/root.tex index 66c21df..326a83b 100644 --- a/UPF_Firewall/document/root.tex +++ b/UPF_Firewall/document/root.tex @@ -172,7 +172,7 @@ \input{Transformation01.tex} \input{Transformation02.tex} \input{NAT-FW.tex} - \input{VoIP.tex} + \input{Voice_over_IP.tex} % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%