Report

Teaser, summary, work performed and final results

Periodic Reporting for period 1 - LV-Pri20 (Logic-based Verification of Privacy-Preservation in Europe\'s 2020 ICT)

Teaser

\"On the one hand, in the IoT, the computational constrains on devices often restrain security measures, making the communication more vulnerable to interception or manipulation. On the other, with the advent of cloud/edge-computing, today\'s communications are no longer based...

Summary

\"On the one hand, in the IoT, the computational constrains on devices often restrain security measures, making the communication more vulnerable to interception or manipulation. On the other, with the advent of cloud/edge-computing, today\'s communications are no longer based on traditional two-party protocols, but instead our data is intercepted, processed, stored and relayed (in original or modified form) by several \"\"middle-man\"\" entities such as corporate proxies, web filters, intruder-detection systems. These multi-party communications clearly pose a compound threat to the security/privacy of our communications and data.

So, firstly, Lv-Pri20 is addressing the verification of privacy-driven properties, such as anonymity in ICT/IoT systems.
Secondly, Lv-Pri20 is concerned with the verification and the provable security in multi-party, multi-hop, proxied communications, where the threat model is often more intricate than that of the two–party case.


Lv-Pri20’s Objectives:
Objective I has been the development of privacy-expressing formalisms to be used in the automatic verification of ICT/IoT systems; these formalisms were mainly based on applied logics.

Objective II has been the development of new algorithms and automatic tools for the verification of security and privacy properties, with a focus of privacy properties; these tools were mainly based on applied logics.

Objective III has been the analysis of classes of applications/systems, against their security and privacy properties with a focus on their privacy properties.

Objective IV has envisaged redesigning systems/applications that had been found vulnerable during the explorations undertaken to achieve the third objective, into versions that are provably secure. Where possible, prototype implementations of the new designs have been envisaged.
\"

Work performed

\"Firstly, we advanced new logic-based methods and tools for the automatic verification of the privacy of systems and programs (see publications A, E, F below). Secondly, where this was not possible (e.g., due to the cryptographic complexity of the systems at hand), we carried other type of analyses: formal proofs by hand on the security/privacy properties of systems (see publications B, C, D, G below).
The systems tackled are manifold: lightweight authentication systems (see publication D), C-like programs (see publication E), real-life authenticated key-exchange infrastructures based on every-day-use protocols like TLS (see publications C, G below).

Published work:
A. \"\"Verifying Security Properties in Unbounded Multiagent Systems\"\", by I. Boureanu, P. Kouvaros, A. Lomuscio, at the 15th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS), 2016.
B. \"\"Security of Distance-Bounding: A Survey\"\", by G. Avoine, M. A. Bingoel, I. Boureanu, S. Capkun, G. Hancke, S. Kardas, C. Kim, C. Lauradoux, B. Martin, J. Munilla, A. Peinado-Dominguez, K. Bonne Rasmussen, D. Singelee, A. Tchamkerten, R. Trujillo-Rasua, S.Vaudenay, in ACM Computing Surveys, Vol. 4, 2017
C. \"\"Content delivery over TLS: a cryptographic analysis of Keyless SSL\"\", by K. Bhargavan, I. Boureanu, P.A. Fouque, C. Onete and B. Richard, at the 2nd IEEE European Symposium on Security and Privacy (Euro S & P), 2017.
D. \"\"Breaking and Fixing the HB+DB protocol\"\", by I. Boureanu, D. Gerault, P. Lafourcade, C. Onete, at ACM WiSec, 2017
E. \"\"A Novel Symbolic Approach to Verifying Epistemic Properties of Programs\"\" by N. Giorgiannis, F. Raimondi, I. Boureanu, at the 26th International Joint Conference on Artificial Intelligence (IJCAI), 2017.

Under-review work:
F. On the verification of anonymity and strategic ability in ICT/IoT, using non-classical logics.
G. On the formal analysis and design of communication mediated by access-controlled proxies w.r.t. to security and privacy-related requirements.

\"

Final results

1. Publication A
We advanced the first formalism and tool based on temporal-epistemic logic that can express a security/privacy semantics, accounting for an unbounded number of participants (e.g., clients, servers, etc.) partaking in concurrent protocol-execution.

SOCIO-ECONOMIC IMPACT:
Our specification of privacy requirements is very natural. This can positively impact system analysts\' daily work.

Also, privacy-enhancing technologies like ours will likely see more commercialisation in the next 5 to 10 years; thus spin-offs and extensions of this work are expected to have an economical and societal impact.


2.Publication B
This is the first systematic and unitary security review of these IoT protocols (i.e., authenticated distance-bounding).

SOCIO-ECONOMIC IMPACT:
Our survey will benefit security researchers starting off in the field of proximity proofs.

We expect that two-factor lightweight authentication like distance-bounding protocols will soon become de-facto primitives in IoT. Commercial distance-bounding protocols (e.g., NXP’s Mifare) are closed designs, so our survey of academic ones could help new start-ups in this market.


3. Publication C
This work is the first to formally treat secured connections between a client and server, intermediated by a commissioned proxy.

SOCIO-ECONOMIC IMPACT
We exhibited attacks on Keyless SSL. This is a commercial, popular product by Cloudflare, which is the world’s 2nd biggest content delivery network (CDN).

We suggested provably secure patches to their design, as well as a new design to work for the up-coming TLS 1.3.

We discussed all these with Cloudflare.

Other companies contacted us to formally assess the security of their designs in this space.

One can envisage that our work could become part of some standardisation documents, in the space of CDN-ing over TLS.

Discussions in the paper about certain security/privacy requirements (e.g., accountability) can be an “eye-opener” for the segment of the society that is security-aware and privacy-conscious.


4. Publication D:
We put right an authenticated distance-bounding protocol called HB+DB.

SOCIO-ECONOMIC IMPACT:
As the lightweight authentication grows as an IoT necessity, the importance of this line also increases.

We also disproved certain experimentally-driven security measures for such IoT protocols.

Indeed, the fellow is now co-organising a workshop that will bring together practitioners, formal-methods’ academics, experimental scientists, to discuss this gap between practice and theory in the security and privacy of distance-bounding.


5. Publication E:
These results viewed the advancement of a new logic to express knowledge of agents “living” within a program expressed over logical facts about the program’s states and the “evolution” of this knowledge as the program executes.

This is the first work to consider the verification of privacy in programs, using epistemic logics, in that the previous works focused on modelling systems rather than programs.

Beyond the higher expressive power, the efficiency shown by our technique compared to existing verification tools exhibits a significant improvement over the state-of-the-art.

SOCIO-ECONOMIC IMPACT:
We believe that this work can push forward the practical verification of privacy-requirements, due (a) to its applicability to software and (b) to its efficiency.

Extensions of this work can be used in ICT/IoT certification, in the way of new legislation in this space like the up-coming GDPR, or inside new security platforms for privacy-conscious users.

Website & more info

More info: http://people.itcarlson.com/ioana/mc.html.