Theory Impl_List_Playground_ChairNetwork

theory Impl_List_Playground_ChairNetwork
imports "../TopoS_Impl"
begin


text‹An example of our chair network [simplified]›

text‹Our access control view on the network›
  definition ChairNetwork_empty :: "string list_graph" where
    "ChairNetwork_empty ≡ ⦇ nodesL = [''WebSrv'', ''FilesSrv'', ''PrinterBW'',
                                ''PrinterColor'', ''Students'',
                                ''Employees'', ''EReachable'',
                                ''Internet''],
                      edgesL = [] ⦈"
  
  lemma "wf_list_graph ChairNetwork_empty" by eval


subsection‹Our security requirements›
  subsubsection‹We have a server with confidential data›
    definition ConfidentialChairData::"(string SecurityInvariant)" where
      "ConfidentialChairData ≡ new_configured_list_SecurityInvariant SINVAR_BLPtrusted_impl.SINVAR_LIB_BLPtrusted ⦇ 
          node_properties = [''FilesSrv'' ↦ ⦇ security_level = 1, trusted = False ⦈,
                             ''Employees'' ↦ ⦇ security_level = 0, trusted = True ⦈,
                             ''EReachable'' ↦ ⦇ security_level = 0, trusted = True ⦈]
          ⦈ ''confidential data''"


  (*
  subsubsection{*We have a hierarchical printing policy*}
    definition "PrintingHierarchy_nodes=[''Employees''↦ DN (''ColorPrinting''--Leaf, 0),
                           ''PrinterColor''↦ DN (''ColorPrinting''--''Printer''--Leaf, 0),
                           ''Students''↦ DN (''ColorPrinting''--''BwPrinting''--Leaf, 0),
                           ''PrinterBW''↦ DN (''ColorPrinting''--''BwPrinting''--''Printer''--Leaf, 0)]"
    definition "PrintingHierarchy_tree=Department ''ColorPrinting'' [
              Department ''Printer'' [], 
              Department ''BwPrinting'' [
                  Department ''Printer'' []]]"
    definition PrintingHierarchy::"string SecurityInvariant" where
      "PrintingHierarchy ≡ new_configured_list_SecurityInvariant SINVAR_DomainHierarchyNG_impl.SINVAR_LIB_DomainHierarchyNG ⦇ 
        node_properties = PrintingHierarchy_nodes
        ⦈"  *)
  subsubsection‹The color printer is only accessibly by employees, The black.white printer by employees and students›
    definition "PrintingACL ≡ new_configured_list_SecurityInvariant SINVAR_LIB_CommunicationPartners ⦇ 
          node_properties = [''PrinterColor'' ↦ Master [''Employees'', ''EReachable''],
                             ''PrinterBW'' ↦ Master [''Employees'', ''EReachable'', ''Students''],
                             ''Employees'' ↦ Care,
                             ''EReachable'' ↦ Care,
                             ''Students'' ↦ Care]
          ⦈ ''printing ACL''"

  subsubsection‹Printers are information sinks›
    definition "PrintingSink ≡ new_configured_list_SecurityInvariant SINVAR_LIB_Sink ⦇ 
          node_properties = [''PrinterColor'' ↦ Sink,
                             ''PrinterBW'' ↦ Sink]
          ⦈ ''printing sink''"



  subsubsection‹Students may access each other but are not accessible from the outside›
    definition "StudentSubnet ≡ new_configured_list_SecurityInvariant SINVAR_LIB_SubnetsInGW ⦇ 
          node_properties = [''Students'' ↦ Member, ''Employees'' ↦ Member, ''EReachable'' ↦ InboundGateway]
          ⦈ ''student subnet''"


  subsubsection‹The files server is only accessibly by employees›
    definition "FilesSrvACL ≡ new_configured_list_SecurityInvariant SINVAR_LIB_CommunicationPartners ⦇ 
          node_properties = [''FilesSrv'' ↦ Master [''Employees'', ''EReachable''],
                             ''Employees'' ↦ Care,
                             ''EReachable'' ↦ Care]
          ⦈ ''file srv acl''"


  subsubsection‹emplyees are reachable from the Internet›
    (*nothing to do here*)

lemma "implc_sinvar ConfidentialChairData ChairNetwork_empty" by eval
lemma "implc_sinvar PrintingACL ChairNetwork_empty" by eval
lemma "implc_sinvar PrintingSink ChairNetwork_empty" by eval
lemma "implc_sinvar StudentSubnet ChairNetwork_empty" by eval
lemma "implc_sinvar FilesSrvACL ChairNetwork_empty" by eval

definition "ChairSecurityRequirements = [ConfidentialChairData, PrintingACL, PrintingSink, StudentSubnet, FilesSrvACL]"

value "implc_get_offending_flows ChairSecurityRequirements ChairNetwork_empty"
value "generate_valid_topology ChairSecurityRequirements ChairNetwork_empty"

value "List.product (nodesL ChairNetwork_empty) (nodesL ChairNetwork_empty)"

definition "ChairNetwork = generate_valid_topology ChairSecurityRequirements 
      ⦇nodesL = nodesL ChairNetwork_empty, edgesL = List.product (nodesL ChairNetwork_empty) (nodesL ChairNetwork_empty) ⦈"

lemma "all_security_requirements_fulfilled ChairSecurityRequirements ChairNetwork" by eval

value "ChairNetwork"

ML_val‹
visualize_graph @{context} @{term "ChairSecurityRequirements"} @{term "ChairNetwork"};
›



end