The security of a system is based above all on the quality of its primitives and on the way they are assembled to form protocols. While the knowledge of primitive analysis is very advanced, the maturity of the protocol design domain is far below expectations. Breakage and repairs are thus the daily routine of the protocols. In the hyperconnected context of our information systems, the SVP project’s objective is to allow the analysis of protocols deployed or in the process of being deployed, both at the level of the specifications of these protocols and of their implementations. We wish to develop techniques and tools that allow the implementation of solutions whose security will no longer be questioned in a cyclical manner.
To meet this challenge, building on the work already done in the formal methods for security community on protocol verification, our project requires several steps, among which :
- develop new functionalities in the existing tools to allow the analysis of more and more complex protocols ;
- build bridges between the different existing techniques and associated tools in order to take advantage of the strengths of each of them ;
- validate the techniques and tools developed in the framework of this project on already widely deployed protocols, and on more recent, fast-growing applications, such as Internet voting.