Theory FTP

(*****************************************************************************
 * 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 ‹The File Transfer Protocol (ftp)›
theory 
  FTP
  imports 
    StatefulCore 
begin

subsubsection‹The protocol syntax›
text‹
  The File Transfer Protocol FTP is a well known example of a protocol which uses dynamic ports and
  is therefore a natural choice to use as an example for our model. 

  We model only a simplified version of the FTP protocol over IntegerPort addresses, still 
  containing all messages that matter for our purposes. It consists of the following four messages:
  \begin{enumerate} 
    \item ‹init›: The client contacts the server indicating
          his wish to get some data.
    \item ‹ftp_port_request p›: The client, usually after having
          received an acknowledgement of the server, indicates a port
          number on which he wants to receive the data.
    \item ‹ftp_ftp_data›: The server sends the requested data over
          the new channel. There might be an arbitrary number of such
          messages, including zero.
      \item ‹ftp_close›: The client closes the connection. The
          dynamic port gets closed again.
  \end{enumerate}

  The content field of a packet therefore now consists of either one of those four messages or a 
  default one.  
›

datatype  msg = ftp_init  | ftp_port_request port | ftp_data | ftp_close | ftp_other

text‹
  We now also make use of the ID field of a packet. It is used as session ID and we make the 
  assumption that they are all unique among different protocol runs.

  At first, we need some predicates which check if a packet is a specific FTP message and has the 
  correct session ID. 
›

definition
  is_init :: "id ⇒ (adrip, msg)packet ⇒ bool" where 
  "is_init = (λ i p. (id p = i ∧ content p = ftp_init))"

definition
  is_ftp_port_request :: "id  ⇒ port ⇒(adrip, msg) packet ⇒ bool" where
  "is_ftp_port_request = (λ i port p. (id p = i ∧ content p = ftp_port_request port))" 

definition
  is_ftp_data :: "id ⇒ (adrip, msg) packet ⇒ bool" where
  "is_ftp_data = (λ i p. (id p = i ∧ content p = ftp_data))"

definition
  is_ftp_close :: "id ⇒ (adrip, msg) packet ⇒ bool" where
  "is_ftp_close = (λ i p.  (id p = i ∧ content p = ftp_close))"

definition 
  port_open :: "(adrip, msg) history ⇒ id ⇒ port ⇒ bool" where
  "port_open = (λ L a p. (not_before (is_ftp_close a) (is_ftp_port_request a p) L))"

definition
  is_ftp_other :: "id ⇒ (adrip, msg ) packet ⇒ bool" where 
  "is_ftp_other = (λ i p. (id p = i ∧ content p = ftp_other))"

fun are_ftp_other where
  "are_ftp_other i (x#xs) = (is_ftp_other i x ∧ are_ftp_other i xs)"
  |"are_ftp_other i [] = True"

subsubsection‹The protocol policy specification›
text‹
  We now have to model the respective state transitions. It is important to note that state 
  transitions themselves allow all packets which are allowed by the policy, not only those which 
  are allowed by the protocol. Their only task is to change the policy. As an alternative, we could 
  have decided that they only allow packets which follow the protocol (e.g. come on the correct 
  ports), but this should in our view rather be reflected in the policy itself.

  Of course, not every message changes the policy. In such cases, we do not have to model different 
  cases, one is enough. In our example, only messages 2 and 4 need special transitions. The default 
  says that if the policy accepts the packet, it is added to the history, otherwise it is simply 
  dropped. The policy remains the same in both cases.  
›

fun last_opened_port where
  "last_opened_port i ((j,s,d,ftp_port_request p)#xs) = (if i=j then p else last_opened_port i xs)"
| "last_opened_port i (x#xs) = last_opened_port i xs"
| "last_opened_port x [] = undefined"

fun FTP_STA :: "((adrip,msg) history, adrip, msg) FWStateTransition"
  where 
 (* FTP_PORT_REQUEST *)
   "FTP_STA ((i,s,d,ftp_port_request pr), (log, pol)) =
       (if before(Not o is_ftp_close i)(is_init i) log ∧
           dest_port (i,s,d,ftp_port_request pr) = (21::port) 
        then Some (((i,s,d,ftp_port_request pr)#log, 
                   (allow_from_to_port pr (subnet_of d) (subnet_of s)) ⨁ pol))
        else Some (((i,s,d,ftp_port_request pr)#log,pol)))"
 (* FTP_PORT_CLOSURE *) 
  |"FTP_STA ((i,s,d,ftp_close), (log,pol)) = 
       (if   (∃ p. port_open log i p) ∧ dest_port (i,s,d,ftp_close) = (21::port) 
        then Some ((i,s,d,ftp_close)#log, 
                   deny_from_to_port (last_opened_port i log) (subnet_of d)(subnet_of s) ⨁ pol)
       else  Some (((i,s,d,ftp_close)#log, pol)))"

 (* DEFAULT *)
  |"FTP_STA (p, s) = Some (p#(fst s),snd s)"


fun    FTP_STD :: "((adrip,msg) history, adrip, msg) FWStateTransition"
  where "FTP_STD (p,s) = Some s" 

definition TRPolicy ::"    (adrip,msg)packet × (adrip,msg)history × ((adrip,msg)packet ↦ unit)
                        ↦ (unit             × (adrip,msg)history × ((adrip,msg)packet ↦ unit))"
  where     "TRPolicy = ((FTP_STA,FTP_STD) ⨂∇ applyPolicy) o (λ(x,(y,z)).((x,z),(x,(y,z))))"

definition TRPolicyMon
  where     "TRPolicyMon = policy2MON(TRPolicy)"

text‹If required to contain the policy in the output›
definition TRPolicyMon' 
  where     "TRPolicyMon' = policy2MON (((λ(x,y,z). (z,(y,z))) o_f  TRPolicy ))"

text‹
  Now we specify our test scenario in more detail. We could test:
  \begin{itemize}
    \item one correct FTP-Protocol run,
    \item several runs after another,
    \item several runs interleaved,
    \item an illegal protocol run, or
    \item several illegal protocol runs.
  \end{itemize}

  We only do the the simplest case here: one correct protocol run.
›

text‹
  There are four different states which are modelled as a datatype.
›
datatype ftp_states = S0 | S1 | S2 | S3

text‹
  The following constant is ‹True› for all sets which are correct FTP runs for a given 
  source and destination address, ID, and data-port number.  
›


fun
  is_ftp :: "ftp_states ⇒ adrip  ⇒ adrip ⇒ id ⇒ port ⇒
            (adrip,msg) history ⇒ bool"
  where
    "is_ftp H c s i p [] = (H=S3)"
  |"is_ftp H c s i p (x#InL) = (snd s = 21  ∧((λ (id,sr,de,co). (((id = i ∧ (
   (H=ftp_states.S2 ∧ sr = c ∧ de = s ∧ co = ftp_init ∧ is_ftp S3 c s i p InL) ∨ 
   (H=ftp_states.S1 ∧ sr = c ∧ de = s ∧ co = ftp_port_request p ∧  is_ftp S2 c s i p InL) ∨ 
   (H=ftp_states.S1 ∧ sr = s ∧ de = (fst c,p) ∧ co= ftp_data ∧ is_ftp S1 c s i p InL) ∨ 
   (H=ftp_states.S0 ∧ sr = c ∧ de = s ∧ co = ftp_close  ∧ is_ftp S1 c s i p InL) ))))) x))"



