Research proof index

Alternate definition of soundness for alwaysMatches: For a singleton policyset, if symcc says the policy alwaysMatches, then the spec authorizer should say it always appears in determiningPolicies

The verifyMatchesDisjoint analysis is complete: if the assertions verifyMatchesDisjoint p₁ p₂ εnv are satisfiable for the policies p₁ and p₂ and the strongly well-formed symbolic environment εnv, then there exists a strongly well-formed concrete environment env ∈ᵢ εnv such that both policies match in env.

The verifyMatchesDisjoint analysis is sound: if the assertions verifyMatchesDisjoint p₁ p₂ εnv are unsatisfiable for the policies p₁ and p₂ and the strongly well-formed symbolic environment εnv, then the policies cannot both match in any strongly well-formed concrete environment env ∈ᵢ εnv.

The verifyMatchesEquivalent analysis is complete: if the assertions verifyMatchesEquivalent p₁ p₂ εnv are satisfiable for the policies p₁ and p₂ and the strongly well-formed symbolic environment εnv, then there exists a strongly well-formed concrete environment env ∈ᵢ εnv such that the policies will have different matching behavior (one matche...

The verifyMatchesEquivalent analysis is sound: if the assertions verifyMatchesEquivalent p₁ p₂ εnv are unsatisfiable for the policies p₁ and p₂ and the strongly well-formed symbolic environment εnv, then the policies will have the same matching behavior (both match or both don't match) when applied to any strongly well-formed concrete environmen...

The verifyMatchesImplies analysis is sound: if the assertions verifyMatchesImplies p₁ p₂ εnv are unsatisfiable for the policies p₁ and p₂ and the strongly well-formed symbolic environment εnv, then if p₁ matches in any strongly well-formed concrete environment env ∈ᵢ εnv, then p₂ also matches.