SEQUOIA: Security properties, process equivalences and automated verification

Home » 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


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