definition  is_single_ftp_run :: "adrip src ⇒ adrip dest ⇒ id ⇒ port  ⇒ (adrip,msg) history set" 
  where      "is_single_ftp_run s d i p = {x. (is_ftp S0 s d i p x)}"

text‹
  The following constant then returns a set of all the historys which denote such a normal 
  behaviour FTP run, again for a given source and destination address, ID, and data-port. 

  The following definition returns the set of all possible interleaving of two correct FTP protocol 
  runs. 
›
definition 
  ftp_2_interleaved :: "adrip src ⇒ adrip dest ⇒ id ⇒ port  ⇒
               adrip src ⇒ adrip dest ⇒ id ⇒ port  ⇒
            (adrip,msg) history set" where
  "ftp_2_interleaved s1 d1 i1 p1 s2 d2 i2 p2 = 
      {x. (is_ftp S0 s1 d1 i1 p1 (packet_with_id x i1)) ∧
          (is_ftp S0 s2 d2 i2 p2 (packet_with_id x i2))}"

lemma subnetOf_lemma: "(a::int) ≠ (c::int) ⟹ ∀x∈subnet_of (a, b::port). (c, d) ∉ x"
  by (rule ballI, simp add: subnet_of_int_def)

lemma subnetOf_lemma2: " ∀x∈subnet_of (a::int, b::port). (a, b) ∈  x"
  by (rule ballI, simp add: subnet_of_int_def)

lemma subnetOf_lemma3: "(∃x. x ∈ subnet_of (a::int, b::port))"
  by (rule exI,  simp add: subnet_of_int_def)

lemma subnetOf_lemma4: "∃x∈subnet_of (a::int, b::port). (a, c::port) ∈ x"
  by (rule bexI, simp_all add: subnet_of_int_def)

lemma port_open_lemma: "¬ (Ex (port_open [] (x::port)))"
  by (simp add: port_open_def)

lemmas FTPLemmas =  TRPolicy_def applyPolicy_def policy2MON_def 
                    Let_def in_subnet_def src_def
                    dest_def  subnet_of_int_def 
                    is_init_def p_accept_def port_open_def is_ftp_data_def is_ftp_close_def 
                    is_ftp_port_request_def content_def PortCombinators
                    exI subnetOf_lemma subnetOf_lemma2 subnetOf_lemma3 subnetOf_lemma4 
                    NetworkCore.id_def adripLemmas port_open_lemma
                    bind_SE_def unit_SE_def valid_SE_def
end