This file proves a key lemma used to show the soundness and completeness of analyses built on top of Cedar's symbolic authorizer.

theorem Cedar.Thm.compileWithEffect_error_implies {effect : Spec.Effect} {p : Spec.Policy} {εnv : SymCC.SymEnv} {err : SymCC.Error} : SymCC.compileWithEffect effect p εnv = Except.error err → p.effect = effect ∧ SymCC.compile p.toExpr εnv = Except.error err

theorem Cedar.Thm.compileWithEffect_none_implies {effect : Spec.Effect} {p : Spec.Policy} {εnv : SymCC.SymEnv} : SymCC.compileWithEffect effect p εnv = Except.ok none → p.effect ≠ effect

theorem Cedar.Thm.compileWithEffect_some_implies {effect : Spec.Effect} {p : Spec.Policy} {εnv : SymCC.SymEnv} {t : SymCC.Term} : SymCC.compileWithEffect effect p εnv = Except.ok (some t) → p.effect = effect ∧ SymCC.compile p.toExpr εnv = Except.ok t

theorem Cedar.Thm.satisfiedPolicies_filterMapM_eq {effect : Spec.Effect} {ps : Spec.Policies} {εnv : SymCC.SymEnv} : List.filterMapM (fun (x : Spec.Policy) => SymCC.compileWithEffect effect x εnv) ps = List.mapM (fun (p : Spec.Policy) => SymCC.compile p.toExpr εnv) (List.filter (fun (p : Spec.Policy) => p.effect == effect) ps)

theorem Cedar.Thm.compile_policy_wf {p : Spec.Policy} {εnv : SymCC.SymEnv} {t : SymCC.Term} : εnv.WellFormedFor p.toExpr → SymCC.compile p.toExpr εnv = Except.ok t → SymCC.Term.WellFormed εnv.entities t ∧ t.typeOf = SymCC.TermType.bool.option

theorem Cedar.Thm.satisfiedPolicies_ok_implies {effect : Spec.Effect} {ps : Spec.Policies} {εnv : SymCC.SymEnv} {t : SymCC.Term} : SymCC.satisfiedPolicies effect ps εnv = Except.ok t → ∃ (ts : List SymCC.Term), t = SymCC.Factory.anyTrue (fun (x : SymCC.Term) => SymCC.Factory.eq x (SymCC.Term.bool true).some) ts ∧ List.mapM (fun (p : Spec.Policy) => SymCC.compile p.toExpr εnv) (List.filter (fun (p : Spec.Policy) => p.effect == effect) ps) = Except.ok ts

@[reducible, inline]

abbrev Cedar.Thm.eqSomeTrue : SymCC.Term → SymCC.Term

Equations

• Cedar.Thm.eqSomeTrue x✝ = Cedar.SymCC.Factory.eq x✝ (Cedar.SymCC.Term.bool true).some

theorem Cedar.Thm.satisfiedPolicies_wf {effect : Spec.Effect} {ps : Spec.Policies} {εnv : SymCC.SymEnv} {t : SymCC.Term} (hwε : εnv.WellFormedForPolicies ps) (hok : SymCC.satisfiedPolicies effect ps εnv = Except.ok t) : SymCC.Term.WellFormed εnv.entities t ∧ t.typeOf = SymCC.TermType.bool

theorem Cedar.Thm.satisfiedPolicies_interpret {effect : Spec.Effect} {ps : Spec.Policies} {εnv : SymCC.SymEnv} {t : SymCC.Term} {I : SymCC.Interpretation} (hwε : εnv.WellFormedForPolicies ps) (hwI : I.WellFormed εnv.entities) (hok : SymCC.satisfiedPolicies effect ps εnv = Except.ok t) : SymCC.satisfiedPolicies effect ps (SymCC.SymEnv.interpret I εnv) = Except.ok (SymCC.Term.interpret I t)

theorem Cedar.Thm.satisfiedPolicies_eq {effect : Spec.Effect} {ps : Spec.Policies} {env : Spec.Env} {εnv : SymCC.SymEnv} {t : SymCC.Term} (hwε : εnv.WellFormedForPolicies ps) (hwe : env.WellFormedForPolicies ps) (heq : env ∼ εnv) (hok : SymCC.satisfiedPolicies effect ps εnv = Except.ok t) : t = SymCC.Term.bool !(Spec.satisfiedPolicies effect ps env.request env.entities).isEmpty

