Formalisation of "Noninterference, Transitivity, and Channel-Control Security Policies" by John Rushby.
Requires std++.
The proofs are in Rushby.v.
co-dan/noninterference-coq
Formalisation of "Noninterference, Transitivity, and Channel-Control Security Policies" by J. Rushby
Coq