Quelle  Analysis.thy

(*****************************************************************************
 * HOL-TestGen --- theorem-prover based test case generation
 *                 http://www.brucker.ch/projects/hol-testgen/
 *                                                                            
 * UPF
 * This file is part of HOL-TestGen.
 *
 * Copyright (c) 2005-2012 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.
 ******************************************************************************)


section‹Properties on Policies›
theory 
  Analysis
  imports
    ParallelComposition
    SeqComposition
begin

text ‹
 In this theory, several standard policy properties are paraphrased in UPF terms.
 ›

subsection‹Basic Properties›

subsubsection‹A Policy Has no Gaps›

definition gap_free :: "('a ↦ 'b) ==> bool" 
where     "gap_free p = (dom p = UNIV)"

subsubsection‹Comparing Policies›
text ‹Policy p is more defined than q:›
definition more_defined :: "('a ↦ 'b) ==>('a ↦ 'b) ==>bool" 
where     "more_defined p q = (dom q ⊆ dom p)"


definition strictly_more_defined :: "('a ↦ 'b) ==>('a ↦ 'b) ==>bool" 
where     "strictly_more_defined p q = (dom q ⊂ dom p)"

lemma strictly_more_vs_more: "strictly_more_defined p q ==> more_defined p q"
  unfolding more_defined_def strictly_more_defined_def
  by auto

text‹Policy p is more permissive than q:›
definition more_permissive :: "('a ↦ 'b) ==> ('a ↦ 'b) ==> bool"  (infixl ‹⊑_A› 60)
where " p ⊑_A q = (∀ x. (case q x of ⌊allow y⌋ ==> (∃ z. (p x = ⌊allow z⌋))
                                   | ⌊deny y⌋ ==> True
                                   | ⊥ ==> True))" 


lemma more_permissive_refl : "p ⊑_A p "
  unfolding more_permissive_def
  by(auto split : option.split decision.split)
    
lemma more_permissive_trans : "p ⊑_A p' ==> p' ⊑_A p'' ==> p ⊑_A p''"
  unfolding more_permissive_def
  apply(auto split : option.split decision.split)
  subgoal for x y
    apply(erule_tac x = x and 
        P = "λx. case p'' x of ⊥ ==> True
                                     | ⌊allow y⌋ ==> ∃z. p' x = ⌊allow z⌋
                                     | ⌊deny y⌋ ==> True" in allE)
    apply(simp, elim exE)
    by(erule_tac x = x in allE, simp)
  done 

text‹Policy p is more rejective than q:›
definition more_rejective :: "('a ↦ 'b) ==> ('a ↦ 'b) ==> bool" (infixl ‹⊑_D› 60)
  where " p ⊑_D q = (∀ x. (case q x of ⌊deny y⌋ ==> (∃ z. (p x = ⌊deny z⌋))
                                  | ⌊allow y⌋ ==> True
                                  | ⊥ ==> True))" 
    
    
