(***************************************************************************** * HOL-TestGen --- theorem-prover based test case generation * http://www.brucker.ch/projects/hol-testgen/ * * This file is part of HOL-TestGen. * * Copyright (c) 2005-2012 ETH Zurich, Switzerland * 2008-2014 Achim D. Brucker, Germany * 2009-2014 Université Paris-Sud, France * * 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. ******************************************************************************) (* $Id: SeqComposition.thy 10879 2014-10-26 11:35:31Z brucker $ *) header{* Sequential Composition *} theory SeqComposition imports ElementaryPolicies begin text{* Sequential composition is based on the idea that two policies are to be combined by applying the second policy to the output of the first one. Again, there are four possibilities how the decisions can be combined. *} section {* Flattening *} text{* A key concept of sequential policy composition is the flattening of nested decisions. There are four possibilities, and these possibilities will give the various flavours of policy composition. *} fun flat_orA :: "('\ decision) decision \ ('\ decision)" where "flat_orA(allow(allow y)) = allow y" |"flat_orA(allow(deny y)) = allow y" |"flat_orA(deny(allow y)) = allow y" |"flat_orA(deny(deny y)) = deny y" lemma flat_orA_deny[dest]:"flat_orA x = deny y \ x = deny(deny y)" apply (case_tac "x") apply (simp_all) apply (case_tac "\") apply (simp_all) apply (case_tac "\") apply (simp_all) done lemma flat_orA_allow[dest]: "flat_orA x = allow y \ x = allow(allow y) \ x = allow(deny y) \ x = deny(allow y)" apply (case_tac "x") apply (simp_all) apply (case_tac "\") apply (simp_all) apply (case_tac "\") apply (simp_all) done fun flat_orD :: "('\ decision) decision \ ('\ decision)" where "flat_orD(allow(allow y)) = allow y" |"flat_orD(allow(deny y)) = deny y" |"flat_orD(deny(allow y)) = deny y" |"flat_orD(deny(deny y)) = deny y" lemma flat_orD_allow[dest]: "flat_orD x = allow y \ x = allow(allow y)" apply (case_tac "x") apply (simp_all) apply (case_tac "\") apply (simp_all) apply (case_tac "\") apply (simp_all) done lemma flat_orD_deny[dest]: "flat_orD x = deny y \ x = deny(deny y) \ x = allow(deny y) \ x = deny(allow y)" apply (case_tac "x") apply (simp_all) apply (case_tac "\") apply (simp_all) apply (case_tac "\") apply (simp_all) done fun flat_1 :: "('\ decision) decision \ ('\ decision)" where "flat_1(allow(allow y)) = allow y" |"flat_1(allow(deny y)) = allow y" |"flat_1(deny(allow y)) = deny y" |"flat_1(deny(deny y)) = deny y" lemma flat_1_allow[dest]: "flat_1 x = allow y \ x = allow(allow y) \ x = allow(deny y)" apply (case_tac "x") apply (simp_all) apply (case_tac "\") apply (simp_all) apply (case_tac "\") apply (simp_all) done lemma flat_1_deny[dest]: "flat_1 x = deny y \ x = deny(deny y) \ x = deny(allow y)" apply (case_tac "x") apply (simp_all) apply (case_tac "\") apply (simp_all) apply (case_tac "\") apply (simp_all) done fun flat_2 :: "('\ decision) decision \ ('\ decision)" where "flat_2(allow(allow y)) = allow y" |"flat_2(allow(deny y)) = deny y" |"flat_2(deny(allow y)) = allow y" |"flat_2(deny(deny y)) = deny y" lemma flat_2_allow[dest]: "flat_2 x = allow y \ x = allow(allow y) \ x = deny(allow y)" apply (case_tac "x") apply (simp_all) apply (case_tac "\") apply (simp_all) apply (case_tac "\") apply (simp_all) done lemma flat_2_deny[dest]: "flat_2 x = deny y \ x = deny(deny y) \ x = allow(deny y)" apply (case_tac "x") apply (simp_all) apply (case_tac "\") apply (simp_all) apply (case_tac "\") apply (simp_all) done section{* Policy Composition *} text{* The following definition allows to compose two policies. Denies and allows are transferred. *} fun lift :: "('\ \ '\) \ ('\ decision \'\ decision)" where "lift f (deny s) = (case f s of \y\ \ \deny y\ | \ \ \)" | "lift f (allow s) = (case f s of \y\ \ \allow y\ | \ \ \)" lemma lift_mt [simp]: "lift \ = \" apply (rule ext) apply (case_tac "x") apply (simp_all) done text{* Since policies are maps, we inherit a composition on them. However, this results in nestings of decisions---which must be flattened. As we now that there are four different forms of flattening, we have four different forms of policy composition: *} definition comp_orA :: "['\\'\, '\\'\] \ '\\'\" (infixl "o'_orA" 55) where "p2 o_orA p1 \ (map_option flat_orA) o (lift p2 o_m p1)" notation (xsymbols) comp_orA (infixl "\\<^sub>\\<^sub>A" 55) lemma comp_orA_mt[simp]:"p \\<^sub>\\<^sub>A \ = \" by(simp add: comp_orA_def) lemma mt_comp_orA[simp]:"\ \\<^sub>\\<^sub>A p = \" by(simp add: comp_orA_def) definition comp_orD :: "['\\'\, '\\'\] \ '\\'\" (infixl "o'_orD" 55) where "p2 o_orD p1 \ (map_option flat_orD) o (lift p2 o_m p1)" notation (xsymbols) comp_orD (infixl "\\<^sub>orD" 55) lemma comp_orD_mt[simp]:"p o_orD \ = \" by(simp add: comp_orD_def) lemma mt_comp_orD[simp]:"\ o_orD p = \" by(simp add: comp_orD_def) definition comp_1 :: "['\\'\, '\\'\] \ '\\'\" (infixl "o'_1" 55) where "p2 o_1 p1 \ (map_option flat_1) o (lift p2 o_m p1)" notation (xsymbols) comp_1 (infixl "\\<^sub>1" 55) lemma comp_1_mt[simp]:"p \\<^sub>1 \ = \" by(simp add: comp_1_def) lemma mt_comp_1[simp]:"\ \\<^sub>1 p = \" by(simp add: comp_1_def) definition comp_2 :: "['\\'\, '\\'\] \ '\\'\" (infixl "o'_2" 55) where "p2 o_2 p1 \ (map_option flat_2) o (lift p2 o_m p1)" notation (xsymbols) comp_2 (infixl "\\<^sub>2" 55) lemma comp_2_mt[simp]:"p \\<^sub>2 \ = \" by(simp add: comp_2_def) lemma mt_comp_2[simp]:"\ \\<^sub>2 p = \" by(simp add: comp_2_def) end