SEQUOIA: Security properties, process equivalences and automated verification

01/01/2014 to 31/12/2018

Most security protocol analysis tools are restricted to analyzing reachability properties while many security properties need to be expressed in terms of some process equivalence. The increasing use of observational equivalence as a modeling tool shows the need for new tools and techniques that are able to analyze such equivalence properties. The aims of this project are:

  • To investigate which process equivalences-among the plethora of existing ones-are appropriate for a given security property, system assumptions and attacker capabilities;
  • To advance the state-of-the-art of automated verification for process equivalences, allowing for instance support for more cryptographic primitives, relevant for case studies;
  • To study protocols that use low-entropy secrets expressed using process equivalences;
  • To apply these results to case studies from electronic voting.
Monday, 29 October, 2018


Outcomes and key themes from ICT 2018 Session on Cybersecurity as key for a Digital Economy and Society

On 5 December 2018, the Digital Single Market of the European Commission sponsored a session on the topic of “Cybersecurity as key for a Digital Economy and Society”. The highly-popular session (over 90 attendees) took place on 5 December 2018 within the flagship ICT2018 Conference in Vienna, Austria.

Khalil Rouhana, Deputy Director General, EC – DG CNECT, kicked off the session with an overview of some of the most pressing issues of the day in cybersecurity: