LV-Pri20 · Logic-based Verification of Privacy-Preservation in Europe's 2020 ICT
Horizon 2020 — Marie Skłodowska-Curie Actions
- Duration
- 2015-06-22 → 2017-06-21
- EU contribution
- €195,455
- Participants
- 2
- Scheme
- MSCA-IF-EF-CAR
Lines connect the coordinator with its partners.
Results in brief
Logic-based Verification of Privacy-Preservation in Europe's 2020 ICT
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.
Data: CORDIS, © European Union
Project objective
In line with the EU 2020 Flagship Initiative on a Digital Agenda for Europe and the upcoming EU Cybersecurity Strategy, the goal of the LV-Pri20 project is to aid our ICT-driven lives, by “safeguarding the human right of privacy in the digital society”. Concretely, the main focus of LV-Pri20 is the formal and automatic analysis of privacy-preservation in today’s ICT. LV-Pri20 will focus on the prevalent wireless media, e.g., RF-identification protocols, remote car-unlocking, wearables, machine-to-machine communication in the Internet of Things (IoT)/ubiquitous computing, but it will not neglect wired environments (given their common cloud-connection). LV-Pri20 will assess and automatically analyse privacy-sensitive applications, in their standalone execution, as well as in the more involved setting of multiple, concurrent executions thereof. This will be done systematically and taxonomically: distinct classes of applications (e.g., identification protocols using Electronic Product Codes vs. the Open Smart Grid Protocol) and different privacy properties (e.g., data non-leakage vs. data-user unlinkability) will be respectively analysed via tailored, well-defined techniques. To specify privacy, LV-Pri20 will design/refine different non-classical logic languages which have inherent semantics for privacy-like expression (e.g., strategy logics). For these, we will then develop new model checking algorithms. All will be incorporated in automatic verification software, which already proved efficient in analysing highly distributed systems, inline with, e.g., the IoT applications envisaged herein.LV-Pri20 will have a multi-disciplinary, collaborative nature, an academic core and industrial side. After an initial privacy scrutiny, new/patched RFID-based, privacy-preserving, communication protocols will be (re-)designed and implemented. For these, we will devise mathematical proofs for one-session security, and run automatic analysis of their multi-session executions.
Original text from CORDIS.
Participants
- UNIVERSITY OF SURREY · GuildfordCoordinatorUnited Kingdom
- IMPERIAL COLLEGE OF SCIENCE TECHNOLOGY AND MEDICINE · LondonUnited Kingdom
Links
Data: CORDIS, © European Union