Theory Example

theory Example
imports "../TopoS_Interface" "../TopoS_Library"
begin

subsection ‹Network Graph and Security Requirements›

  text‹We define the network›
  definition example_net_secgw :: "nat list_graph" where
  "example_net_secgw ≡ ⦇ nodesL = [1::nat,2,3, 8, 11,12], 
    edgesL = [
      (1,8),(8,2),(2,8),(8,1), 
      (8,11),(8,12), 
      (11,12)] ⦈"
  value "wf_list_graph example_net_secgw"


  text‹We add two security requirements›
  definition NMParams_secgw_1 :: "(nat, secgw_member) TopoS_Params" where
  "NMParams_secgw_1 ≡ ⦇ node_properties = [1 ↦ DomainMember, 
                                     2 ↦ DomainMember, 
                                     3 ↦ DomainMember,
                                     8 ↦ PolEnforcePoint] ⦈"


  definition NMParams_blptrusted_1 :: "(nat, SINVAR_BLPtrusted.node_config) TopoS_Params" where
  "NMParams_blptrusted_1 ≡ ⦇ node_properties = [1 ↦ ⦇ security_level = 1, trusted = False ⦈, 
                                     2 ↦ ⦇ security_level = 1, trusted = False ⦈, 
                                     3 ↦ ⦇ security_level = 1, trusted = False ⦈,
                                     8 ↦ ⦇ security_level = 0, trusted = True ⦈] ⦈"

  text‹Both security requirements fulfilled?›
  value "PolEnforcePoint_eval example_net_secgw NMParams_secgw_1"
  value "SINVAR_BLPtrusted_impl.BLP_eval example_net_secgw NMParams_blptrusted_1"


text‹Add violations!›
  definition example_net_secgw_invalid where
  "example_net_secgw_invalid ≡ example_net_secgw⦇edgesL := (1,11)#(11,1)#(11,8)#(1,2)#(edgesL example_net_secgw)⦈"

  text‹Security Requirement still fulfilled?›
  value "PolEnforcePoint_eval example_net_secgw_invalid NMParams_secgw_1"
  text‹Whom to blame?›
  value "PolEnforcePointExtended_offending_list example_net_secgw_invalid
          (SINVAR_SecGwExt_impl.NetModel_node_props NMParams_secgw_1)"

  text‹Security Requirement still fulfilled?›
  value "SINVAR_BLPtrusted_impl.BLP_eval example_net_secgw_invalid NMParams_blptrusted_1"
  text‹Whom to blame?›
  value "SINVAR_BLPtrusted_impl.BLP_offending_list example_net_secgw_invalid
      (SINVAR_BLPtrusted_impl.NetModel_node_props NMParams_blptrusted_1)"


end