| EPSRC Reference: |
GR/K34368/01 |
| Title: |
ROPA: ESTABLISHING SECURITY PROPERTIES OF DISTRIBUTED SYSTEMS VIA MODEL-CHECKING |
| Principal Investigator: |
Wallen, Professor L |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science |
| Organisation: |
University of Oxford |
| Scheme: |
ROPA |
| Starts: |
01 February 1995 |
Ends: |
31 January 1997 |
Value (£): |
79,871
|
| EPSRC Research Topic Classifications: |
| Digital Signal Processing |
|
|
| EPSRC Industrial Sector Classifications: |
| Transport Systems and Vehicles |
|
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
To adapt and combine model-checking techniques and methods from Z and CSP to establish security properties of IT systems in distributed environments.To conduct a controlled experiment to develop and test the theory using distributed file system as a case study. Progress:The project began on 01.02.95 with the appointment of an RA, Dr. Gavin Lowe. Despite this very recent official start, there has been a significant amount of activity in the area since the application was submitted which contributes to the objectives of the grant.Work on the incorporation of determinism checking into FDR and work on the applications of CSP to crypto protocols (such as key exchange) has progressed [R9Sa,R9Sb,R9Sc,RWWu94]. A preliminary theory of abstraction and refinement underpinning independence and security specifications in CSP has been developed [RWu94]; these developments are being applied to the TCP protocol and crypto portocols to analyse the security of ATM machines and PIN numbers. FDR has been used to discover an error in published authentication protocol concerning agents in a distributed environment; it has also been shown how to fix the error. Investigations are proceeding to ascertain if the new protocol is now free from interference. An exciting application of the ideas of non-interference to safety properties of railway signalling is being developed in collaboration with British Rail and the Smith Institute using a CASE studentship. This has led to a substantial number of publications [S95,SW9Sa,SW9Sb]. [R95a] A.W. Roscoe. CSP and determinism in security modelling. (To appear) in the proceedings of 1995 IEEE Symposium on Security and Privacy. [R95b] A Roscoe. Prospects for describing, specifying and verifying Key-exchange protocols in CSP and FDR Formal Systems Technical Report, December 1994. [R9Sc] A.W. Roscoe. Modelling and verifying key-exchange protocols using CSP and FDR. Submitted for publication. [RWWu94] A.W.Roscoe J.C.P. Woodcock and L Wulf.Non-interference through determinism. Proc. ESORICS 94, Springer LNCS 875, pp33-53. [RWu95] A.W. Roscoe and L Wulf.Composing and decomposing systems under security properties. Submitted for publication. [S95a] A.C. Simpson.Railway Signalling as a case Study in Safety through Determinism. (To be presented at) Aspect '95, 1995. [S95b] A.C. Simpson. The Application of Formal Methods to the Development of an ATP (Automatic Train Protection) System , IEE Colloquium on Communication Networks in Transportation, January 1995. [SW95] A.C Simpson and J.C.P. Woodcock,Safety through Security.(To be presented to) IFIP Working Group, March 1995. Preprints of all papers are available from the P.I.s
|
|
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.ox.ac.uk |