-
Notifications
You must be signed in to change notification settings - Fork 18
/
Copy pathAuthorization.lean
97 lines (84 loc) · 3.42 KB
/
Authorization.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
/-
Copyright Cedar Contributors
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
import Cedar.Spec
import Cedar.Thm.Authorization.Authorizer
/-! This file contains basic theorems about Cedar's authorizer. -/
namespace Cedar.Thm
open Cedar.Data
open Cedar.Spec
/--
Forbid trumps permit: if a `forbid` policy is satisfied, the request is denied.
-/
theorem forbid_trumps_permit
(request : Request) (entities : Entities) (policies : Policies) :
(∃ (policy : Policy),
policy ∈ policies ∧
policy.effect = .forbid ∧
satisfied policy request entities) →
(isAuthorized request entities policies).decision = .deny
:= by
intro h
unfold isAuthorized
simp [if_satisfied_then_satisfiedPolicies_non_empty h]
/--
A request is explicitly permitted when there is at least one satisfied permit policy.
-/
def IsExplicitlyPermitted (request : Request) (entities : Entities) (policies : Policies) : Prop :=
∃ (policy : Policy),
policy ∈ policies ∧
policy.effect = .permit ∧
satisfied policy request entities
/-- A request is allowed only if it is explicitly permitted. -/
theorem allowed_if_explicitly_permitted (request : Request) (entities : Entities) (policies : Policies) :
(isAuthorized request entities policies).decision = .allow →
IsExplicitlyPermitted request entities policies
:= by
unfold isAuthorized
generalize (satisfiedPolicies .forbid policies request entities) = forbids
generalize hp : (satisfiedPolicies .permit policies request entities) = permits
simp only [Bool.and_eq_true, Bool.not_eq_true']
cases forbids.isEmpty <;> simp
cases h₁ : permits.isEmpty <;> simp
unfold IsExplicitlyPermitted
subst hp
exact if_satisfiedPolicies_non_empty_then_satisfied h₁
/--
Default deny: if not explicitly permitted, the request is denied.
This is contrapositive of allowed_if_explicitly_permitted.
-/
theorem default_deny (request : Request) (entities : Entities) (policies : Policies) :
¬ IsExplicitlyPermitted request entities policies →
(isAuthorized request entities policies).decision = .deny
:= by
intro h₀
generalize h₁ : (isAuthorized request entities policies).decision = dec
by_contra h₂
cases dec
case allow =>
have h₃ := allowed_if_explicitly_permitted request entities policies h₁
contradiction
case deny => contradiction
/--
Order and duplicate independence: isAuthorized produces the same result
regardless of policy order or duplicates.
-/
theorem order_and_dup_independent (request : Request) (entities : Entities) (policies₁ policies₂ : Policies) :
policies₁ ≡ policies₂ →
isAuthorized request entities policies₁ = isAuthorized request entities policies₂
:= by
intro h
have hf := satisfiedPolicies_order_and_dup_independent .forbid request entities h
have hp := satisfiedPolicies_order_and_dup_independent .permit request entities h
have he := errorPolicies_order_and_dup_independent request entities h
simp [isAuthorized, hf, hp, he]
end Cedar.Thm