McLean, J. ``Proving Noninterference and Functional Correctness
Using Traces,''  Journal of Computer Security, vol. 1, no. 1, 1992.
<a href="1992mclean-jcs.ps">
 PostScript</a>
<P>