Research Interests
Security topics we specialise in include:
- Security Protocols: Verifying their correctness for security properties including: authentication, authorisation, confidentiality, integrity and non-repudiation. We are also interested in issues such as compositionality, scalability and delegation mechanisms.
- Intrusion Detection: Analysing issues concerning the deployment of intrusion detection systems.
- Information flow / Non-interference: Producing improved formal models of information flow and using them to analyse systems.
- Steganography: Developing foundations for covert channel capacity and investigating practical issues for the productization of steganography screening.
- Pervasive (Ubiquitous) Computing: Pervasive, or ubiquitous, computing is a term for the presence of communicating computing systems in more and more items in everyday life. It presents a number of security challenges, such as authentication in a very different and heterogeneous environment and the need to protect privacy.
The verification techniques we specialise in include:
- Process algebraic approaches: Particularly using the process algebra CSP.
- Model checking techniques: Primarily using the tool FDR.
- Casper: Compiler that takes a high level description of a security protocol and generates the corresponding model in CSP, allowing the use of model checking techniques to prove or disprove properties about the protocol.
- Data independence techniques: Enables a more complete analysis of security protocols using model checking techniques; for example, by enabling participants to perform unbounded protocol runs.