Model checking trace-based information flow properties

Information flow properties are a way of specifying security properties of systems. A system is v...