Documentation

Cedar.Thm.SymCC.Verifier.VerifyIsAuthorized

This file proves the soundness and completeness of Cedar.SymCC.verifyIsAuthorized for well-behaved verification queries. This enables proving soundness and completenss of analyses built on verifyIsAuthorized by proving that their queries are well-behaved. #

source
def Cedar.Thm.WellBehavedIsAuthorizedQuery (φ : SymCC.Term → SymCC.Term → SymCC.Term) (f : Spec.Response → Spec.Response → Bool) :
Prop
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Cedar.Thm.WellBehavedIsAuthorizedQuery.WellFormedInput (t : SymCC.Term) (εs : SymCC.SymEntities) :
    Prop
    Equations
    Instances For
      source
      def Cedar.Thm.WellBehavedIsAuthorizedQuery.WellFormedInputs (t₁ t₂ : SymCC.Term) (εs : SymCC.SymEntities) :
      Prop
      Equations
      Instances For
        source
        def Cedar.Thm.WellBehavedIsAuthorizedQuery.WellFormedOutput (φ : SymCC.Term → SymCC.Term → SymCC.Term) :
        Prop
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Cedar.Thm.WellBehavedIsAuthorizedQuery.Interpretable (φ : SymCC.Term → SymCC.Term → SymCC.Term) :
          Prop
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Cedar.Thm.WellBehavedIsAuthorizedQuery.Same (φ : SymCC.Term → SymCC.Term → SymCC.Term) (f : Spec.Response → Spec.Response → Bool) :
            Prop
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem Cedar.Thm.verifyIsAuthorized_is_sound {φ : SymCC.Term → SymCC.Term → SymCC.Term} {f : Spec.Response → Spec.Response → Bool} {ps₁ ps₂ : Spec.Policies} {εnv : SymCC.SymEnv} {asserts : SymCC.Asserts} :
              WellBehavedIsAuthorizedQuery φ f → εnv.StronglyWellFormedForPolicies ps₁ → εnv.StronglyWellFormedForPolicies ps₂ → SymCC.verifyIsAuthorized φ ps₁ ps₂ εnv = Except.ok asserts → εnv ⊭ asserts → ∀ (env : Spec.Env), env∈ᵢεnv → env.StronglyWellFormedForPolicies ps₁ → env.StronglyWellFormedForPolicies ps₂ → f (Spec.isAuthorized env.request env.entities ps₁) (Spec.isAuthorized env.request env.entities ps₂) = true
              source
              theorem Cedar.Thm.verifyIsAuthorized_is_complete {φ : SymCC.Term → SymCC.Term → SymCC.Term} {f : Spec.Response → Spec.Response → Bool} {ps₁ ps₂ : Spec.Policies} {εnv : SymCC.SymEnv} {asserts : SymCC.Asserts} :
              WellBehavedIsAuthorizedQuery φ f → εnv.StronglyWellFormedForPolicies ps₁ → εnv.StronglyWellFormedForPolicies ps₂ → SymCC.verifyIsAuthorized φ ps₁ ps₂ εnv = Except.ok asserts → εnv ⊧ asserts → ∃ (env : Spec.Env), env∈ᵢεnv ∧ env.StronglyWellFormedForPolicies ps₁ ∧ env.StronglyWellFormedForPolicies ps₂ ∧ SymCC.Env.EnumCompleteFor env εnv ∧ f (Spec.isAuthorized env.request env.entities ps₁) (Spec.isAuthorized env.request env.entities ps₂) = false