RBAC

file.tla

Matches(Binding, User) ≝
  ∃ Subject ∈ Binding.Subjects:
    CASE Subject.Kind = "User" ⟶
           Subject.Name = User.Name
      [] Subject.Kind = "Group" ⟶
           Subject.Name \in User.Groups
      [] Subject.Kind = "ServiceAccount" ⟶
           ServiceAccount(Subject.Name, WithDefault(Subject.Namespace, Binding.Namespace)) = User.Name