On the refinement of non-interference

Abstract

It is known that functional refinement does not preserve the security properties of a system. The authors propose a trace-based method for specifying the security properties of a system and a method which ensures that this security is preserved under refinement. They include an example to illustrate the use of the definitions and make use of non-interference (as defined in their notation).< <ETX xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">&gt;</ETX>