Formalisation of "Noninterference, Transitivity, and Channel-Control Security Policies" by John Rushby. Requires std++. The proofs are in Rushby.v.