[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Inconsistent access control policies checking using TLA+

Hi All,

Is it possible to identify inconsistent access policies using TLA+?

Inconsistent access policies are one of the following:

users= {u1, u2}
dataTypes= {T1, T2}
permission= {u1 -> T1, u2 -> T2} // u1 and u2 can access T1 and T2 respectively
restriction= {u1 -> T2} // u1 can not access T2

Then we define some access policy P1:
P1 = {∀ t ∈ dataTypes u2 -> t => u1 -> t} // This tells, u1 can acces all dataTypes that u2 can access. This is an inconsistent defenition according to permission and restriction set.

I am trying to ask that, is it possible to identify these type of inconsistent definitions using TLA+?

- Thaks and Regards

Nikhila K N