(*****************************************************************************
 * 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_ip,'β) packet → (adr_ip,'β) 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_ipp,'β) packet → (adr_ipp,'β) 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_ip,'β) packet ↦ (adr_ip,'β) packet set" where
  "srcNat2pool_IntPort srcs transl =
      {x. fst (src x) ∈ srcs} ◃ (A_f (src2poolPort transl))" 

definition srcNat2pool_IntProtocolPort :: "int set → int set →
 (adr_ipp,'β) packet ↦ (adr_ipp,'β) packet set" where 
  "srcNat2pool_IntProtocolPort srcs transl =
      {x. (fst ( (src x))) ∈ srcs} ◃ (A_f (src2poolPort_Protocol transl))" 

definition srcPat2poolPort_t :: "int set → (adr_ip,'β) packet → (adr_ip,'β) 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_ipp,'β) packet → (adr_ipp,'β) 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_ip,'β) packet ↦
                                            (adr_ip,'β) 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_ipp,'β) packet ↦ (adr_ipp,'β) 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