State-of-the-art technologies are struggling to keep pace with the variety of possible security vulnerabilities. There are few suitable guidelines or automated tools to design or analyze security protocols. Therefore, many protocols have security flaws and imperfections. The lack of a consistent methodology and tools for analyzing security protocols throughout the various stages of their design not only hinders the early detection, and therefore prevention, of security vulnerabilities, but it also complicates a subsequent comprehensive analysis of these protocols. Moreover, state-of-the-art verification tools typically only address particular narrow aspects of a protocol's security, and they require expert knowledge in current verification research; hence they do not help protocol designers.
The challenge of the ERC Starting Grant END2ENDSecurity is to develop a general methodology and tools for guaranteeing end-to-end security -- from high-level specifications of the desired security requirements for a given task, to a specification of a security protocol that relies on innovative cryptographic primitives, to a secure, executable program.
The ERC Starting Grant was concluded in 2014. We refer to the progress reports for a detailed exposition of its scientific achievements: