Gavin Lowe

Gavin Lowe carries out research on formal aspects of Computer Security, particularly security protocols. He has developed a technique for analysing security protocols, making use of the process algebra CSP. Briefly: a model is built of the protocol and of an attacker who can attack the protocol; the model checker FDR is used to explore the state space looking for attacks. He has produced a compiler, Casper, which makes these techniques easier to apply, making them accessible to industry, and allowing them to be used in teaching.

He has extended this basic technique in order to analyse many different features of security protocols. He has also studied ways of designing protocols, to prevent certain classes of attacks, or to aid the design process. Further, he has studied the question of information flow in multi-level security systems, where no information should flow from a high security level to a low one.

He has also carried out more foundational and theoretical work in mathematical models of concurrency, particularly of systems exhibiting timed or probabilistic behaviours, and in developing model-checking techniques.