Formal Analysis for Encryption- Based Multilevel Model for DBMS - Multilevel Security for Relational Databases - page 129

Encryption-based multilevel model

Insert
Delete
Select

MLR
Data

Encryption
System

Success/
Failure

Figure 6.1 The interface of the encryption-based multilevel model.

UPLEVEL statements) from users with varying security classification
levels. The outputs from the encryption-based multilevel database
model are the results retrieved by the users that include the following:

• Group of the retrieved tuples for the SELECT statement
• SUCCESS or FAILURE status for the INSERT, DELETE,
UPDATE, or UPLEVEL statements

Theorem 6.7.1: The encryption-based multilevel model is secure.
To prove this theorem, the following lemmas should be proven.

Lemma 6.7.1: For security classification level L, changing TH ( L )
cannot affect the output to the user S ∈ SV ( L ).

Proof of Lemma 6.7.1: If a SELECT statement is executed by a user
that has security classification level L ′, where S ∈ SV ( L ) ( L ′ ≤ L ), no
tuples in TH ( L ′) will be taken into the calculation of P. Since L ′ ≤ L
includes that TH ( L ′) ⊇ TH ( L ), modifying TH ( L ) cannot affect the
tuples' output to S ∈ SV ( L ).

By the INSERT, DELETE, UPDATE, and UPLEVEL
operations for a user that has security classification level L ′, where
S ∈ SV ( L ) ( L ′ ≤ L ):
The INSERT operation executed by a user, s, could be rejected if:

• There is a tuple t ′ ∈ r with t ′[ A 1 ] = a 1 ∧ t ′[ TC ] = L ′.
• The tuple t that is inserted violates the entity integrity, the
foreign key integrity, or the referential integrity properties.

The DELETE operation executed by a user, s, could be rejected if:

• The tuple with security classification level L that is deleted
is referenced by some tuples that have security classification
level L ′ where ( L ′ ≤ L ).