login · source · print

TMSP: Trends in Mechanized Security Proofs

EUTypes WG4 meeting / Satellite workshop of FSCD 2017, Oxford, UK, 3 September 2017


Recent cyber attacks against the US election have shown: the more valuable a target the higher the likelihood that it will be attacked. Adversaries, in particular nation states, have nearly unlimited capacity to devise cyberattacks and exploit even the smallest vulnerabilities. And there is evidence for this. Voter registration systems in several US states were attacked during the months and weeks leading up to the US election. In contrast no evidence was found that voting machines, including DRE, optical scan machines, or result transmissions systems were actually tampered with -- yet. The challenge is clear: How can the security of such critical systems be improved efficiently and effectively. The challenge lies in the fact that these systems tend to be complex (using often advanced mathematics and statistical reasoning) and large (consisting of multiple communicating nodes that involve human operators).


  • the state of the art in mechanized security proofs
  • rich type systems for security
  • case studies in mechanized security proofs
  • the formal modeling and adequacy of threat models
  • security proofs in the symbolic model versus semantic security proofs

For this workshop we will invite leading experts in mechanized reasoning, protocol verification, and cyber security, to discuss how type-based proof assistant can be used to mechanize the analysis of security properties and voting protocols. Case studies will also be discussed. We will also invite private organizations, companies and that have a strong interest in identifying vulnerabilities early during the design process.

This workshop is funded by the EUTypes COST project (https://eutypes.cs.ru.nl/) and co-organised by the DemTech project

Invited Speakers

  • TBA

Program, Abstracts, Slides

  • TBA


  • Carsten Schürmann
  • Herman Geuvers