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.
