About me

I am an Associate Professor at the Research School of Computer Science, The Australian National University. My main research interests span theoretical as well as practical aspects of computer science; these include formal methods, computational logic, automated theorem proving and computer security. More specifically, I am interested in modelling aspects of computational systems (such as parts of operating systems, communication protocols, simple authentication devices, etc) as mathematical theories, and developing tools and techniques to prove their correctness or to find potential flaws.

Research Interests

Proof theory: logical framework for reasoning about computations, higher-order abstract syntax, abstract logic programming, deep inference.

Theorem proving and verification.

Concurrency theory: process calculi, process equivalence, bisimulation.

Computer security: security protocol verification, operating system security, information flow security.

Phd Opportunities

I am looking for PhD students interested in doing research in formal methods for computer security, in particular in security protocols design and verification and mobile code security. Candidates with backgrounds in formal logic, discrete maths, and strong programming skills are preferred. Please email me for details and to express your interest.

Projects

Mechanized equivalence proofs for security protocols. Funded by the Ministry of Education Singapore. Principal Investigator. 2015-2018.

Securify: a compositional approach of building security verified system. Funded by the National Research Foundation, Singapore. Co-principal investigator. 2015-2020.

Formal verification of security protocols. 2013-2016. Nanyang Technological University. Principal Investigator. 2013-2017.

Evidence-based frameworks for security protocol verification. 2011 - 2015. Funded by the Australian Research Concil. Chief Investigator. 2011-2015.

Proof theoretical methods for reasoning about process equivalence. 2008 - 2011. Funded by the Australian Research Council. Chief Investigator. 2008-2010.

Software

Contact tracing: CVE-2020-12856 (COVIDSafe), CVE-2020-14292 (COVIDSafe), Apple/Google Exposure Notification framework

SPEC: An equivalence checker for cryptographic protocols.

Bedwyr. An automated theorem proving/model checking system based on the logic Linc.

LogicDroid: A customized Android operating system with security extension based on metric linear-time temporal logic

Professional activities

Program committee in IJCAR 2018, ITP 2018, FSCD 2018, CSF 2018, POST 2019, FSCD 2019.

Associate Editor for ACM Transactions on Computational Logic (since 2017). Area editor for proof theory and logical aspects of concurrency.

Past professional activities