(*****************************************************************************
 * Copyright (c) 2005-2010 ETH Zurich, Switzerland
 *               2008-2015 Achim D. Brucker, Germany
 *               2009-2017 Université Paris-Sud, France
 *               2015-2017 The University of Sheffield, UK
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 *
 *     * Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *
 *     * Redistributions in binary form must reproduce the above
 *       copyright notice, this list of conditions and the following
 *       disclaimer in the documentation and/or other materials provided
 *       with the distribution.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 *****************************************************************************)

subsection‹Packets and Networks›
theory 
  NetworkCore
  imports 
    Main
begin

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.
  
  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:›
type_synonym id = int

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  = "'α"
type_synonym    'α dest = "'α"

instance int ::adr ..
instance nat ::adr ..

instance "fun" :: (adr,adr) adr ..
instance prod :: (adr,adr) adr ..

text‹
  The content is also specified with an unconstrained generic type: 
›
type_synonym 'β content = "'β"

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:›

type_synonym ('α,'β) packet = "id × 'α src × 'α dest × 'β content"

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‹
  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

instance int ::port ..
instance nat :: port ..
instance "fun" :: (port,port) port ..
instance "prod" :: (port,port) port ..

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"

definition dest :: "('α::adr,'β) packet ⇒ 'α dest"
  where "dest = fst o snd o snd"

definition content :: "('α::adr,'β) packet ⇒ 'β content"
  where "content = snd o snd o snd"

datatype protocol = tcp | udp

lemma either: "⟦a ≠ tcp;a ≠ udp⟧ ⟹ False"
  by (case_tac "a",simp_all)

lemma either2[simp]: "(a ≠ tcp) = (a = udp)"
  by (case_tac "a",simp_all)                 

lemma either3[simp]: "(a ≠ udp) = (a = tcp)"
  by (case_tac "a",simp_all)                

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.›

type_synonym 'α net = "'α set set"
 
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.›

lemma in_subnet: 
  "(a, e) ⊏ {{(x1,y). P x1 y}} = P a e"
  by (simp add: in_subnet_def)

lemma src_in_subnet: 
  "src(q,(a,e),r,t) ⊏ {{(x1,y). P x1 y}} = P a e"
  by (simp add: in_subnet_def in_subnet src_def)

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‹
  Address models should provide a definition for the following constant, returning a network 
  consisting of the input address only. 
›

consts subnet_of :: "'α::adr ⇒ 'α net"

lemmas packet_defs = in_subnet_def id_def content_def src_def dest_def

end

(*****************************************************************************
 * Copyright (c) 2005-2010 ETH Zurich, Switzerland
 *               2008-2015 Achim D. Brucker, Germany
 *               2009-2016 Université Paris-Sud, France
 *               2015-2016 The University of Sheffield, UK
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 *
 *     * Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *
 *     * Redistributions in binary form must reproduce the above
 *       copyright notice, this list of conditions and the following
 *       disclaimer in the documentation and/or other materials provided
 *       with the distribution.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 *****************************************************************************)

subsection ‹Datatype Addresses›
theory 
  DatatypeAddress
  imports 
    NetworkCore 
begin

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

definition
  dmz::"DatatypeAddress net" where
  "dmz = {{dmz_adr}}"
definition
  intranet::"DatatypeAddress net" where
  "intranet = {{intranet_adr}}"
definition
  internet::"DatatypeAddress net" where
  "internet = {{internet_adr}}"
  
end

(*****************************************************************************
 * Copyright (c) 2005-2010 ETH Zurich, Switzerland
 *               2008-2015 Achim D. Brucker, Germany
 *               2009-2016 Université Paris-Sud, France
 *               2015-2016 The University of Sheffield, UK
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 *
 *     * Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *
 *     * Redistributions in binary form must reproduce the above
 *       copyright notice, this list of conditions and the following
 *       disclaimer in the documentation and/or other materials provided
 *       with the distribution.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 *****************************************************************************)

subsection ‹Datatype Addresses with Ports›
theory 
  DatatypePort
  imports 
    NetworkCore
begin

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

type_synonym  
  port = int
type_synonym  
  DatatypePort =  "(DatatypeAddress × port)"

instance DatatypeAddress :: adr ..

definition
  dmz::"DatatypePort net" where
  "dmz = {{(a,b). a = dmz_adr}}"
definition
  intranet::"DatatypePort net" where
  "intranet = {{(a,b). a = intranet_adr}}"
definition
  internet::"DatatypePort net" where
  "internet = {{(a,b). a = internet_adr}}"

overloading src_port_datatype ≡ "src_port :: ('α::adr,'β) packet ⇒ 'γ::port" 
begin 
definition 
  "src_port_datatype (x::(DatatypePort,'β) packet)  ≡ (snd o fst o snd) x"
end 

overloading dest_port_datatype ≡ "dest_port :: ('α::adr,'β) packet ⇒ 'γ::port"
begin
definition 
  "dest_port_datatype (x::(DatatypePort,'β) packet)  ≡(snd o fst o snd o snd) x"
end 

overloading subnet_of_datatype ≡ "subnet_of :: 'α::adr ⇒ 'α net"
begin 
definition
  "subnet_of_datatype (x::DatatypePort) ≡ {{(a,b::int). a = fst x}}" 
end

lemma src_port : "src_port ((a,x,d,e)::(DatatypePort,'β) packet) = snd x"
  by (simp add: src_port_datatype_def in_subnet)

lemma dest_port : "dest_port ((a,d,x,e)::(DatatypePort,'β) packet) = snd x"
  by (simp add: dest_port_datatype_def in_subnet)
    
lemmas DatatypePortLemmas = src_port dest_port src_port_datatype_def dest_port_datatype_def 

end

(*****************************************************************************
 * Copyright (c) 2005-2010 ETH Zurich, Switzerland
 *               2008-2015 Achim D. Brucker, Germany
 *               2009-2016 Université Paris-Sud, France
 *               2015-2016 The University of Sheffield, UK
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 *
 *     * Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *
 *     * Redistributions in binary form must reproduce the above
 *       copyright notice, this list of conditions and the following
 *       disclaimer in the documentation and/or other materials provided
 *       with the distribution.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 *****************************************************************************)

subsection ‹Integer Addresses›
theory 
  IntegerAddress
  imports 
    NetworkCore
begin

text‹A theory where addresses are modelled as Integers.›

type_synonym 
  adr⇩i = "int" 
  
end

(*****************************************************************************
 * Copyright (c) 2005-2010 ETH Zurich, Switzerland
 *               2008-2015 Achim D. Brucker, Germany
 *               2009-2016 Université Paris-Sud, France
 *               2015-2016 The University of Sheffield, UK
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 *
 *     * Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *
 *     * Redistributions in binary form must reproduce the above
 *       copyright notice, this list of conditions and the following
 *       disclaimer in the documentation and/or other materials provided
 *       with the distribution.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 *****************************************************************************)

subsection‹Integer Addresses with Ports›
theory 
  IntegerPort
  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.
›

type_synonym 
  address = int

type_synonym 
  port = int

type_synonym 
  adr⇩i⇩p = "address × port" 

overloading src_port_int ≡ "src_port :: ('α::adr,'β) packet ⇒ 'γ::port" 
begin 
definition 
  "src_port_int (x::(adr⇩i⇩p,'β) packet)  ≡ (snd o fst  o snd) x"
end 

overloading dest_port_int ≡ "dest_port :: ('α::adr,'β) packet ⇒ 'γ::port"
begin
definition 
  "dest_port_int (x::(adr⇩i⇩p,'β) packet) ≡ (snd o fst o  snd o snd) x"
end 

overloading subnet_of_int ≡ "subnet_of :: 'α::adr ⇒ 'α net"
begin 
definition
  "subnet_of_int (x::(adr⇩i⇩p)) ≡ {{(a,b::int). a = fst x}}" 
end

lemma src_port: "src_port (a,x::adr⇩i⇩p,d,e) = snd x"
  by (simp add: src_port_int_def in_subnet)

lemma dest_port: "dest_port (a,d,x::adr⇩i⇩p,e) = snd x"
  by (simp add: dest_port_int_def in_subnet)

lemmas adr⇩i⇩pLemmas = src_port dest_port src_port_int_def dest_port_int_def

end

(*****************************************************************************
 * Copyright (c) 2005-2010 ETH Zurich, Switzerland
 *               2008-2015 Achim D. Brucker, Germany
 *               2009-2016 Université Paris-Sud, France
 *               2015-2016 The University of Sheffield, UK
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 *
 *     * Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *
 *     * Redistributions in binary form must reproduce the above
 *       copyright notice, this list of conditions and the following
 *       disclaimer in the documentation and/or other materials provided
 *       with the distribution.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 *****************************************************************************)

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.›

type_synonym 
  address = int

type_synonym 
  port = int 

type_synonym 
  adr⇩i⇩p⇩p = "address × port × protocol" 

instance protocol :: adr ..

overloading src_port_int_TCPUDP ≡ "src_port :: ('α::adr,'β) packet ⇒ 'γ::port" 
begin 
definition 
  "src_port_int_TCPUDP (x::(adr⇩i⇩p⇩p,'β) packet)  ≡ (fst o snd o fst  o snd) x"
end 

overloading dest_port_int_TCPUDP ≡ "dest_port :: ('α::adr,'β) packet ⇒ 'γ::port"
begin
definition 
  "dest_port_int_TCPUDP (x::(adr⇩i⇩p⇩p,'β) packet) ≡ (fst o snd o fst o  snd o snd) x"
end 

overloading subnet_of_int_TCPUDP ≡ "subnet_of :: 'α::adr ⇒ 'α net"
begin 
definition
  "subnet_of_int_TCPUDP (x::(adr⇩i⇩p⇩p)) ≡ {{(a,b,c). a = fst x}}::adr⇩i⇩p⇩p net" 
end

overloading src_protocol_int_TCPUDP ≡ "src_protocol :: ('α::adr,'β) packet ⇒ protocol"
begin
definition 
  "src_protocol_int_TCPUDP (x::(adr⇩i⇩p⇩p,'β) packet) ≡ (snd o snd o fst o snd) x"
end

overloading dest_protocol_int_TCPUDP ≡ "dest_protocol :: ('α::adr,'β) packet ⇒ protocol"
begin
definition 
  "dest_protocol_int_TCPUDP (x::(adr⇩i⇩p⇩p,'β) packet) ≡ (snd o snd o fst o snd o snd) x"
end

lemma src_port: "src_port (a,x::adr⇩i⇩p⇩p,d,e) = fst (snd x)"
  by (simp add: src_port_int_TCPUDP_def in_subnet)

lemma dest_port: "dest_port (a,d,x::adr⇩i⇩p⇩p,e) = fst (snd x)"
  by (simp add: dest_port_int_TCPUDP_def in_subnet)

text ‹Common test constraints:›

definition port_positive :: "(adr⇩i⇩p⇩p,'b) packet ⇒ bool" where
  "port_positive x = (dest_port x > (0::port))"

definition fix_values :: "(adr⇩i⇩p⇩p,DummyContent) packet ⇒ bool" where
  "fix_values x =  (src_port x = (1::port) ∧ src_protocol x = udp ∧ content x = data ∧ id x = 1)"


lemmas adr⇩i⇩p⇩pLemmas = src_port dest_port src_port_int_TCPUDP_def dest_port_int_TCPUDP_def 
  src_protocol_int_TCPUDP_def dest_protocol_int_TCPUDP_def subnet_of_int_TCPUDP_def 

lemmas adr⇩i⇩p⇩pTestConstraints = port_positive_def fix_values_def
  
end

(*****************************************************************************
 * Copyright (c) 2005-2010 ETH Zurich, Switzerland
 *               2008-2015 Achim D. Brucker, Germany
 *               2009-2016 Université Paris-Sud, France
 *               2015-2016 The University of Sheffield, UK
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 *
 *     * Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *
 *     * Redistributions in binary form must reproduce the above
 *       copyright notice, this list of conditions and the following
 *       disclaimer in the documentation and/or other materials provided
 *       with the distribution.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 *****************************************************************************)

subsection ‹Formalizing IPv4 Addresses›
theory 
  IPv4
  imports 
    NetworkCore
begin
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)" 

type_synonym 
  port    =  "int"

type_synonym 
  ipv4    =  "(ipv4_ip × port)"

overloading src_port_ipv4 ≡ "src_port :: ('α::adr,'β) packet ⇒ 'γ::port" 
begin 
definition 
  "src_port_ipv4 (x::(ipv4,'β) packet) ≡ (snd o fst o snd) x"
end 

overloading dest_port_ipv4 ≡ "dest_port :: ('α::adr,'β) packet ⇒ 'γ::port"
begin
definition 
  "dest_port_ipv4  (x::(ipv4,'β) packet) ≡ (snd o fst o snd o snd) x"
end 

overloading subnet_of_ipv4 ≡ "subnet_of :: 'α::adr ⇒ 'α net"
begin 
definition
  "subnet_of_ipv4 (x::ipv4) ≡ {{(a,b::int). a =  fst x}}" 
end

definition subnet_of_ip :: "ipv4_ip ⇒ ipv4 net"
  where "subnet_of_ip ip = {{(a,b). (a = ip)}}"

lemma src_port: "src_port (a,(x::ipv4),d,e) = snd x"
  by (simp add: src_port_ipv4_def in_subnet)

lemma dest_port: "dest_port (a,d,(x::ipv4),e) = snd x"
  by (simp add: dest_port_ipv4_def in_subnet)


lemmas IPv4Lemmas = src_port dest_port src_port_ipv4_def dest_port_ipv4_def

end

(*****************************************************************************
 * Copyright (c) 2005-2010 ETH Zurich, Switzerland
 *               2008-2015 Achim D. Brucker, Germany
 *               2009-2016 Université Paris-Sud, France
 *               2015-2016 The University of Sheffield, UK
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 *
 *     * Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *
 *     * Redistributions in binary form must reproduce the above
 *       copyright notice, this list of conditions and the following
 *       disclaimer in the documentation and/or other materials provided
 *       with the distribution.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 *****************************************************************************)

subsection ‹IPv4 with Ports and Protocols›
theory 
  IPv4_TCPUDP
  imports IPv4
begin

type_synonym 
  ipv4_TCPUDP    =  "(ipv4_ip × port × protocol)"
 
instance protocol :: adr ..

overloading src_port_ipv4_TCPUDP ≡ "src_port :: ('α::adr,'β) packet ⇒ 'γ::port" 
begin 
definition 
  "src_port_ipv4_TCPUDP (x::(ipv4_TCPUDP,'β) packet) ≡ (fst o snd o fst o snd) x"
end 

overloading dest_port_ipv4_TCPUDP ≡ "dest_port :: ('α::adr,'β) packet ⇒ 'γ::port"
begin
definition 
  "dest_port_ipv4_TCPUDP  (x::(ipv4_TCPUDP,'β) packet) ≡ (fst o snd o fst o snd o snd) x"
end 

overloading subnet_of_ipv4_TCPUDP ≡ "subnet_of :: 'α::adr ⇒ 'α net"
begin 
definition
  "subnet_of_ipv4_TCPUDP (x::ipv4_TCPUDP) ≡ {{(a,b). a = fst x}}::(ipv4_TCPUDP net)" 
end

overloading dest_protocol_ipv4_TCPUDP ≡ "dest_protocol :: ('α::adr,'β) packet ⇒ protocol"
begin
definition 
  "dest_protocol_ipv4_TCPUDP (x::(ipv4_TCPUDP,'β) packet) ≡ (snd o snd o fst o snd o snd) x"
end

definition subnet_of_ip :: "ipv4_ip ⇒ ipv4_TCPUDP net"
  where "subnet_of_ip ip = {{(a,b). (a = ip)}}"

lemma src_port: "src_port (a,(x::ipv4_TCPUDP),d,e) = fst (snd x)"
  by (simp add: src_port_ipv4_TCPUDP_def in_subnet)

lemma dest_port: "dest_port (a,d,(x::ipv4_TCPUDP),e) = fst (snd x)"
  by (simp add: dest_port_ipv4_TCPUDP_def in_subnet)

lemmas Ipv4_TCPUDPLemmas = src_port dest_port src_port_ipv4_TCPUDP_def dest_port_ipv4_TCPUDP_def 
  dest_protocol_ipv4_TCPUDP_def subnet_of_ipv4_TCPUDP_def
end

(*****************************************************************************
 * Copyright (c) 2005-2010 ETH Zurich, Switzerland
 *               2008-2015 Achim D. Brucker, Germany
 *               2009-2016 Université Paris-Sud, France
 *               2015-2016 The University of Sheffield, UK
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 *
 *     * Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *
 *     * Redistributions in binary form must reproduce the above
 *       copyright notice, this list of conditions and the following
 *       disclaimer in the documentation and/or other materials provided
 *       with the distribution.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (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 Models›
theory            
  NetworkModels
  imports
    DatatypeAddress
    DatatypePort

    IntegerAddress
    IntegerPort
    IntegerPort_TCPUDP

    IPv4
    IPv4_TCPUDP
begin

text‹
  One can think of many different possible address representations. In this distribution, we include 
  seven different variants:
  \begin{itemize} 
    \item DatatypeAddress: Three explicitly named addresses, which build up a network consisting of 
          three disjunct  subnetworks. I.e. there are no overlaps and there is no way to distinguish 
          between individual hosts within a network.
    \item DatatypePort: An address is a pair, with the first element being the same as above, and 
          the second being a port number modelled as an Integer\footnote{For technical reasons,
          we always use Integers instead of Naturals. As a consequence, the (test) specifications 
          have to be adjusted to eliminate negative numbers.}.
    \item adr\_i: An address in an Integer.
    \item adr\_ip: An address is a pair of an Integer and a port (which is again an Integer).
    \item adr\_ipp: An address is a triple consisting of two Integers modelling the IP address and 
          the port number, and the specification of the network protocol
    \item IPv4: An address is a pair. The first element is a four-tuple of Integers, modelling an 
          IPv4 address, the second element is an Integer denoting the port number.
    \item IPv4\_TCPUDP: The same as above, but including additionally the specification of the 
          network protocol.
  \end{itemize}

  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

(*****************************************************************************
 * Copyright (c) 2005-2010 ETH Zurich, Switzerland
 *               2008-2015 Achim D. Brucker, Germany
 *               2009-2016 Université Paris-Sud, France
 *               2015-2016 The University of Sheffield, UK
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 *
 *     * Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *
 *     * Redistributions in binary form must reproduce the above
 *       copyright notice, this list of conditions and the following
 *       disclaimer in the documentation and/or other materials provided
 *       with the distribution.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 *****************************************************************************)

subsection ‹Policy Core›
theory 
  PolicyCore
  imports 
     NetworkCore 
     UPF.UPF
begin


text‹A policy is seen as a partial mapping from packet to packet out.›

type_synonym ('α, 'β) FWPolicy = "('α, 'β) packet ↦ unit" 

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 ‹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 ‹p_accept› is ‹True› iff the policy
  accepts the packet. 
›

definition
  p_accept :: "('α, 'β) packet ⇒ ('α, 'β) FWPolicy ⇒ bool" where
  "p_accept p pol =  (pol p = ⌊allow ()⌋)"

end

(*****************************************************************************
 * Copyright (c) 2005-2010 ETH Zurich, Switzerland
 *               2008-2015 Achim D. Brucker, Germany
 *               2009-2017 Université Paris-Sud, France
 *               2015-2017 The University of Sheffield, UK
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 *
 *     * Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *
 *     * Redistributions in binary form must reproduce the above
 *       copyright notice, this list of conditions and the following
 *       disclaimer in the documentation and/or other materials provided
 *       with the distribution.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 *****************************************************************************)

subsection ‹Policy Combinators›
theory 
  PolicyCombinators
  imports 
    PolicyCore
begin

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.›

definition 
  allow_all_from :: "'α::adr net ⇒ (('α,'β) packet ↦ unit)" where
  "allow_all_from src_net =   {pa. src pa ⊏ src_net} ◃ A⇩U " 

definition 
  deny_all_from    :: "'α::adr net ⇒ (('α,'β) packet ↦ unit)" where
  "deny_all_from src_net   =  {pa. src pa ⊏  src_net}  ◃D⇩U "
        
definition
  allow_all_to    :: "'α::adr net ⇒ (('α,'β) packet ↦ unit)" where
  "allow_all_to dest_net   = {pa. dest pa ⊏  dest_net}  ◃ A⇩U"

definition 
  deny_all_to :: "'α::adr net ⇒ (('α,'β) packet ↦ unit)" where
  "deny_all_to dest_net = {pa. dest pa ⊏ dest_net} ◃D⇩U "

definition 
  allow_all_from_to    :: "'α::adr net ⇒ 'α::adr net ⇒ (('α,'β) packet ↦ unit)" where
  "allow_all_from_to src_net dest_net = 
                                   {pa. src pa ⊏ src_net ∧ dest pa ⊏ dest_net} ◃ A⇩U "

definition 
  deny_all_from_to    :: "'α::adr net ⇒ 'α::adr net ⇒ (('α,'β) packet ↦ unit)" where
  "deny_all_from_to src_net dest_net = {pa. src pa ⊏ src_net ∧ dest pa ⊏ dest_net} ◃ D⇩U"


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
  allow_all_to_def deny_all_to_def allow_all_from_to_def
  deny_all_from_to_def UPFDefs
                           
end

(*****************************************************************************
 * Copyright (c) 2005-2010 ETH Zurich, Switzerland
 *               2008-2015 Achim D. Brucker, Germany
 *               2009-2016 Université Paris-Sud, France
 *               2015-2016 The University of Sheffield, UK
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 *
 *     * Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *
 *     * Redistributions in binary form must reproduce the above
 *       copyright notice, this list of conditions and the following
 *       disclaimer in the documentation and/or other materials provided
 *       with the distribution.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 *****************************************************************************)

subsection ‹Policy Combinators with Ports›
theory 
  PortCombinators
  imports 
    PolicyCombinators
begin

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. 

  This theory requires from the network models a definition for the two following constants:
  \begin{itemize}
    \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
  "allow_all_from_port src_net s_port = {pa. src_port pa = s_port} ◃ allow_all_from src_net"
  
definition 
  deny_all_from_port    :: "'α::adr net ⇒ 'γ::port ⇒ (('α,'β) packet ↦ unit)" where
  "deny_all_from_port src_net s_port  = {pa. src_port pa = s_port} ◃ deny_all_from src_net "

definition
  allow_all_to_port    :: "'α::adr net ⇒ 'γ::port ⇒ (('α,'β) packet ↦ unit)" where
  "allow_all_to_port dest_net d_port  = {pa. dest_port pa = d_port} ◃ allow_all_to dest_net"

definition 
  deny_all_to_port :: "'α::adr net ⇒  'γ::port ⇒ (('α,'β) packet ↦ unit)" where
  "deny_all_to_port dest_net d_port = {pa. dest_port pa = d_port} ◃ deny_all_to dest_net"

definition
  allow_all_from_port_to:: "'α::adr net ⇒ 'γ::port ⇒ 'α::adr net ⇒ (('α,'β) packet ↦ unit)"
  where
    "allow_all_from_port_to src_net s_port dest_net   
       = {pa. src_port pa = s_port} ◃ allow_all_from_to src_net dest_net"

definition 
  deny_all_from_port_to::"'α::adr net ⇒  'γ::port ⇒ 'α::adr net ⇒ (('α,'β) packet ↦ unit)"
  where
    "deny_all_from_port_to src_net s_port dest_net  
      = {pa. src_port pa = s_port} ◃ deny_all_from_to src_net dest_net "

definition
  allow_all_from_port_to_port::"'α::adr net ⇒ 'γ::port ⇒ 'α::adr net ⇒ 'γ::port ⇒
                              (('α,'β) packet ↦ unit)" where
  "allow_all_from_port_to_port src_net s_port dest_net d_port = 
      {pa. dest_port pa = d_port} ◃ allow_all_from_port_to src_net s_port dest_net"

definition 
  deny_all_from_port_to_port :: "'α::adr net ⇒  'γ::port ⇒ 'α::adr net ⇒
                                 'γ::port ⇒ (('α,'β) packet ↦ unit)" where
  "deny_all_from_port_to_port src_net s_port dest_net d_port = 
     {pa. dest_port pa = d_port} ◃ deny_all_from_port_to src_net s_port dest_net"
  
definition 
  allow_all_from_to_port    :: "'α::adr net  ⇒ 'α::adr net ⇒
                                'γ::port ⇒ (('α,'β) packet ↦ unit)" where
  "allow_all_from_to_port src_net dest_net d_port =  
    {pa. dest_port pa = d_port} ◃ allow_all_from_to src_net dest_net"

definition 
  deny_all_from_to_port    :: "'α::adr net ⇒ 'α::adr net ⇒ 'γ::port ⇒
                               (('α,'β) packet ↦ unit)" where
  "deny_all_from_to_port src_net dest_net d_port = 
                                 {pa. dest_port pa = d_port} ◃ deny_all_from_to src_net dest_net"

definition 
  allow_from_port_to :: "'γ::port ⇒ 'α::adr net ⇒ 'α::adr net ⇒ (('α,'β) packet ↦ unit)"
  where 
    "allow_from_port_to port src_net dest_net =   
            {pa. src_port pa = port} ◃ allow_all_from_to src_net dest_net"

definition 
  deny_from_port_to :: "'γ::port ⇒ 'α::adr net ⇒ 'α::adr net ⇒ (('α,'β) packet ↦ unit)"
  where 
    "deny_from_port_to port src_net dest_net =   
            {pa. src_port pa = port} ◃ deny_all_from_to src_net dest_net"

definition 
  allow_from_to_port :: "'γ::port  ⇒ 'α::adr net ⇒ 'α::adr net ⇒ (('α,'β) packet ↦ unit)"
  where 
    "allow_from_to_port port src_net dest_net =   
         {pa. dest_port pa = port} ◃ allow_all_from_to src_net dest_net"

definition 
  deny_from_to_port :: "'γ::port  ⇒ 'α::adr net ⇒ 'α::adr net ⇒ (('α,'β) packet ↦ unit)"
  where 
    "deny_from_to_port port src_net dest_net =   
         {pa. dest_port pa = port} ◃ deny_all_from_to src_net dest_net"

definition 
  allow_from_ports_to :: "'γ::port set ⇒ 'α::adr net ⇒ 'α::adr net ⇒
                          (('α,'β) packet ↦ unit)" where
  "allow_from_ports_to ports src_net dest_net =   
         {pa. src_port pa ∈ ports} ◃ allow_all_from_to src_net dest_net"

definition 
  allow_from_to_ports :: "'γ::port set ⇒ 'α::adr net ⇒ 'α::adr net ⇒
                          (('α,'β) packet ↦ unit)" where
  "allow_from_to_ports ports src_net dest_net =   
        {pa. dest_port pa ∈ ports} ◃ allow_all_from_to src_net dest_net"

definition 
  deny_from_ports_to :: "'γ::port set ⇒ 'α::adr net ⇒ 'α::adr net ⇒
                          (('α,'β) packet ↦ unit)" where
  "deny_from_ports_to ports src_net dest_net =   
         {pa. src_port pa ∈ ports} ◃ deny_all_from_to src_net dest_net"

definition 
  deny_from_to_ports :: "'γ::port set ⇒ 'α::adr net ⇒ 'α::adr net ⇒
                          (('α,'β) packet ↦ unit)" where
  "deny_from_to_ports ports src_net dest_net =   
        {pa. dest_port pa ∈ ports} ◃ deny_all_from_to src_net dest_net"
  
definition
  allow_all_from_port_tos:: "'α::adr net ⇒ ('γ::port) set ⇒ 'α::adr net ⇒ (('α,'β) packet ↦ unit)"
  where
    "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‹
  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
  deny_all_to_port_def allow_all_from_to_port_def
  deny_all_from_to_port_def
  allow_from_ports_to_def allow_from_to_ports_def
  deny_from_ports_to_def deny_from_to_ports_def
  allow_all_from_port_to_def deny_all_from_port_to_def
  allow_from_port_to_def allow_from_to_port_def deny_from_to_port_def
  deny_from_port_to_def allow_all_from_port_tos_def

lemmas PortCombinators = PortCombinatorsCore PolicyCombinators

end

(*****************************************************************************
 * Copyright (c) 2005-2010 ETH Zurich, Switzerland
 *               2008-2015 Achim D. Brucker, Germany
 *               2009-2016 Université Paris-Sud, France
 *               2015-2016 The University of Sheffield, UK
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 *
 *     * Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *
 *     * Redistributions in binary form must reproduce the above
 *       copyright notice, this list of conditions and the following
 *       disclaimer in the documentation and/or other materials provided
 *       with the distribution.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 *****************************************************************************)

subsection ‹Policy Combinators with Ports and Protocols›

theory 
  ProtocolPortCombinators
  imports 
    PortCombinators
begin

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. 

  This theory requires from the network models a definition for the two following constants:
  \begin{itemize}
    \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
  "allow_all_from_port_prot p src_net s_port =   
       {pa. dest_protocol pa = p} ◃ allow_all_from_port src_net s_port"

definition 
  deny_all_from_port_prot    :: "protocol =>'α::adr net ⇒ 'γ::port ⇒ (('α,'β) packet ↦ unit)" where
  "deny_all_from_port_prot p src_net s_port =  
       {pa. dest_protocol pa = p} ◃ deny_all_from_port src_net s_port" 

definition
  allow_all_to_port_prot    :: "protocol =>'α::adr net ⇒ 'γ::port ⇒ (('α,'β) packet ↦ unit)" where
  "allow_all_to_port_prot p dest_net d_port  =  
     {pa. dest_protocol pa = p} ◃ allow_all_to_port dest_net d_port"

definition 
  deny_all_to_port_prot :: "protocol =>'α::adr net ⇒  'γ::port ⇒ (('α,'β) packet ↦ unit)" where
  "deny_all_to_port_prot p dest_net d_port = 
    {pa. dest_protocol pa = p} ◃ deny_all_to_port dest_net d_port"

definition
  allow_all_from_port_to_prot:: "protocol =>'α::adr net ⇒ 'γ::port ⇒ 'α::adr net ⇒ (('α,'β) packet ↦ unit)"
  where
    "allow_all_from_port_to_prot p src_net s_port dest_net =  
   {pa. dest_protocol pa = p} ◃ allow_all_from_port_to src_net s_port dest_net"

definition 
  deny_all_from_port_to_prot::"protocol ⇒ 'α::adr net ⇒  'γ::port ⇒ 'α::adr net ⇒ (('α,'β) packet ↦ unit)"
  where
    "deny_all_from_port_to_prot p src_net s_port dest_net = 
   {pa. dest_protocol pa = p} ◃  deny_all_from_port_to  src_net s_port dest_net"

definition
  allow_all_from_port_to_port_prot::"protocol ⇒ 'α::adr net ⇒ 'γ::port ⇒ 'α::adr net ⇒ 'γ::port ⇒
                              (('α,'β) packet ↦ unit)" where
  "allow_all_from_port_to_port_prot p src_net s_port dest_net d_port = 
       {pa. dest_protocol pa = p} ◃      allow_all_from_port_to_port src_net s_port dest_net d_port "

definition 
  deny_all_from_port_to_port_prot :: "protocol =>'α::adr net ⇒  'γ::port ⇒ 'α::adr net ⇒
                                 'γ::port ⇒ (('α,'β) packet ↦ unit)" where
  "deny_all_from_port_to_port_prot p src_net s_port dest_net d_port =              
   {pa. dest_protocol pa = p} ◃       deny_all_from_port_to_port src_net s_port dest_net d_port"

definition 
  allow_all_from_to_port_prot    :: "protocol =>'α::adr net  ⇒ 'α::adr net ⇒
                                'γ::port ⇒ (('α,'β) packet ↦ unit)" where
  "allow_all_from_to_port_prot p src_net dest_net d_port = 
    {pa. dest_protocol pa = p} ◃ allow_all_from_to_port src_net dest_net d_port "

definition 
  deny_all_from_to_port_prot    :: "protocol =>'α::adr net ⇒ 'α::adr net ⇒ 'γ::port ⇒
                               (('α,'β) packet ↦ unit)" where
  "deny_all_from_to_port_prot p src_net dest_net d_port =   
    {pa. dest_protocol pa = p} ◃ deny_all_from_to_port src_net dest_net d_port"

definition 
  allow_from_port_to_prot :: "protocol =>'γ::port ⇒ 'α::adr net ⇒ 'α::adr net ⇒ (('α,'β) packet ↦ unit)"
  where 
    "allow_from_port_to_prot p port src_net dest_net =   
    {pa. dest_protocol pa = p} ◃ allow_from_port_to port src_net dest_net"

definition 
  deny_from_port_to_prot :: "protocol =>'γ::port ⇒ 'α::adr net ⇒ 'α::adr net ⇒ (('α,'β) packet ↦ unit)"
  where 
    "deny_from_port_to_prot p port src_net dest_net =   
    {pa. dest_protocol pa = p} ◃ deny_from_port_to port src_net dest_net"

definition 
  allow_from_to_port_prot :: "protocol =>'γ::port  ⇒ 'α::adr net ⇒ 'α::adr net ⇒ (('α,'β) packet ↦ unit)"
  where 
    "allow_from_to_port_prot p port src_net dest_net =   
  {pa. dest_protocol pa = p} ◃ allow_from_to_port port src_net dest_net"

definition 
  deny_from_to_port_prot :: "protocol =>'γ::port  ⇒ 'α::adr net ⇒ 'α::adr net ⇒ (('α,'β) packet ↦ unit)"
  where 
    "deny_from_to_port_prot p port src_net dest_net =   
    {pa. dest_protocol pa = p} ◃ deny_from_to_port port src_net dest_net"

definition 
  allow_from_ports_to_prot :: "protocol =>'γ::port set ⇒ 'α::adr net ⇒ 'α::adr net ⇒
                          (('α,'β) packet ↦ unit)" where
  "allow_from_ports_to_prot p ports src_net dest_net =   
   {pa. dest_protocol pa = p} ◃ allow_from_ports_to ports src_net dest_net"

definition 
  allow_from_to_ports_prot :: "protocol =>'γ::port set ⇒ 'α::adr net ⇒ 'α::adr net ⇒
                          (('α,'β) packet ↦ unit)" where
  "allow_from_to_ports_prot p ports src_net dest_net =   
    {pa. dest_protocol pa = p} ◃ allow_from_to_ports ports src_net dest_net"

definition 
  deny_from_ports_to_prot :: "protocol =>'γ::port set ⇒ 'α::adr net ⇒ 'α::adr net ⇒
                          (('α,'β) packet ↦ unit)" where
  "deny_from_ports_to_prot p ports src_net dest_net =   
    {pa. dest_protocol pa = p} ◃ deny_from_ports_to ports src_net dest_net"

definition 
  deny_from_to_ports_prot :: "protocol =>'γ::port set ⇒ 'α::adr net ⇒ 'α::adr net ⇒
                          (('α,'β) packet ↦ unit)" where
  "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.› 

lemmas ProtocolCombinatorsCore = 
  allow_all_from_port_prot_def deny_all_from_port_prot_def allow_all_to_port_prot_def
  deny_all_to_port_prot_def allow_all_from_to_port_prot_def
  deny_all_from_to_port_prot_def
  allow_from_ports_to_prot_def allow_from_to_ports_prot_def
  deny_from_ports_to_prot_def deny_from_to_ports_prot_def
  allow_all_from_port_to_prot_def deny_all_from_port_to_prot_def
  allow_from_port_to_prot_def allow_from_to_port_prot_def deny_from_to_port_prot_def
  deny_from_port_to_prot_def 

lemmas ProtocolCombinators = PortCombinators.PortCombinators ProtocolCombinatorsCore

end

(*****************************************************************************
 * Copyright (c) 2005-2010 ETH Zurich, Switzerland
 *               2008-2015 Achim D. Brucker, Germany
 *               2009-2016 Université Paris-Sud, France
 *               2015-2016 The University of Sheffield, UK
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 *
 *     * Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *
 *     * Redistributions in binary form must reproduce the above
 *       copyright notice, this list of conditions and the following
 *       disclaimer in the documentation and/or other materials provided
 *       with the distribution.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 *****************************************************************************)

subsection ‹Ports›
theory Ports
  imports 
    Main
begin

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 ‹Ports› to the simplifier.
›

definition http::int where "http = 80"

lemma http1: "x ≠ 80 ⟹ x ≠ http"
  by (simp add: http_def)

lemma http2: "x ≠ 80 ⟹ http ≠ x"
  by (simp add: http_def)

definition smtp::int where "smtp = 25"

lemma smtp1: "x ≠ 25 ⟹ x ≠ smtp"
  by (simp add: smtp_def)

lemma smtp2: "x ≠ 25 ⟹ smtp ≠ x"
  by (simp add: smtp_def)

definition ftp::int where "ftp = 21"

lemma ftp1: "x ≠ 21 ⟹ x ≠ ftp"
  by (simp add: ftp_def)

lemma ftp2: "x ≠ 21 ⟹ ftp ≠ x"
  by (simp add: ftp_def)

text‹And so on for all desired port numbers.›

lemmas Ports = http1 http2 ftp1 ftp2 smtp1 smtp2

end

(*****************************************************************************
 * Copyright (c) 2005-2010 ETH Zurich, Switzerland
 *               2008-2015 Achim D. Brucker, Germany
 *               2009-2016 Université Paris-Sud, France
 *               2015-2016 The University of Sheffield, UK
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 *
 *     * Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *
 *     * Redistributions in binary form must reproduce the above
 *       copyright notice, this list of conditions and the following
 *       disclaimer in the documentation and/or other materials provided
 *       with the distribution.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (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›
theory 
  PacketFilter
  imports
    NetworkModels
    ProtocolPortCombinators
    Ports
begin 
end

(*****************************************************************************
 * Copyright (c) 2005-2010 ETH Zurich, Switzerland
 *               2008-2015 Achim D. Brucker, Germany
 *               2009-2016 Université Paris-Sud, France
 *               2015-2016 The University of Sheffield, UK
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 *
 *     * Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *
 *     * Redistributions in binary form must reproduce the above
 *       copyright notice, this list of conditions and the following
 *       disclaimer in the documentation and/or other materials provided
 *       with the distribution.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 *****************************************************************************)

subsection‹Network Address Translation›
theory 
  NAT
  imports 
    "../PacketFilter/PacketFilter"
begin


definition src2pool :: "'α set ⇒ ('α::adr,'β) packet ⇒ ('α,'β) packet set" where
  "src2pool t = (λ p. ({(i,s,d,da). (i = id p ∧ s ∈ t ∧ d = dest p ∧ da = content p)}))"

definition src2poolAP where
  "src2poolAP t = A⇩f (src2pool t)"

definition srcNat2pool :: "'α set ⇒ 'α set ⇒ ('α::adr,'β) packet ↦ ('α,'β) packet set" where 
  "srcNat2pool srcs transl = {x. src x ∈ srcs} ◃ (src2poolAP transl)"

definition src2poolPort :: "int set ⇒ (adr⇩i⇩p,'β) packet ⇒ (adr⇩i⇩p,'β) packet set" where
  "src2poolPort t = (λ p. ({(i,(s1,s2),(d1,d2),da). 
          (i = id p ∧ s1 ∈ t ∧ s2 = (snd (src p)) ∧ d1 = (fst (dest p)) ∧ 
                d2 = snd (dest p) ∧ da = content p)}))"

definition src2poolPort_Protocol :: "int set ⇒ (adr⇩i⇩p⇩p,'β) packet ⇒ (adr⇩i⇩p⇩p,'β) packet set" where
  "src2poolPort_Protocol t = (λ p. ({(i,(s1,s2,s3),(d1,d2,d3), da). 
  (i = id p ∧ s1 ∈ t ∧ s2 = (fst (snd (src p))) ∧ s3 = snd (snd (src p)) ∧ 
                   (d1,d2,d3) = dest p ∧ da = content p)}))"

definition srcNat2pool_IntPort :: "address set ⇒ address set ⇒ 
 (adr⇩i⇩p,'β) packet ↦ (adr⇩i⇩p,'β) packet set" where
  "srcNat2pool_IntPort srcs transl = 
      {x. fst (src x) ∈ srcs} ◃ (A⇩f (src2poolPort transl))" 

definition srcNat2pool_IntProtocolPort :: "int set ⇒ int set ⇒ 
 (adr⇩i⇩p⇩p,'β) packet ↦ (adr⇩i⇩p⇩p,'β) packet set" where 
  "srcNat2pool_IntProtocolPort srcs transl =
      {x. (fst ( (src x))) ∈ srcs} ◃ (A⇩f (src2poolPort_Protocol transl))" 

definition srcPat2poolPort_t :: "int set ⇒ (adr⇩i⇩p,'β) packet ⇒ (adr⇩i⇩p,'β) packet set" where
  "srcPat2poolPort_t t = (λ p. ({(i,(s1,s2),(d1,d2),da). 
           (i = id p ∧ s1 ∈ t ∧ d1 = (fst (dest p)) ∧ d2 = snd (dest p)∧ da = content p)}))"

definition srcPat2poolPort_Protocol_t :: "int set ⇒ (adr⇩i⇩p⇩p,'β) packet ⇒ (adr⇩i⇩p⇩p,'β) packet set" where
  "srcPat2poolPort_Protocol_t t = (λ p. ({(i,(s1,s2,s3),(d1,d2,d3),da). 
  (i = id p ∧ s1 ∈ t ∧ s3 = src_protocol p ∧ (d1,d2,d3) = dest p ∧ da = content p)}))"

definition srcPat2pool_IntPort :: "int set ⇒ int set ⇒ (adr⇩i⇩p,'β) packet ↦ 
                                            (adr⇩i⇩p,'β) packet set" where 
  "srcPat2pool_IntPort srcs transl = 
  {x. (fst (src x)) ∈ srcs} ◃ (A⇩f (srcPat2poolPort_t transl))" 

definition srcPat2pool_IntProtocol :: 
  "int set ⇒ int set ⇒ (adr⇩i⇩p⇩p,'β) packet ↦ (adr⇩i⇩p⇩p,'β) packet set" where 

  "srcPat2pool_IntProtocol srcs transl = 
  {x. (fst (src x)) ∈ srcs} ◃ (A⇩f (srcPat2poolPort_Protocol_t transl))" 

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 ∧ 
                               s3 = iudp ∧ a = i110 ∧ aa = X606X3 ∧ b = X607X4 ∧ ba = data} 
                 = {(i, (s1, s2, s3), aba).
                    i = i1 ∧ s1 = i101 ∧ s3 = iudp ∧ (λ ((a,aa,b),ba). a = i110 ∧ aa = X606X3 ∧
                    b = X607X4 ∧ ba = data) aba}"
  by auto

lemma datasimp2: "{(i, (s1, s2, s3), aba).
                    ∀a aa b ba. aba = ((a, aa, b), ba) ⟶ i = i1 ∧ s1 = i132 ∧ s3 = iudp ∧ 
                        s2 = i1 ∧ a = i110 ∧ aa = i4 ∧ b = iudp ∧ ba = data}
                = {(i, (s1, s2, s3), aba).
                       i = i1 ∧ s1 = i132 ∧ s3 = iudp ∧ s2 = i1 ∧ (λ ((a,aa,b),ba). a = i110 ∧ 
                       aa = i4 ∧ b = iudp ∧ ba = data) aba}"
  by auto

lemma datasimp3: "{(i, (s1, s2, s3), aba).
                     ∀ a aa b ba. aba = ((a, aa, b), ba) ⟶ i = i1 ∧ i115 < s1 ∧ s1 < i124 ∧ 
                         s3 = iudp ∧ s2 = ii1 ∧ a = i110 ∧ aa = i3 ∧ b = itcp ∧ ba = data}
                = {(i, (s1, s2, s3), aba).
                         i = i1 ∧ i115 < s1 ∧ s1 < i124 ∧ s3 = iudp ∧ s2 = ii1 ∧ 
                       (λ ((a,aa,b),ba). a = i110 & aa = i3 & b = itcp & ba = data) aba}"
  by auto

lemma datasimp4: "{(i, (s1, s2, s3), aba).
                    ∀a aa b ba. aba = ((a, aa, b), ba) ⟶ i = i1 ∧ s1 = i132 ∧ s3 = iudp ∧ 
                        s2 = ii1 ∧ a = i110 ∧ aa = i7 ∧ b = itcp ∧ ba = data}
                = {(i, (s1, s2, s3), aba).
                        i = i1 ∧ s1 = i132 ∧ s3 = iudp ∧ s2 = ii1 ∧ 
                        (λ ((a,aa,b),ba). a = i110 ∧ aa = i7 ∧ b = itcp ∧ ba = data) aba}"
  by auto

lemma datasimp5: " {(i, (s1, s2, s3), aba).
                     i = i1 ∧ s1 = i101 ∧ s3 = iudp ∧ (λ ((a,aa,b),ba). a = i110 ∧ aa = X606X3 ∧ 
                       b = X607X4 ∧ ba = data) aba}
                 = {(i, (s1, s2, s3), (a,aa,b),ba).
                       i = i1 ∧ s1 = i101 ∧ s3 = iudp ∧  a = i110 ∧ aa = X606X3 ∧ 
                       b = X607X4 ∧ ba = data}"
  by auto

lemma datasimp6: "{(i, (s1, s2, s3), aba).
                     i = i1 ∧ s1 = i132 ∧ s3 = iudp ∧ s2 = i1 ∧ 
                     (λ ((a,aa,b),ba). a = i110 ∧  aa = i4 ∧ b = iudp ∧ ba = data) aba}
                 = {(i, (s1, s2, s3), (a,aa,b),ba).
                       i = i1 ∧ s1 = i132 ∧ s3 = iudp ∧ s2 = i1 ∧ a = i110 ∧ 
                       aa = i4 ∧ b = iudp ∧ ba = data}"
  by auto

lemma datasimp7: "{(i, (s1, s2, s3), aba).
                     i = i1 ∧ i115 < s1 ∧ s1 < i124 ∧ s3 = iudp ∧ s2 = ii1 ∧ 
                     (λ ((a,aa,b),ba). a = i110 ∧ aa = i3 ∧ b = itcp ∧ ba = data) aba} 
                = {(i, (s1, s2, s3), (a,aa,b),ba).
                     i = i1 ∧ i115 < s1 ∧ s1 < i124 ∧ s3 = iudp ∧ s2 = ii1 
                     ∧ a = i110 ∧ aa = i3 ∧ b = itcp ∧ ba = data}"
  by auto

lemma datasimp8: "{(i, (s1, s2, s3), aba). i = i1 ∧ s1 = i132 ∧ s3 = iudp ∧ s2 = ii1 ∧ 
                   (λ ((a,aa,b),ba). a = i110 ∧ aa = i7 ∧ b = itcp ∧ ba = data) aba}
                = {(i, (s1, s2, s3), (a,aa,b),ba). i = i1 ∧ s1 = i132 ∧ s3 = iudp 
                                   ∧ s2 = ii1 ∧  a = i110 ∧ aa = i7 ∧ b = itcp ∧ ba = data}"
  by auto

lemmas datasimps = datasimp datasimp2 datasimp3 datasimp4
                   datasimp5 datasimp6 datasimp7 datasimp8

lemmas NATLemmas = src2pool_def src2poolPort_def
                   src2poolPort_Protocol_def src2poolAP_def srcNat2pool_def
                   srcNat2pool_IntProtocolPort_def srcNat2pool_IntPort_def
                   srcPat2poolPort_t_def srcPat2poolPort_Protocol_t_def
                   srcPat2pool_IntPort_def srcPat2pool_IntProtocol_def
end

(*****************************************************************************
 * Copyright (c) 2005-2010 ETH Zurich, Switzerland
 *               2008-2015 Achim D. Brucker, Germany
 *               2009-2016 Université Paris-Sud, France
 *               2015-2016 The University of Sheffield, UK
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 *
 *     * Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *
 *     * Redistributions in binary form must reproduce the above
 *       copyright notice, this list of conditions and the following
 *       disclaimer in the documentation and/or other materials provided
 *       with the distribution.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 *****************************************************************************)

subsection ‹Policy Normalisation: Core Definitions›
theory
  FWNormalisationCore
imports
  "../PacketFilter/PacketFilter"
begin

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}.

  The normalisation procedure transforms policies into semantically equivalent  ones which are 
  ``easier'' to test. It is organized into nine phases. We impose the following two restrictions 
  on the input policies: 
  \begin{itemize}
  \item Each policy must contain a $\mathtt{DenyAll}$ rule. If this restriction were to be lifted, 
        the $\mathtt{insertDenies}$ phase would have to be adjusted accordingly.
  \item For each pair of networks $n_1$ and $n_2$, the networks are either disjoint or equal. If 
        this restriction were to be lifted, we would need some additional phases before the start 
        of the normalisation procedure presented below. This rule would split single rules into 
        several by splitting up the networks such that they are all pairwise disjoint or equal. 
        Such a transformation is clearly semantics-preserving and the condition would hold after
        these phases.
  \end{itemize}
  As a result, the procedure generates a list of policies, in which:
  \begin{itemize}
  \item each element of the list contains a policy which completely specifies the blocking behavior 
        between two networks, and
  \item there are no shadowed rules.
  \end{itemize}
  This result is desirable since the test case generation for rules between networks $A$ and $B$ 
  is independent of the rules that specify the behavior for traffic flowing between networks $C$ 
  and $D$. Thus, the different segments of the policy can be processed individually. The 
  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‹
  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:›

datatype ('α,'β) Combinators = 
  DenyAll
  | DenyAllFromTo 'α 'α 
  | AllowPortFromTo 'α 'α 'β 
  | Conc "(('α,'β) Combinators)" "(('α,'β) Combinators)" (infixr "⊕" 80)

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‹
  This section defines several functions which are useful later for the combinators, invariants, 
  and proofs. 
›
  
fun srcNet where 
 "srcNet (DenyAllFromTo x y) = x"
|"srcNet (AllowPortFromTo x y p) = x"
|"srcNet DenyAll = undefined"
|"srcNet (v ⊕ va) = undefined" 

fun destNet where 
 "destNet (DenyAllFromTo x y) = y"
|"destNet (AllowPortFromTo x y p) = y"
|"destNet DenyAll = undefined"
|"destNet (v ⊕ va) = undefined" 

fun srcnets where
 "srcnets DenyAll = [] " 
|"srcnets (DenyAllFromTo x y) = [x] " 
|"srcnets (AllowPortFromTo x y p) = [x] " 
|"(srcnets (x ⊕ y)) = (srcnets x)@(srcnets y)"

fun destnets where
 "destnets DenyAll = [] " 
|"destnets (DenyAllFromTo x y) = [y] " 
|"destnets (AllowPortFromTo x y p) = [y] "
|"(destnets (x ⊕ y)) = (destnets x)@(destnets y)"

fun (sequential) net_list_aux where
 "net_list_aux [] = []"
|"net_list_aux (DenyAll#xs) = net_list_aux xs"
|"net_list_aux ((DenyAllFromTo x y)#xs) = x#y#(net_list_aux xs)"
|"net_list_aux ((AllowPortFromTo x y p)#xs) = x#y#(net_list_aux xs)"
|"net_list_aux ((x⊕y)#xs) = (net_list_aux [x])@(net_list_aux [y])@(net_list_aux xs)"

fun net_list where "net_list p = remdups (net_list_aux p)"

definition bothNets where "bothNets x = (zip (srcnets x) (destnets x))"

fun (sequential) normBothNets where 
 "normBothNets ((a,b)#xs) = (if ((b,a) ∈ set xs) ∨ (a,b) ∈ set (xs) 
                            then (normBothNets xs)
                            else (a,b)#(normBothNets xs))"
|"normBothNets x = x" 

fun makeSets where 
 "makeSets ((a,b)#xs) = ({a,b}#(makeSets xs))"
|"makeSets [] = []"

fun bothNet where
 "bothNet DenyAll = {}"
|"bothNet (DenyAllFromTo a b) = {a,b}"
|"bothNet (AllowPortFromTo a b p) = {a,b}"
|"bothNet (v ⊕ va) = undefined "

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 
  "Nets_List x = makeSets (normBothNets (bothNets x))"

fun (sequential) first_srcNet where 
  "first_srcNet (x⊕y) = first_srcNet x"
| "first_srcNet x = srcNet x"

fun (sequential) first_destNet where 
  "first_destNet (x⊕y) = first_destNet x"
| "first_destNet x = destNet x"

fun (sequential) first_bothNet where
 "first_bothNet (x⊕y) = first_bothNet x"
|"first_bothNet x = bothNet x"

fun (sequential) in_list where 
 "in_list DenyAll l = True"
|"in_list x l = (bothNet x ∈ set l)"

fun all_in_list where 
 "all_in_list [] l = True"
|"all_in_list (x#xs) l = (in_list x l ∧ all_in_list xs l)" 

fun (sequential) member where
 "member a (x⊕xs) = ((member a x) ∨ (member a xs))"
|"member a x = (a = x)"

fun sdnets where
  "sdnets DenyAll = {}"
| "sdnets (DenyAllFromTo a b) = {(a,b)}"
| "sdnets (AllowPortFromTo a b c) = {(a,b)}"
| "sdnets (a ⊕ b) = sdnets a ∪ sdnets b"

definition packet_Nets  where "packet_Nets x a b = ((src x ⊏ a ∧ dest x ⊏ b) ∨
                                                    (src x ⊏ b ∧ dest x ⊏ a))"

definition subnetsOfAdr where "subnetsOfAdr a = {x. a ⊏ x}"

definition fst_set where "fst_set s = {a. ∃ b. (a,b) ∈ s}"

definition snd_set where "snd_set s = {a. ∃ b. (b,a) ∈ s}"

fun memberP where
 "memberP r (x#xs) = (member r x ∨ memberP r xs)"
|"memberP r [] = False"

fun firstList where 
 "firstList (x#xs) = (first_bothNet x)"
|"firstList [] = {}"

subsubsection‹Invariants›

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›
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.›
definition netsDistinct where "netsDistinct a b = (¬ (∃ x. x ⊏ a ∧ x ⊏ b))"

definition twoNetsDistinct where
  "twoNetsDistinct a b c d = (netsDistinct a c ∨ netsDistinct b d)"

definition allNetsDistinct where 
  "allNetsDistinct p = (∀ a b. (a ≠ b ∧ a ∈ set (net_list p) ∧
                        b ∈ set (net_list p)) ⟶ netsDistinct a b)"

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.›
fun singleCombinators where 
"singleCombinators [] = True"
|"singleCombinators ((x⊕y)#xs) = False"
|"singleCombinators (x#xs) = singleCombinators xs"

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.›
fun OnlyTwoNets where 
 "OnlyTwoNets (DenyAll#xs) = OnlyTwoNets xs"
|"OnlyTwoNets (x#xs) = (onlyTwoNets x ∧ OnlyTwoNets xs)"
|"OnlyTwoNets [] = True"

fun noDenyAll where
 "noDenyAll (x#xs) = ((¬ member DenyAll x) ∧ noDenyAll xs)"
|"noDenyAll [] = True"

fun noDenyAll1 where 
  "noDenyAll1 (DenyAll#xs) = noDenyAll xs"
| "noDenyAll1 xs = noDenyAll xs"

fun separated where
  "separated (x#xs) = ((∀ s. s ∈ set xs ⟶ disjSD_2 x s) ∧ separated xs)"
| "separated [] = True"

fun NetsCollected where 
  "NetsCollected (x#xs) = (((first_bothNet x ≠ firstList xs) ⟶
          (∀a∈set xs. first_bothNet x ≠ first_bothNet a)) ∧ NetsCollected (xs))"
| "NetsCollected [] = True"

fun NetsCollected2 where
 "NetsCollected2 (x#xs) = (xs = [] ∨ (first_bothNet x ≠ firstList xs ∧
                           NetsCollected2 xs))"
|"NetsCollected2 [] = True"

subsubsection‹Transformations›

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
 "policy2list (x ⊕ y) = (concat [(policy2list x),(policy2list y)])"
|"policy2list x = [x]"

fun list2FWpolicy::"(('α, 'β) Combinators) list ⇒
                  (('α, 'β) Combinators)" where
 "list2FWpolicy [] = undefined "
|"list2FWpolicy (x#[]) = x"
|"list2FWpolicy (x#y) = x ⊕ (list2FWpolicy y)"

text‹Remove all the rules appearing before a DenyAll. There are two alternative versions.›

fun removeShadowRules1 where
  "removeShadowRules1 (x#xs) = (if (DenyAll ∈ set xs) 
                                then ((removeShadowRules1 xs))
                                else x#xs)"
| "removeShadowRules1 [] = []"

fun  removeShadowRules1_alternative_rev where
  "removeShadowRules1_alternative_rev [] = []"
| "removeShadowRules1_alternative_rev (DenyAll#xs) = [DenyAll]"
| "removeShadowRules1_alternative_rev [x] = [x]"
| "removeShadowRules1_alternative_rev (x#xs)=
                 x#(removeShadowRules1_alternative_rev xs)"

definition removeShadowRules1_alternative where
   "removeShadowRules1_alternative p =
                         rev (removeShadowRules1_alternative_rev (rev p))"

text‹
  Remove all the rules which allow a port, but are shadowed by a deny between these subnets.
›

fun removeShadowRules2::  "(('α, 'β) Combinators) list ⇒
                          (('α, 'β) Combinators) list"
where
  "(removeShadowRules2 ((AllowPortFromTo x y p)#z)) = 
        (if (((DenyAllFromTo x y) ∈ set z)) 
         then ((removeShadowRules2 z))
         else (((AllowPortFromTo x y p)#(removeShadowRules2 z))))"
| "removeShadowRules2 (x#y) = x#(removeShadowRules2 y)"
| "removeShadowRules2 [] = []"

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 ⇒ 
                (('α) set) list ⇒ bool" 
where
 "smaller DenyAll x l = True" 
| "smaller x DenyAll l = False"
| "smaller x y l = 
 ((x = y) ∨         (if (bothNet x) = (bothNet y) then 
                       (case y of (DenyAllFromTo a b) ⇒ (x = DenyAllFromTo b a)  
                            | _ ⇒  True)
                    else
                        (position (bothNet x) l <= position (bothNet y) l)))"

text‹We provide two different sorting algorithms: Quick Sort (qsort) and Insertion Sort (sort)›

fun qsort where
  "qsort [] l     = []"
| "qsort (x#xs) l = (qsort [y←xs. ¬ (smaller x y l)] l) @ [x] @ (qsort [y←xs. smaller x y l] l)"

lemma qsort_permutes:
  "set (qsort xs l) = set xs"
  apply (induct "xs" "l" rule: qsort.induct)
  by (auto)

lemma set_qsort [simp]: "set (qsort xs l)  = set xs" 
  by (simp add: qsort_permutes)
    
fun insort where
	  "insort a [] l = [a]"
	| "insort a (x#xs) l = (if (smaller a x l) then a#x#xs else x#(insort a xs l))"

fun sort where
  "sort [] l = []"
| "sort (x#xs) l = insort x (sort xs l) l"

fun sorted  where
  "sorted [] l = True"
| "sorted [x] l = True"
| "sorted (x#y#zs) l = (smaller x y l ∧ sorted (y#zs) l)"

fun separate where
 "separate (DenyAll#x) = DenyAll#(separate x)"
| "separate (x#y#z) = (if (first_bothNet x = first_bothNet y) 
                   then (separate ((x⊕y)#z))
                   else (x#(separate(y#z))))"
|"separate x = x"                

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))
                    | _  ⇒ (DenyAllFromTo (first_srcNet x) (first_destNet x) ⊕ 
                       (DenyAllFromTo (first_destNet x) (first_srcNet x)) ⊕ x)#
                                (insertDenies xs))"
| "insertDenies [] = []"

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
  "removeDuplicates (x⊕xs) = (if member x xs then (removeDuplicates xs)
                              else x⊕(removeDuplicates xs))"
| "removeDuplicates x = x"

fun removeAllDuplicates where 
 "removeAllDuplicates (x#xs) = ((removeDuplicates (x))#(removeAllDuplicates xs))"
|"removeAllDuplicates x = x"

text ‹Insert a DenyAll at the beginning of a policy.›
fun insertDeny where 
 "insertDeny (DenyAll#xs) = DenyAll#xs"
|"insertDeny xs = DenyAll#xs"


definition "sort' p l = sort l p"
definition "qsort' p l = qsort l p"

declare dom_eq_empty_conv [simp del]

fun list2policyR::"(('α, 'β) Combinators) list ⇒
                   (('α, 'β) Combinators)" where
 "list2policyR (x#[]) = x"
|"list2policyR (x#y) = (list2policyR y) ⊕ x"
|"list2policyR [] = undefined "


text‹
  We provide the definitions for two address representations. 
›


subsubsection‹IntPort›

fun C :: "(adr⇩i⇩p net, port) Combinators ⇒ (adr⇩i⇩p,DummyContent) packet ↦ unit"
where
" C DenyAll = deny_all" 
|"C (DenyAllFromTo x y) = deny_all_from_to x y"
|"C (AllowPortFromTo x y p) = allow_from_to_port p x y"
|"C  (x ⊕ y) =  C x ++ C y"

fun CRotate :: "(adr⇩i⇩p net, port) Combinators ⇒ (adr⇩i⇩p,DummyContent) packet ↦ unit"
where
" CRotate DenyAll = C DenyAll" 
|"CRotate (DenyAllFromTo x y) = C (DenyAllFromTo x y)"
|"CRotate (AllowPortFromTo x y p) = C (AllowPortFromTo x y p)"
|"CRotate (x ⊕ y) = ((CRotate y) ++ ((CRotate x)))"

fun rotatePolicy where
  "rotatePolicy DenyAll = DenyAll" 
| "rotatePolicy (DenyAllFromTo a b) = DenyAllFromTo a b"
| "rotatePolicy (AllowPortFromTo a b p) = AllowPortFromTo a b p"
| "rotatePolicy (a⊕b) = (rotatePolicy b) ⊕ (rotatePolicy a)"

lemma check: "rev (policy2list (rotatePolicy p)) = policy2list p"
  apply (induct "p")
  by (simp_all) 


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‹
  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⇩i⇩p net,port) Combinators) list ⇒ bool" where
  "wellformed_policy3 [] = True"
| "wellformed_policy3 ((AllowPortFromTo a b p)#xs) = ((∀ r. r ∈ set xs ⟶
      dom (C r) ∩ dom (C (AllowPortFromTo a b p)) = {}) ∧ wellformed_policy3 xs)"
| "wellformed_policy3 (x#xs) = wellformed_policy3 xs"


definition 
  "normalize' p  = (removeAllDuplicates o insertDenies o separate o
                   (sort' (Nets_List p))  o removeShadowRules2 o remdups o
                   (rm_MT_rules C) o insertDeny o removeShadowRules1 o
                   policy2list) p"

definition 
  "normalizeQ' p  = (removeAllDuplicates o insertDenies o separate o
                   (qsort' (Nets_List p))  o removeShadowRules2 o remdups o
                   (rm_MT_rules C) o insertDeny o removeShadowRules1 o
                   policy2list) p"

definition normalize :: 
  "(adr⇩i⇩p net, port) Combinators ⇒ 
   (adr⇩i⇩p net, port) Combinators list" 
where
   "normalize p = (removeAllDuplicates (insertDenies (separate (sort
                   (removeShadowRules2 (remdups ((rm_MT_rules C) (insertDeny
                  (removeShadowRules1 (policy2list p)))))) ((Nets_List p))))))"

definition
   "normalize_manual_order p l = removeAllDuplicates (insertDenies (separate
    (sort (removeShadowRules2 (remdups ((rm_MT_rules C) (insertDeny
    (removeShadowRules1 (policy2list p)))))) ((l)))))"

definition normalizeQ :: 
  "(adr⇩i⇩p net, port) Combinators ⇒ 
   (adr⇩i⇩p net, port) Combinators list" 
where
   "normalizeQ p = (removeAllDuplicates (insertDenies (separate (qsort
                   (removeShadowRules2 (remdups ((rm_MT_rules C) (insertDeny
                  (removeShadowRules1 (policy2list p)))))) ((Nets_List p))))))"

definition
   "normalize_manual_orderQ p l = removeAllDuplicates (insertDenies (separate
    (qsort (removeShadowRules2 (remdups ((rm_MT_rules C) (insertDeny
    (removeShadowRules1 (policy2list p)))))) ((l)))))"

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›

fun Cp :: "(adr⇩i⇩p⇩p net, protocol × port) Combinators ⇒ 
          (adr⇩i⇩p⇩p,DummyContent) packet ↦ unit"
where
 " Cp DenyAll = deny_all"  
|"Cp (DenyAllFromTo x y) = deny_all_from_to x y"
|"Cp (AllowPortFromTo x y p) = allow_from_to_port_prot (fst p) (snd p) x y"
|"Cp  (x ⊕ y) =  Cp x ++ Cp y"


fun Dp :: "(adr⇩i⇩p⇩p net, protocol × port) Combinators ⇒ 
          (adr⇩i⇩p⇩p,DummyContent) packet ↦ unit"
where
" Dp DenyAll = Cp DenyAll" 
|"Dp (DenyAllFromTo x y) = Cp (DenyAllFromTo x y)"
|"Dp (AllowPortFromTo x y p) = Cp (AllowPortFromTo x y p)"
|"Dp  (x ⊕ y) =  Cp (y ⊕ x)"

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‹
  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⇩i⇩p⇩p net, protocol × port) Combinators) list ⇒ bool" where
  "wellformed_policy3Pr [] = True"
| "wellformed_policy3Pr ((AllowPortFromTo a b p)#xs) = ((∀ r. r ∈ set xs ⟶
      dom (Cp r) ∩ dom (Cp (AllowPortFromTo a b p)) = {}) ∧ wellformed_policy3Pr xs)"
| "wellformed_policy3Pr (x#xs) = wellformed_policy3Pr xs"

definition 
 normalizePr' :: "(adr⇩i⇩p⇩p net, protocol × port) Combinators
  ⇒ (adr⇩i⇩p⇩p net, protocol × port) Combinators list" where 
 "normalizePr' p = (removeAllDuplicates o insertDenies o separate o
                   (sort' (Nets_List p))  o removeShadowRules2 o remdups o
                   (rm_MT_rules Cp) o insertDeny o removeShadowRules1 o
                   policy2list) p"

definition normalizePr :: 
"(adr⇩i⇩p⇩p net, protocol × port) Combinators
  ⇒ (adr⇩i⇩p⇩p net, protocol × port) Combinators list" where
   "normalizePr p = (removeAllDuplicates (insertDenies (separate (sort
                   (removeShadowRules2 (remdups ((rm_MT_rules Cp) (insertDeny
                  (removeShadowRules1 (policy2list p)))))) ((Nets_List p))))))"

definition
   "normalize_manual_orderPr p l = removeAllDuplicates (insertDenies (separate
    (sort (removeShadowRules2 (remdups ((rm_MT_rules Cp) (insertDeny
    (removeShadowRules1 (policy2list p)))))) ((l)))))"


definition 
 normalizePrQ' :: "(adr⇩i⇩p⇩p net, protocol × port) Combinators
  ⇒ (adr⇩i⇩p⇩p net, protocol × port) Combinators list" where 
 "normalizePrQ' p = (removeAllDuplicates o insertDenies o separate o
                   (qsort' (Nets_List p))  o removeShadowRules2 o remdups o
                   (rm_MT_rules Cp) o insertDeny o removeShadowRules1 o
                   policy2list) p"

definition normalizePrQ :: 
"(adr⇩i⇩p⇩p net, protocol × port) Combinators
  ⇒ (adr⇩i⇩p⇩p net, protocol × port) Combinators list" where
   "normalizePrQ p = (removeAllDuplicates (insertDenies (separate (qsort
                   (removeShadowRules2 (remdups ((rm_MT_rules Cp) (insertDeny
                  (removeShadowRules1 (policy2list p)))))) ((Nets_List p))))))"

definition
   "normalize_manual_orderPrQ p l = removeAllDuplicates (insertDenies (separate
    (qsort (removeShadowRules2 (remdups ((rm_MT_rules Cp) (insertDeny
    (removeShadowRules1 (policy2list p)))))) ((l)))))"

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‹
  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))  
                     (snd(normBothNets (bothNets p)!n)) ⟶ 
    FUT x = Cp ((normalizePr p)!Suc n) x)"

declare Cp.simps [simp del]

lemmas PLemmas = C.simps Cp.simps dom_def PolicyCombinators.PolicyCombinators
                 PortCombinators.PortCombinatorsCore aux
                 ProtocolPortCombinators.ProtocolCombinatorsCore src_def dest_def in_subnet_def
                 adr⇩i⇩p⇩pLemmas adr⇩i⇩p⇩pLemmas

lemma aux: "⟦x ≠ a; y≠b; (x ≠ y ∧ x ≠ b) ∨  (a ≠ b ∧ a ≠ y)⟧ ⟹ {x,a} ≠ {y,b}"
  by (auto)

lemma aux2: "{a,b} = {b,a}"
  by auto
end