Noninterference and unwinding for LOCK

The LOCK noninterference policy for analyzing security properties of systems is presented. An unwinding theorem is developed. Difficulties resulting from trying to apply an abstract noninterference policy to a real system are discussed. A comparison is made between the LOCK noninterference policy and other versions of noninterference. >