PLTalk Model

auth.als

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 |
				u.can_access[c]
}

pred can_access[u: User, r: Resource] {
	u in r.allow or u in r.^parent.allow
}

check parent_implies_child