Automated Reasoning for Security Protocol Analysis

People

Supervisor

Description

A security protocol is a sequence of message exchanges between parties in a network system, usually used to establish certain security targets such as authentication, exchanges of session keys, etc. Security protocols are often described informally, with many underlying assumptions about a possible attacker or intruder left implicit. Often such a description looks deceptively simple (typically a few lines of texts) and it is easy to overlook some implicit assumptions in its analysis. This has been the case for a number of well-known protocols in the literature, where flaws were discovered only when the intruder model was made explicit and precise.

A common, but coarse, abstraction of the capability of an intruder used in security protocol models is the so-called Dolev-Yao model, in which encryption is treated as a black box. In reality, the implementation of encryption functions is often done with operators that satisfy some algebraic properties, e.g., exclusive-Or (which satisfies the properties of an abelian group), homomorphic encryptions, or more advanced techniques based on elliptic curves.

In this project, we are investigating various formal models of intruders, based on formal logic and algebra, and how automated reasoning techniques can be developed for the analysis of security protocols under those models. This in turn will be used to develop a rigorous framework in which the corretness claims, or the existence of a flaw, of a security protocol can be stated precisely and proven mechanically.

Some potential research topics in this area:
(1) Exploring uses of state-of-the-art theorem provers for protocol verification: Some security properties, such as secrecy and authentication, can be encoded as statements in first-order logic. The encoding is such that attacks on a protocol correspond to proofs in first-order logic. Automated reasoning for first-order logic is well-developed and there are now a number of highly effective and mature theorem provers for first-order logic. We will explore various encoding techniques and experiments with using these first-order solvers to help proving security properties of protocols.
This is suitable for Honours/Masters level 2 semester project.

(2) Techniques for analysing algebraic properties in intruder models: Although encoding protocols in first-order logic may help solve security protocol analysis problems, since first-order logic is semi-decidable, first-order theorem provers may not always produce answers. This subproject will look at designing specific decision procedures for specific intruder models. This is suitable for PhD students.

(3) Scaling up protocol verification: automated protocol verification is essentially a search problem for an infinite state system. Most practical protocol verifiers will use some symbolic representation of states in their search. A natural question is whether this search procedure can be parallelised. This subproject will experiment with a number of state-of-the-art protocol verifiers, to evaluate their inherent support for parallelisation. A more advanced topic would be to modify existing verification algorithms to be more suitable for parallelisation. A collection of benchmarks, specific to protocol verification problems, will be produced. This is suitable for Honours/PhD levels.

(4) Modelling real-world protocols: This subproject involves surveying security protocols used in many different applied settings. Of particular interests are protocols for low-power devices, eg, IoT devices, implantable medical devices, and protocols in new standards, eg, 5G network protocols. We will model these protocols formally and verify their security properties. This is suitable for an Honours/Masters level project.

Requirements

Good programming skills, familiarity with logic and theoretic CS (eg, through completion of ANU COMP1600 course), and basics of crypto (eg, through completion of ANU COMP2700 course). 

 

 

Background Literature

Basics of security protocols:

Colin Boyd and Anish Mathuria. Protocols for Authentication and Key Establishment. Springer-Verlag, 2003.

 

Research papers:

- Danny Dolev, Andrew Chi-Chih Yao: On the Security of Public Key Protocols (Extended Abstract). FOCS 1981: 350-357. https://doi.org/10.1109/SFCS.1981.32

- Gavin Lowe: An Attack on the Needham-Schroeder Public-Key Authentication Protocol. Inf. Process. Lett. 56(3): 131-133 (1995). https://doi.org/10.1016/0020-0190(95)00144-2

- Véronique Cortier, Stéphanie Delaune, Pascal Lafourcade: A survey of algebraic properties used in cryptographic protocols. Journal of Computer Security 14(1): 1-43 (2006). http://content.iospress.com/articles/journal-of-co...

- Ton van Deursen, Sasa Radomirovic: Attacks on RFID Protocols. IACR Cryptology ePrint Archive 2008: 310 (2008). http://eprint.iacr.org/2008/310

- Peter Selinger: Models for an adversary-centric protocol logic. Electr. Notes Theor. Comput. Sci. 55(1): 69-84 (2001). https://doi.org/10.1016/S1571-0661(04)00245-2

 

 

 
 
 
 

 

 
  •  
  •  

 

Keywords

security protocol, first-order logic, theorem proving

 

Updated:  1 June 2019/Responsible Officer:  Dean, CECS/Page Contact:  CECS Marketing