theorem Cedar.Thm.satisfiedPolicies_bisimulation {effect : Spec.Effect} {ps : Spec.Policies} {env : Spec.Env} {εnv : SymCC.SymEnv} {t : SymCC.Term} {I : SymCC.Interpretation} (hwε : εnv.WellFormedForPolicies ps) (hwe : env.WellFormedForPolicies ps) (hwI : I.WellFormed εnv.entities) (heq : env ∼ SymCC.SymEnv.interpret I εnv) (hok : SymCC.satisfiedPolicies effect ps εnv = Except.ok t) : SymCC.Term.interpret I t = SymCC.Term.bool !(Spec.satisfiedPolicies effect ps env.request env.entities).isEmpty

theorem Cedar.Thm.same_decisions_def {d : Spec.Decision} {t : SymCC.Term} : d ∼ t ↔ SymCC.SameDecisions d t

theorem Cedar.Thm.same_decisions_iff_allow_true_or_deny_false {d : Spec.Decision} {t : SymCC.Term} : d ∼ t ↔ d = Spec.Decision.allow ∧ t = SymCC.Term.bool true ∨ d = Spec.Decision.deny ∧ t = SymCC.Term.bool false

theorem Cedar.Thm.same_responses_iff_same_decisions {r : Spec.Response} {t : SymCC.Term} : r ∼ t ↔ r.decision ∼ t

theorem Cedar.Thm.same_responses_self_decision {resp : Spec.Response} : resp ∼ resp.decision

theorem Cedar.Thm.same_decision_and_response_implies_same_decision {decision : Spec.Decision} {resp : Spec.Response} {t : SymCC.Term} : decision ∼ t → resp ∼ t → resp ∼ decision

theorem Cedar.Thm.isAuthorized_ok_implies {ps : Spec.Policies} {εnv : SymCC.SymEnv} {t : SymCC.Term} : SymCC.isAuthorized ps εnv = Except.ok t → ∃ (tp : SymCC.Term), ∃ (tf : SymCC.Term), SymCC.satisfiedPolicies Spec.Effect.permit ps εnv = Except.ok tp ∧ SymCC.satisfiedPolicies Spec.Effect.forbid ps εnv = Except.ok tf ∧ t = SymCC.Factory.and tp (SymCC.Factory.not tf)

theorem Cedar.Thm.isAuthorized_wf {ps : Spec.Policies} {εnv : SymCC.SymEnv} {t : SymCC.Term} : εnv.WellFormedForPolicies ps → SymCC.isAuthorized ps εnv = Except.ok t → SymCC.Term.WellFormed εnv.entities t ∧ t.typeOf = SymCC.TermType.bool

theorem Cedar.Thm.isAuthorized_interpret_eq_when_interpret_eq {ps : Spec.Policies} {εnv : SymCC.SymEnv} {I I' : SymCC.Interpretation} {t : SymCC.Term} (hwε : εnv.WellFormedForPolicies ps) (hwI : I.WellFormed εnv.entities) (hwI' : I'.WellFormed εnv.entities) (heq : ∀ (p : Spec.Policy) (t : SymCC.Term), p ∈ ps → SymCC.compile p.toExpr εnv = Except.ok t → SymCC.Term.interpret I t = SymCC.Term.interpret I' t) (hok : SymCC.isAuthorized ps εnv = Except.ok t) : SymCC.Term.interpret I t = SymCC.Term.interpret I' t

theorem Cedar.Thm.isAuthorized_interpret {ps : Spec.Policies} {εnv : SymCC.SymEnv} {t : SymCC.Term} {I : SymCC.Interpretation} : εnv.WellFormedForPolicies ps → I.WellFormed εnv.entities → SymCC.isAuthorized ps εnv = Except.ok t → SymCC.isAuthorized ps (SymCC.SymEnv.interpret I εnv) = Except.ok (SymCC.Term.interpret I t)

theorem Cedar.Thm.isAuthorized_same {ps : Spec.Policies} {env : Spec.Env} {εnv : SymCC.SymEnv} {t : SymCC.Term} : εnv.WellFormedForPolicies ps → env.WellFormedForPolicies ps → env ∼ εnv → SymCC.isAuthorized ps εnv = Except.ok t → Spec.isAuthorized env.request env.entities ps ∼ t

theorem Cedar.Thm.isAuthorized_bisimulation {ps : Spec.Policies} {env : Spec.Env} {εnv : SymCC.SymEnv} {t : SymCC.Term} {I : SymCC.Interpretation} : εnv.WellFormedForPolicies ps → env.WellFormedForPolicies ps → I.WellFormed εnv.entities → env ∼ SymCC.SymEnv.interpret I εnv → SymCC.isAuthorized ps εnv = Except.ok t → Spec.isAuthorized env.request env.entities ps ∼ SymCC.Term.interpret I t