Implementing Access Control Logic in a Corporate IT System

The objective of this case study is to demonstrate how logical reasoning and formal proofs can be applied to design and verify access control policies in a corporate IT environment using the principles from Chapter 3.

A mid-sized company is developing an internal web application to provide employees with access to sensitive resources. The system must enforce the following access control rules:

1. Only authenticated users can access the system.
2. Users with admin privileges can access all resources.
3. Regular users can access only their own data.
4. If a user is not authenticated, they must be denied access.

The IT team wants to ensure that these rules are logically sound, non-redundant, and enforceable through code.

For the logical representation of this scenario, let the following propositions represent system conditions:

• • [latex]A(x)[/latex]: User [latex]x[/latex] is authenticated.
  • [latex]R(x)[/latex]: User [latex]x[/latex] is a regular user.
  • [latex]D(x)[/latex]: User [latex]x[/latex] is an admin.
  • [latex]P(x)[/latex]: User [latex]x[/latex] is permitted access.
  • [latex]O(x)[/latex]: User [latex]x[/latex] is accessing their own data.

Task 1

State the access controls using logic. For example, rule 1 would be [latex]A(x) \rightarrow P(x)[/latex].

Task 2

Perform a redundancy check by checking if any rules are contrapositive of each other. List the pairs of rules that are contrapositives.

Task 3

Perform a consistency check by checking if any rules have inconsistencies between regular users and admin users. State any inconsistencies for each rule.

Task 4

Create a combined rule that defines a unified access condition. It should be a biconditional that ensures access is granted only if the user is authenticated and either an admin or a regular user accessing their own data.

Task 5

Prove the following theorem: If a user is not authenticated, they cannot access the system.

Task 6

Prove the following theorem: If a user is authenticated and an admin, they can access any resource.

Task 7

Implement the scenario using pseudocode.