Summary: We propose to investigate the application of the work of Syverson and Gray in developing a logic for reasoning about time in a security context as well as an adaptation of the use of a probabilistic bisimulation by Sands and Sabelfeld to demonstrate non-interference of imperative programs in the presence of a probabilistic scheduler. We propose to investigate the use of operational semantics together with a probabilistic bisimulation to handle branching behaviours within loops. Loops are currently a difficult problem in quantifying the leakage of secrets on the basis of information theory

David Clark

• Chalmers University of Technology, Sweden

This project was funded by the EPSRC.