Formal modelling and verifying communication and authentication protocols
Eligibility: UK/EU/International graduates with the required entry requirements
Funding details: Bursary plus tuition fees (UK/International (including EU at international rates from Sept 21)
Duration: Full-Time – between three and three and a half years fixed term
Application deadline: 27 May 2023 (international), 31 August 2023 (UK)
Interview date: Will be confirmed to shortlisted candidates
Start date: September 2023
For further details contact: Dr Rakib Abdur or Dr Lei Pan
Introduction
This PhD project is part of the Cotutelle arrangement between Coventry University, UK and Deakin University, Melbourne, Australia.
This is a CU Led project. The successful applicant will spend the 1st year at Coventry University and the following year at Deakin University and then the final 1.5 years at Coventry University
The supervision team will be drawn from the two Universities.
Project details
Communication and authentication protocols should be modelled and verified with formal methods before implementation to ensure their correctness. Some existing communication protocols have been modelled and proven to be secure without the presence of quantum-capable attackers. In this project, we will address the challenge of modelling and verifying communication and authentication protocols against quantum-capable attackers. That is, the protocols should be proven secure through formally specified proofs. This project will deliver formal method proofs of multiple communication and authentication protocols.
This project aims to achieve the following goals:
- Investigate state-of-the art design of standard communication and authentication protocols. Consider one or more such protocols, for example DoPI with TLS, and analyse security vulnerabilities against post-quantum cryptographic standard.
- Propose a formal framework to model and verify secrecy and authentication properties of such protocols for a more detailed security analysis against quantum attacks.
- Evaluate the scalability and expressiveness of the proposed approach by applying the framework, tool, and techniques to one or more desired communication and authentication protocols.
Funding
Tuition fees, stipend (£18,622 p/a) and additional allowances.
Benefits
The successful candidate will receive comprehensive research training including technical, personal and professional skills.
All researchers at Coventry University (from PhD to Professor) are part of the Doctoral College and Centre for Research Capability and Development, which provides support with high-quality training and career development activities.
Candidate specification
Applicants must meet the admission and scholarship criteria for both Coventry University and Deakin University for entry to the cotutelle programme.
This includes;
- Applicants should have graduated within the top 15% of their undergraduate cohort. This might include a high 2:1 in a relevant discipline/subject area with a minimum 70% mark (80% for Australian graduates) in the project element or equivalent with a minimum 70% overall module average (80% for Australian graduates).
- A Masters degree in a relevant subject area, with overall mark at minimum Merit level. In addition, the mark for the Masters dissertation (or equivalent) must be a minimum of 80%. Please note that where a candidate has 70-79% and can provide evidence of research experience to meet equivalency to the minimum first-class honours equivalent (80%+) additional evidence can be submitted and may include independently peer-reviewed publications, research-related awards or prizes and/or professional reports.
- Language proficiency (IELTS overall minimum score of 7.0 with a minimum of 6.5 in each component).
For an overview of each University’s entry requirements please visit:
https://www.deakin.edu.au/research/become-a-research-student/research-degree-entry-pathways
Please note that it is essential that applicants confirm that they are able to physically locate to both Coventry University (UK) and Deakin University (Australia).
Additional requirements
Applicants must have a good honours degree (as stated in the Candidate Specification section above) in Computer Science/Cyber Security or a closely related discipline, with a research interest in the areas related to Formal Methods/verification/Security Protocol Analysis. Prior knowledge of the PRISM model checker is preferred but not essential. Applicants must also have a strong background in high-level programming languages, especially in Python and/or C++/Java, preferably with a basic knowledge of temporal logics and model checking.
How to apply
All applications require full supporting documentation, a covering letter, plus an up to 2000-word supporting statement showing how the applicant’s expertise and interests are relevant to the project.
All candidates must apply to both Universities.
To find out more about the project please contact Dr Rakib Abdur or Dr Lei Pan.
Apply to Coventry University Apply to Deakin University
