JFLA 2026

Electronic voting aims at guaranteeing apparently conflicting properties: no one should know how I voted and yet, I should be able to check that my vote has been properly counted. Electronic voting belongs to the large family of security protocols, that aim at securing communications against powerful adversaries that may read, block, and modify messages.

In this talk, we survey how voting protocols work through the example of the French Legislative elections in 2022. We will then see how to analyze them using formal methods and in particular ProVerif, in order to detect attacks at an early stage, or prove security, yielding a better understanding of the security guarantees and the threat model.

Iris est un système logique dédié à la vérification de programmes séquentiels et concurrents. Il est issu de la tradition des logiques dites de séparation, qui soulignent l’importance fondamentale du raisonnement local, c’est-à-dire la possibilité de comprendre et de vérifier chaque composant d’un système logiciel indépendamment des autres. On entend par là en particulier la possibilité d’analyser une fonction indépendamment de son appelant et un fil d’exécution indépendamment des autres fils qui s’exécutent de façon concurrente.

Deux des notions fondamentales qui rendent Iris particulièrement riche et flexible, car elles permettent à la fois raisonnement local à propos de chaque acteur et coordination entre l’ensemble des acteurs, sont l’état fantôme séparable et les invariants. Nous proposerons un aperçu de ces notions et de leurs applications. Nous illustrerons également l’utilisation d’Iris en tant que logique embarquée dans l’assistant de preuve Rocq.