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


Pilots for the European Cybersecurity Competence Networks: how can your SME benefit? - 6th Webinar -

The four pilot projects involved in the development of the European Cybersecurity Competence Network will present their plans and upcoming tools and services for SMEs in the webinar on the 2nd of April, 10:00 AM CEST



Future Events

Cyber Insurance and its Contribution to Cyber Risk Mitigation - Leiden March 25-29
25/03/2019 to 29/03/2019

The rise in both the scale and severity of recent cyberattacks demands new thinking about cybersecurity risk and the mitigation and transfer of that risk. Cyber insurance is one potential way to manage risk by transferring damage liability, but the cyber insurance market is immature and the understanding and actuarial knowledge of cyber-risk is currently underdeveloped.

e-SIDES workshop 2019

e-SIDES workshop: Towards Value-Centric Big Data: Connect People, Processes and Technology


2 April 2019

10am to 4pm


e-SIDES is a research project funded by European Commission H2020 Programme that deals with the ethical, legal, social and economic implications of privacy-preserving technologies in different big data context.