#	Pagina
attuale pagina	/open-h2020/projects/207596/results.html

Report

Teaser, summary, work performed and final results

Periodic Reporting for period 2 - POPSTAR (Reasoning about Physical properties Of security Protocols with an Application To contactless Systems)

Teaser

Summary

Whereas traditional security protocols achieve their security goals relying solely on cryptographic primitives like encryptions and hash functions, the protocols employed to secure contactless devices establish and rely in addition on properties of the physical world. For instance, they may use, as basic building blocks, protocols for ensuring physical proximity, secure localisation, or secure neighbourhood discovery.

The main objective of the POPSTAR project is to develop foundations and practical tools to analyse modern security protocols that establish and rely on physical properties. The POPSTAR project will significantly advance the use of formal verification to contribute to the security analysis of protocols that rely on physical properties. This project is bold and ambitious, and answers the forthcoming expectation from consumers and citizens for high level of trust and confidence about contactless nomadic devices.

Work performed

We provide an overview of the result obtained regarding the different tasks of the project.
Task 1/Task 2: Reasoning about physical properties.
We make some progress in this direction. In particular, we propose a model and a first reduction result for the analysis of distance bounding protocols. These results were obtained with Cyrille Wiedling (postdoc during the first months of the project) and a master student, Alexandre Debant, who started his PhD in Oct. 2017. Alexandre Debant is now working on an extension of an existing verification tool to take into account time and location.
We also extend an existing verification tool, namely Akiss, to deal with protocols that rely on the exclusive-or operator, a low-level operator often used in distance bounding protocols, and protocols that rely on short authenticated strings like e.g the 3D Secure protocol used in payment applications.
Task 3: Novel approaches for reasoning about trace equivalence.
We have made substantial progress on this task. We have proposed a procedure based on graph planning and SAT solving to check trace equivalence, and a prototype has been implemented. Our aim is now to enlarge the scope of the procedure in order to be able to analyse a larger class of protocols. Regarding the other approach based on sufficient conditions, SolÃ¨ne Moreau has been hired as a PhD student and has started to work on this topic since September 2018.
Task 4: Automated tool support.
We already made progress in this direction. In particular, we have proposed some partial order reduction techniques to improve the efficiency of verification procedures.
Task 5: Application to real-world contactless systems.
We study the specification of some real-world protocols such as the 3D-secure protocol but we did not conduct any practical experiment for the moment.

Final results

The POPSTAR project will develop fondations and practical tools to analyse modern security protocols that rely on physical properties. This will enable the detection of security flaws, and the development of general design principles to guarantee a high level of security in many applications that are carried out using contactless devices.