Â
Toutes nos félicitations à Jannik Dreier, maître de conférences à l’Université de Lorraine, enseignant à Telecom Nancy et chercheur au Loria (UMR CNRS – Université de Lorraine) et à ses confrères : David Basin (ETH Zurich), Cas Cremers (CISPA) et Ralf Sasse (ETH Zurich), lauréats du Prix Levchin 2026 !
Le Prix Levchin (« for Real-World Cryptography ») honore des innovations à fort impact dans la cryptographie et son utilisation dans des systèmes du monde réel. Il leur a été remis le 9 mars lors de Real-World Crypto Symposium à Taipei, conférence internationale majeure en cryptographie appliquée réunissant chaque année environ 600 professionnels académiques et industriels du domaine.
Ce prix prestigieux récompense les quatre chercheurs pour leurs travaux sur le développement du Tamarin Prover, un outil de vérification des protocoles cryptographiques, et son application aux protocoles cryptographiques industriels et du monde réel.
« Nous sommes très honorés d’avoir reçu ce prix. Au Real-World Crypto Symposium, de nombreux chercheurs et industriels recherchent et proposent des solutions pour appliquer la cryptographie dans la pratique. Le prix Levchin est une reconnaissance qui couronne plus d’une dizaine d’années de développement et d’amélioration de l’outil, et qui souligne l’impact concret et tangible de Tamarin dans la vraie vie, bien au-delà de la recherche fondamentale. »
Des avancées scientifiques pour la sécurité des protocoles cryptographiques
Au cours de la dernière décennie, les recherches sur le Tamarin Prover ont considérablement fait progresser l’état de l’art dans la vérification des protocoles cryptographiques. Elles ont permis de passer à l’échelle industrielle et d’atteindre un niveau de précision sans précédent dans l’analyse assistée par ordinateur de ces protocoles.
« Le travail sur Tamarin a commencé avec Cas Cremers, David Basin et deux doctorants, Simon Meier et Benedikt Schmidt, rejoint par Ralf Sasse et moi-même après. Aujourd’hui le projet a pris vraiment beaucoup d’ampleur, avec de nombreux contributeurs, notamment des doctorants et stagiaires du Loria, du CISPA et de l’ETH. » commente Jannik Dreier, chercheur au Loria dans l’équipe Pesto (Loria / Inria).
Tamarin offre à la fois une vérification automatique et une recherche de preuves guidée par l’utilisateur, à la manière des assistants de preuve interactifs. Tamarin peut être utilisé pour découvrir de nouvelles attaques, aider à concevoir des améliorations et fournir des preuves de correction.
« L’année dernière, nous avons également publié un livre sur Tamarin, conçu comme un guide pratique pour les utilisateurs. L’écriture de cet ouvrage nous a demandé 5 ans, mais nous espérons qu’il contribuera à la démocratisation des techniques de vérification. »
Tamarin a été utilisé pour analyser une grande variété de protocoles comme TLS 1.3, 5G-AKA, EMV, iMessage PQ3 et d’autres standards industriels. L’outil Tamarin est open source, librement accessible, et compte une base d’utilisateurs mondiale, tant dans le milieu académique qu’industriel : De nombreuses entreprises utilisent désormais Tamarin directement pour les protocoles qu’elles développent ou normalisent, par exemple chez Apple, Amazon, Cloudflare, Google, Mozilla, Ericsson, Huawei, Dfinity et SRI.
« Tamarin n’est pas réservé à la recherche ou à l’industrie : il est aussi utilisé dans l’enseignement, pour apprendre les techniques de vérification et de sécurisation de protocoles aux étudiants. J’utilise Tamarin dans mon cours sur la sécurité des protocoles cryptographiques à Telecom Nancy. J’accompagne ce cours d’un « championnat des protocoles », un évènement où les étudiants s’entraînent développer des protocoles, les analyser et détecter les failles dans les protocoles concurrents, manuellement et en utilisant Tamarin. »
Félicitation à toute l’équipe pour l’obtention de ce prix qui vient saluer plus de 10 années de recherche.
Â
Propos recueillis par le service communication du Loria
Pour aller plus loin :
