Skip to content

Instantly share code, notes, and snippets.


hwayne/auth.als Secret

Created Jul 17, 2020
What would you like to do?
PLTalk Model
sig User {}
sig Resource {
, allow: set User
, parent: lone Resource
fact "No resource can be its own ancestor" {
no iden & ^parent
assert parent_implies_child {
-- if you can access a parent, you can access its child
all u: User, r: Resource |
u.can_access[r] =>
all c: r.~parent |
pred can_access[u: User, r: Resource] {
u in r.allow or u in r.^parent.allow
check parent_implies_child
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.