lemma more_rejective_trans : "p ⊑_D p' ==> p' ⊑_D p'' ==> p ⊑_D p''"
  unfolding more_rejective_def
  apply(auto split : option.split decision.split)
  subgoal for x y
    apply(erule_tac x = x and 
        P = "λx. case p'' x of ⊥ ==> True
                                     | ⌊allow y⌋ ==> True
                                     | ⌊deny y⌋ ==> ∃z. p' x = ⌊deny z⌋" in allE)
    apply(simp, elim exE)
    by(erule_tac x = x in allE, simp)
  done


lemma more_rejective_refl : "p ⊑_D p "
  unfolding more_rejective_def
  by(auto split : option.split decision.split)
    
    
lemma "A_f f ⊑_A p"
  unfolding more_permissive_def allow_all_fun_def allow_pfun_def 
  by(auto split: option.split decision.split)
    
lemma "A_I ⊑_A p"
  unfolding more_permissive_def allow_all_fun_def allow_pfun_def allow_all_id_def
  by(auto split: option.split decision.split)
    
subsection‹Combined Data-Policy Refinement›
  
definition policy_refinement :: 
  "('a ↦ 'b) ==> ('a' ==> 'a) ==>('b' ==> 'b) ==> ('a' ↦ 'b') ==> bool" 
  (‹_ ⊑_, _› [50,50,50,50]50)
  where     "p ⊑_a,b q ≡
              (∀ a. case p a of
                      ⊥ ==> True
                    | ⌊allow y⌋ ==> (∀ a'∈{x. abs_a x=a}.
                                     ∃ b'. q a' = ⌊allow b'⌋
                                            ∧ abs_b b' = y)
                    | ⌊deny y⌋ ==> (∀ a'∈{x. abs_a x=a}.
                                     ∃ b'. q a' = ⌊deny b'⌋
                                            ∧ abs_b b' = y))"                                     
    
theorem polref_refl: "p ⊑_, p"
  unfolding policy_refinement_def
  by(auto split: option.split decision.split)
    
theorem polref_trans: 
  assumes A: "p ⊑_, p'"
    and     B: "p' ⊑_',' p''"
  shows   "p ⊑ _{o f', o g'} p''"
  apply(insert A B)
  unfolding policy_refinement_def 
  apply(auto split: option.split decision.split simp: o_def)[1]
  subgoal for a a'
    apply(erule_tac x="f (f' a')" in allE, simp)[1]
    apply(erule_tac x="f' a'" in allE, auto)[1]
    apply(erule_tac x=" (f' a')" in allE, auto)[1]
    done 
  subgoal for a a'
    apply(erule_tac x="f (f' a')" in allE, simp)[1]
    apply(erule_tac x="f' a'" in allE, auto)[1]
    apply(erule_tac x=" (f' a')" in allE, auto)[1]
    done
  done 

subsection ‹Equivalence of Policies›
subsubsection‹Equivalence over domain D›
  
definition p_eq_dom :: "('a ↦ 'b) ==> 'a set ==> ('a ↦ 'b) ==>bool" (‹_ ≈ _› [60,60,60]60)
  where     "p ≈ q = (∀x∈D. p x = q x)"
    
text‹p and q have no conflicts›
definition no_conflicts :: "('a ↦ 'b) ==>('a ↦ 'b) ==>bool" where
  "no_conflicts p q = (dom p = dom q ∧ (∀x∈(dom p).
    (case p x of ⌊allow y⌋ ==> (∃z. q x = ⌊allow z⌋)
               | ⌊deny y⌋ ==> (∃z. q x = ⌊deny z⌋))))"
  
lemma policy_eq:
  assumes p_over_qA: "p ⊑_A q "
    and  q_over_pA:    "q ⊑_A p" 
    and  p_over_qD:    "q ⊑_D p" 
    and  q_over_pD:    "p ⊑_D q" 
    and  dom_eq:       "dom p = dom q"
  shows                "no_conflicts p q"
  apply (insert p_over_qA q_over_pA p_over_qD q_over_pD dom_eq)
  apply (simp add:  no_conflicts_def more_permissive_def more_rejective_def
      split: option.splits decision.splits)
  apply (safe)
    apply (metis domI domIff dom_eq)
   apply (metis)+
  done
    
subsubsection‹Miscellaneous›
  
lemma dom_inter: "[dom p ∩ dom q = {}; p x = ⌊y⌋] ==> q x = ⊥"
  by (auto)
    
lemma dom_eq: "dom p ∩ dom q = {} ==> p ⨁_A q = p ⨁_D q"
  unfolding override_A_def override_D_def
  by (rule ext, auto simp: dom_def split: prod.splits option.splits decision.splits )
    
lemma dom_split_alt_def : "(f, g) Δ p = (dom(p ▹ Allow) ◃ (A_f f)) ⨁ (dom(p ▹ Deny) ◃ (D_f g))"
  apply (rule ext)
  apply (simp add: dom_split2_def Allow_def Deny_def dom_restrict_def
      deny_all_fun_def allow_all_fun_def map_add_def)
  apply (simp split: option.splits decision.splits)
  apply (auto simp: map_add_def o_def deny_pfun_def ran_restrict_def image_def)
  done

end