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

Theorem 6.6.1: The encryption-based multilevel model is complete.

To prove the completeness of the encryption-based multilevel
model, the following lemmas should be proven.

Lemma 6.6.1: The sequences of the data manipulation operations
transform any legal database state to an empty database state.

Proof: In the DELETE operation, the following steps can be
performed:

• If the base tuple is deleted, any entity will be deleted totally.
In the DELETE operation, if the values of [

tE A C are
given in the WHERE clause, only the referencing tuples will
be deleted. This will ensure the referential integrity property.
• The empty database state can exist by deleting all entities in
all multilevel relational instances.

( )] 1

1

Lemma 6.6.2: The sequences of the data manipulation operation
transform any empty database to any legal database state.

Proof: In the INSERT operation, the following steps can be performed:

• The referencing tuples will be inserted before inserting the
referenced tuples.
• Each tuple is inserted by a user with a security classification
level equal to the tuple classification value as follows:
• The base tuple t is inserted by a user using an INSERT
statement with all A i that have t 1 [ A i ] ≠ null listed in the
INTO clause, and t 1 [ A i ] in the VALUES clause.

In the UPLEVEL operation, inserting any additional tuple t m is
done by the following step:

• All mC with t m [ C i ] < t m [ TC ] are included in the USE

clause of the UPLEVEL statement.

tE A [ ( )]

1 1

The legal database state can exist by using INSERT, UPLEVEL,
and UPDATE for inserting all entities in all multilevel relational
instances. This legal database state should satisfy the entity integrity,