Model-based Analysis of Security Protocols

Objectives:

To develop a practical framework for security protocol analysis and verification that will successfully integrate formal methods and object oriented modelling techniques.

Contact:

The contact for this research project is here.

PhD Thesis:

The research project has been summarized in a PhD thesis defended at the Gdansk University of Technology in November 2008.

Marcin Olszewski:
"An Integrated Framework for Security Protocols Analysis"

Rationale:

The ubiquity of Internet services requires secure means of communication between nodes in distributed IT systems. In particular each node must have means to verify the identity of its correspondent. Authentication protocols are usually used for this purpose. Standard approaches to ensuring the quality of IT products often prove insufficient for security protocols, as those are prone to subtle design errors. Far better results may be obtained by utilising formal methods - techniques based on mathematical principles thus offering high reliability of results.

However, the task of deriving a formal model of a security protocol specification is often a considerable challenge in it own right. Protocols used in practice are often quite complicated, and the analyst is required to come up with a formal model which represents all the significant characteristics of the protocol and at the same time is small enough to make formal inference feasible. Also a possibility of faults in the formalisation step must be taken into account. Therefore it is crucial to ensure the process of constructing formal models from informal specifications to be both, cost-effective and error free. The reliability of the results of protocol analysis also requires the formalisation step to be traceable - there should be no doubt whereas the formal model in question indeed represents the analysed protocol fully and accurately.

Approach:

The approach is to integrate a powerful informal modelling method (UML in our case) with a well-established formal method supported by matured tools (the chosen method is CSP). UML acts as a front-end which is used to capture the scope and the essence of the analysed problem and to represent it as a set of UML-based models. The models are then transformed into CSP specifications that are subsequently subjected to formal analyses.

Support for the CSP method is provided by two software tools: FDR (a commercial product) and Casper (freely available software).

The whole approach is packaged into a Model-based Security Protocol Analysis Framework - MSPAF. An integral part of the MSPAF is the object-oriented semi-formal approach to modelling of cryptographic protocols, their application context and security requirements. It is based on UML and includes a catalogue of specialised analytical patterns. The latter help to achieve a certain degree of standardisation and formalisation of object-oriented models developed while applying MSPAF. By using semi-formal UML models as an intermediate representation of a security protocol, the actual formalisation step proceeds more seamlessly. The models also provide an additional documentation material which helps to make the analysis more traceable.

It is also investigated how MSPAF can support the Trust Cases by providing additional evidence on the trustworthiness of the developer systems.

Schedule:

  • The project started in 2003.

  • In 2003 the first experiments with the MSPAF framework were carried out with respect to the selected protocols.

  • In 2004 the framework was applied with respect to a suite of protocols related to the deployment of electronic signature services.

  • In 2005-2006 the development of a system supporting the framework and validation experiments took place.
  • In 2008 the PhD thesis summarising the results was submitted for review.

Results:

At present the MSPAF approach was applied to analyze linear authentication and key exchange protocols. Three separate case studies confirmed gave promising results and have shown the usefulness of MSPAF in both, finding security faults in authentication protocols and in positively verifying their security properties. The ability to integrate MSPAF with the Trust Cases was investigated in relation to the 5th FP DRIVE project.

The ultimate goal is to be able to perform successful analyses of industry-grade protocols, designed for real distributed systems with specific security requirements. Specifications of such protocols are often very complex and lengthy (up to 100 pages), the protocols itself are sometimes of a compositional design - i.e. a larger protocol uses smaller ones as building blocks. This additional complexity has to be dealt with before the actual automated formal verification can proceed. Model based approach offers tools which may be able to solve this problem. Intermediate representations, step-by-step formalisation, well-defined documentation all help to overcome complexity and achieve traceability even for large analytical problems.

Publications:

  1. Olszewski M., Cyra L.: An integrated framework for security protocol analysis, Proceedings of Symposium on Information, Computer and Communications Security (ASIACCS'08), Tokyo, Japan, 18-20 March, 2008, pp. 77-86.

  2. Cyra L., Olszewski M.: Wykorzystanie programu AutoFocus do analizy protokołów kryptograficznych, 3rd National Conference on Information Technologies, Gdansk, Poland, 2006, pp. 639-646 (in Polish)

  3. Olszewski M.: A model-based approach to analysis of security protocols – a case study, Proceedings of IEEE International Conference on Technologies for Homeland Security and Safety (TEHOSS 2005), Gdańsk, Poland, September 28-30, 2005, pp. 221-226.

  4. Gorski J., Olszewski M.: A model-based approach to analysis of authentication protocols, Computer Information Systems and Applications vol. II, Proceedings of 11th Multi-conference on Advanced Computer Systems, Bialystok, Poland, 2004, pp. 229-239.

  5. Olszewski M.: Analiza protokołów uwierzytelniania z wykorzystaniem modelowania obiektowego i formalnego, 8th National Conference on Applied Cryptography ENIGMA 2004, Warszawa, Poland, 2004 (in Polish)

  6. Olszewski M.: A system facilitating security analysis of authentication protocols, MSc Dissertation, Gdansk University of Technology, Gdansk, Poland, September 2003.