- cloud security and privacy
- policy formalisation and enforcement
- natural language processing, applied AI
- model checking and process algebra
- quantum cryptography
Some Past Results and Contributions:
- Design of languages, logics and tools for protocol specification and verification
- In joint work with Paulo Mateus and Pedro Baltazar (IST Lisbon), Nick helped to develop EpCTL, a probabilistic temporal logic that uses EPPL (exogenous probabilistic propositional logic) as its core.
- Model checking
- In collaboration with Rajagopal Nagarajan and Simon Gay Nick developed a model checker, QMC, for the analysis of properties of quantum communication and quantum cryptographic protocols. QMC is the first of its kind to our knowledge. Earlier work has included the use of a classical, probabilistic model checker for the analysis of similar protocols. This work combined classical verification techniques and models with the mathematics of quantum computing and quantum information, so this is clearly interdisciplinary.
- Syntax and semantics of languages for quantum programming
- Nick’s undergraduate final year project ‘Formal Specification and Verification of Quantum Protocols’ extended the work ofSimon Gay and Rajagopal Nagarajan on verifying the security of the BB84 protocol using classical process algebra and the probabilistic model checker PRISM. He was involved in the early stages of development of CQP (Communicating Quantum Processes), a quantum process algebra with a formal semantics and type system. Nick developed a quantum specification language for use in conjunction with the QMC model checker; the language has an operational semantics and an implementation.