Inconsistent access control policies checking using TLA+

[knnik...@xxxxxxxxx]

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