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

The UPDATE operation executed by a user, s, could be rejected if:
• There is a tuple t ′ ∈ r with t ′[ A 1 ] = t [ A 1 ] ∧ t ′[ TC ] = L ′.
• The tuple t that is updated violates the entity integrity, foreign
key integrity, or referential integrity properties.
The UPLEVEL operation executed by a user, s, could be rejected if:
• There is a tuple t ′ ∈ r with t ′[ A 1 ] = t [ A 1 ] ∧ t ′[ C 1 ] = t [ C 1 ] ∧
t ′[ TC ] = L ′.
• The tuple t that is updated violates the entity integrity, the
foreign key integrity, or the referential integrity properties.
Since t, t ′ ∉ TH ( L ′) ⊇ TH ( L ), modifying TH ( L ) cannot affect the
S/F information output to S ∈ SV ( L ); therefore, modifying TH ( L )
cannot affect the output to S ∈ SV ( L ).
Lemma 6.7.2: For security classification level L, deleting any input
from user S ∈ SH ( L ) cannot change TV ( L ).
Proof of Lemma 6.7.2: The user can change the database states by an
INSERT, DELETE, UPDATE, or UPLEVEL operation.
The INSERT operation is executed by a user, s, that has security
classification level L ′, where S ∈ SH ( L ) ( L ′ > L ) can only generate the
L ′-tuple t ′ since L ′ > L, t ′ ∉ TV ( L ).
The DELETE operation is executed by a user, s, that has security
classification level L ′, where S ∈ SH ( L ) ( L ′ > L ) can only delete L ′-tuples
t ′, and may change the polyinstantiation tuple t ″ at levels L ″( L ″ > L ′).
The UPDATE operation is executed by a user, s, that has security
classification level L ′, where S ∈ SH ( L ) ( L ′ > L ) can only change L ′-tuples
t ′ and may change the polyinstantiation tuple t ″ at levels L ″( L ″ > L ′).
The UPLEVEL operation is executed by a user, s, that has security
classification level L ′, where S ∈ SH ( L ) ( L ′ > L ) can only change L ′-tuples
t ′ and may change the polyinstantiation tuple t ″ at levels L ″( L ″ > L ′).
From the previous paragraphs, deleting any input from a subject
S ∈ SH ( L ) cannot change TV ( L ).
Proof of Theorem 6.7.1: From Lemma 6.7.1 and Lemma 6.7.2, for
any security classification level L, since S = SV ( L ) ∪ SH ( L ), SV ( L ) ∩