Seclib.Prim.Rule

Rule — ⚪ definition

structure · source

Vendor-neutral authorization primitives: Rule, appliesOf, denyOverrides. No cloud provider noun appears in this module.

structure Rule where

denyOverridesRules — ⚪ definition

def · source

def denyOverridesRules (rules : List Rule) : Bool

denyOverrides_remove_allow_narrows — 🟢 proved

theorem · source

Lemma 1: Removing an allow rule narrows access

theorem denyOverrides_remove_allow_narrows (rules : List Rule) (i : Nat)
    (hi : i < rules.length) (hallow : (rules[i]).decision = .allow)
    (h : denyOverridesRules (rules.eraseIdx i) = true) :
    denyOverridesRules rules = true

denyOverrides_add_deny_narrows — 🟢 proved

theorem · source

Lemma 2: Adding a deny narrows

theorem denyOverrides_add_deny_narrows (rules : List Rule) (i : Nat)
    (hi : i < rules.length) (hdeny : (rules[i]).decision = .deny)
    (h : denyOverridesRules rules = true) :
    denyOverridesRules (rules.eraseIdx i) = true

conj_narrows — 🟢 proved

theorem · source

Lemma 3: Conjunction of evaluation gates never widens access

theorem conj_narrows (a b : Bool) (h : a && b = true) : a = true ∧ b = true

appliesOf_unknown_conservative — 🟢 proved

theorem · source

Lemma 4: Unknown applicability is conservative

theorem appliesOf_unknown_conservative (rules rules_noCtx : List Rule)
    (hlen : rules.length = rules_noCtx.length)
    (hpair : ∀ j (hj : j < rules.length),
      (rules_noCtx[j]'(hlen ▸ hj)).decision = (rules[j]).decision ∧
      (rules_noCtx[j]'(hlen ▸ hj)).sat = (rules[j]).sat ∧
      ((rules_noCtx[j]'(hlen ▸ hj)).applicability = .t ∨
       (rules_noCtx[j]'(hlen ▸ hj)).applicability = .u) ∧
      ((rules_noCtx[j]'(hlen ▸ hj)).applicability = .t →
       (rules[j]).applicability = .t))
    (h : denyOverridesRules rules = true) :
    denyOverridesRules rules_noCtx = true