GT MFS 2023 - Sciencesconf.org

Keynote - Formally verified compilation, security and faults

David Monniaux

Coffee break

Tools for Protocol Analysis

chair: Guillaume Scerri

› Enhancing Automation in Tamarin - Maïwenn Racouchot, Loria, Inria Nancy 10:30-10:55 (25min)

› Systematic translation of Cryptographic Axioms by Bi-deduction - Justine Sauvage, Inria de Paris 10:55-11:20 (25min)

› Unrestricting restrictions in ProVerif - Vincent Cheval, Inria Paris, Prosecco 11:20-11:45 (25min)

Lunch

Protocol Analysis

chair: Alexandre Debant

› Conception et vérification d'un protocole de vote par correspondance - Léo Louistisserand, Ecole Normale Supérieure Paris-Saclay 14:15-14:40 (25min)

› Attacking and Fixing Protocols using Exponentiation Mix-Net Automatically with Refined Models - Dhekra Mahmoud, Laboratoire dÍnformatique, de Modélisation et dÓptimisation des Systèmes - Jannik Dreier, Proof techniques for security protocols - Pascal Lafourcade, Laboratoire dÍnformatique, de Modélisation et dÓptimisation des Systèmes 14:40-15:05 (25min)

Program Verification

chair: Frédéric Besson

› Quantization for opaque predicate location. - Alexandre Gonzalvez, Institut de Recherche en Informatique et Systèmes Aléatoires 15:05-15:30 (25min)

› StarMalloc: A Modern, Security-Oriented Verified Memory Allocator - Antonin Reitz, Inria Paris 15:30-15:55 (25min)

Coffee break

Tool Session

Banquet -- moved from Wednesday