| EPSRC Reference: |
GR/L61002/01 |
| Title: |
A CSP APPROACH TO THE ANALYSIS OF SECURITY PROTOCOLS |
| Principal Investigator: |
Lowe, Professor G |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Mathematics |
| Organisation: |
University of Leicester |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
22 September 1997 |
Ends: |
21 September 2000 |
Value (£): |
53,770
|
| EPSRC Research Topic Classifications: |
| Digital Signal Processing |
|
|
| EPSRC Industrial Sector Classifications: |
| No relevance to Underpinning Sectors |
|
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
The proposed project will continue recent research into analysing security protocols using the process algebra CSP and its model checker FDR. We will investigate how to model further protocol features within the CSP/FDR framework. We will investigate various methods of verifying security protocols, based upon the use of FDR. We will study methods of proving by hand that if a protocol is secure for a small system (checked using FDR) then it is secure for all larger systems. We will also investigate induction based techniques for model checking in a wider context, looking at ways of proving that if a system of a particular size is correct, then so is a system of the 'next size up'; we will use FSR to prove the inductive step, making use of results due to Lazic and Roscoe; we will then apply these induction based techniques to security protocols. Finally, we will investigate ways of verifying protocols that satisfy a number of 'healthiness principles' which seem to prevent the most common forms of attack. Our will aim to apply our techniques to real-world systems. We will also seek to understand the links between the modelling of security protocols and other areas such as fault tolerance.
|
|
Key Findings |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
|
Potential use in non-academic contexts |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
|
Impacts |
|
| Description |
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk |
| Summary |
|
| Date Materialised |
|
|
|
|
Sectors submitted by the Researcher |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
| Project URL: |
|
| Further Information: |
|
| Organisation Website: |
http://www.le.ac.uk |