SEQUOIA - Security Properties, Process Equivalences, and Automated Verification

Home » Services » Cybersecurity Cataloge » SEQUOIA - Security Properties, Process Equivalences, and Automated Verification
01/03/2015 to 28/02/2019


Modern society is becoming ever-more digitalized. In particular, electronic services provided over the internet are now standard tools for individuals to network, manage their bank accounts, and even vote in important elections. It is therefore critical to deploy strongly secure systems to accomplish these tasks, which present the dual challenge of being both of socio-economic importance, and highly complex.

While cryptographic protocols are implemented to attempt securing these procedures, design errors remain abundant, as recent examples of practical attacks on such systems demonstrate. It is thus important to further refine the necessary tools to verify the correctness of these protocols. A highly successful technique to accomplish this is to use symbolic analysis. Two particularly important features of this technique stand out: 1) it is well-suited to analyze complex systems and 2) it is amenable to automation.

The aim of this project is to extend the capabilities of symbolic analysis so as to capture the subtle security properties of modern-day cryptographic protocols. Many of these properties can be expressed in terms of indistinguishabilty of processes, a notion that symbolic analysis currently lacks the necessary theoretical foundations to fully understand, and automated tools to verify. The technical objective is to begin filling this gap.

Examples of concrete security properties that indistinguishability naturally captures include anonymity, unlinkability, maximal protection of weak secrets such as passwords, and more. The main practical objective of the project is to provide an automated tool (using AKISS – Active Knowledge In Security protocolS - as a starting point) allowing the verification of indistinguishability, and therefore of the above-mentioned properties. We plan to illustrate our findings by performing an analysis on an e-voting protocol that actually relies on several of these properties.

Tuesday, 8 January, 2019


On 18 July 2019, will organize a webinar in collaboration with the GDPR Cluster projects entitled “GDPR compliance in the emerging technologies”.

Future Events

The 14th International Conference on Availability, Reliability and Security (ARES 2019), will be held from August 26 to August 29, 2019 at the University of Kent, Canterbury, UK.

26/08/2019 to 29/08/2019

PROTECTIVE is co-organising the 2nd International Workshop on Cyber Threat Intelligence Management(CyberTIM 2019) as apart of the ARES 2019 conference in the UK on 26-29 August 2019.

26/08/2019 to 29/08/2019