Arthur Gontier

Présentation

Depuis janvier 2024, je suis chercheur postdoctoral à l’université de Glasgow, dans la section FATA. Je travaille avec Ciaran McCreesh, Matthew McIlree et le groupe VeriPB sur des solveurs certifiants, c’est-à-dire des solveurs d’optimisation sous contraintes qui génèrent une preuve vérifiable de leur raisonnement.

Auparavant, j’ai effectué ma thèse sur la cryptanalyse symétrique à l’aide de langages déclaratifs. J’ai utilisé des solveurs de contraintes, de programmation linéaire et de satisfiabilité booléenne, mais aussi des algorithmes dédiés, pour trouver des caractéristiques différentielles ou monter des attaques par cube, par exemple. Je travaillais dans l’équipe CAPSULE à Rennes, encadré par Stéphanie Delaune, Patrick Derbez et Charles Prud’homme.

Avant cela, j’ai obtenu le master Optimisation et recherche opérationnelle à Nantes et à Bruxelles, et j’ai effectué plusieurs stages de recherche sur l’optimisation multi-objectif, l’analyse statique de programmes et les explications en programmation par contraintes.

Thèmes de recherche

• Génération de preuves pour les solveurs d’optimisation sous contraintes. Faire en sorte qu’un solveur justifie chacune de ses déductions, afin que ses réponses puissent être vérifiées indépendamment. Je travaille actuellement sur la simplification des preuves VeriPB, pour rendre leur vérification praticable, mais aussi pour expliquer les raisonnements critiques des solveurs.
• Solveurs génériques pour la cryptanalyse. Modéliser des propriétés cryptographiques pour les résoudre avec des solveurs peut mener à de nouvelles découvertes. De plus, si ces solveurs sont certifiants, on peut en déduire des preuves de sécurité.
• Analyse de conflits, explications et génération de preuves. Démocratiser l’utilisation des explications de conflits et des justifications de propagation, en générant des explications pour les contraintes globales à partir de leurs décompositions et en externalisant les justifications des propagateurs.
• Outils génériques de cryptanalyse. J’ai contribué à TAGADA, un outil où chacun peut modéliser un chiffrement par blocs et en obtenir automatiquement la cryptanalyse différentielle. Ce genre d’outil est précieux pour automatiser et accélérer la cryptanalyse.

Publications

Conférences internationales à comité de lecture

1. Trimming pseudo-Boolean proofs Berhan Oumer Adame, Bart Bogaerts, Benjamin Bogø, Simon Dold, Arthur Gontier, Wietze Koops, Ciaran McCreesh, Matthew McIlree, Jakob Nordström, Andy Oertel, Adrian Rebola‑Pardo, Mark Turnbull Formal Methods in Computer-Aided Design (FMCAD 2026), Graz, Autriche, 14–18 septembre 2026 — accepté pour publication pdf code
2. Faster certified symmetry breaking using orders with auxiliary variables Markus Anders, Bart Bogaerts, Benjamin Bogø, Arthur Gontier, Wietze Koops, Ciaran McCreesh, Magnus O. Myreen, Jakob Nordström, Andy Oertel, Adrian Rebola‑Pardo, Yong Kiam Tan. 40th AAAI Conference on Artificial Intelligence (AAAI 2026), 2026 pdf code
3. A CP-based automatic tool for instantiating truncated differential characteristics François Delobel, Patrick Derbez, Arthur Gontier, Loïc Rouquette, Christine Solnon International Conference on Cryptology in India (INDOCRYPT 2023), pages 247–268, Springer, 2023 pdf slides code
4. New algorithm for exhausting optimal permutations for generalized Feistel networks Stéphanie Delaune, Patrick Derbez, Arthur Gontier, Charles Prud'homme Progress in Cryptology – INDOCRYPT 2022, LNCS 13774, pages 103–124, Springer, 2022 pdf slides exposé code
5. A simpler model for recovering superpoly on Trivium Stéphanie Delaune, Patrick Derbez, Arthur Gontier, Charles Prud'homme Selected Areas in Cryptography – SAC 2021, LNCS 13203, pages 266–285, Springer, 2021 pdf slides exposé code

Workshops et congrès nationaux

1. Diffusion totale dans le schéma de Feistel généralisé Stéphanie Delaune, Patrick Derbez, Arthur Gontier, Charles Prud'homme ROADEF 2022, 23^e congrès annuel de la Société française de recherche opérationnelle et d’aide à la décision, Villeurbanne – Lyon, France, février 2022 pdf slides
2. Conflict analysis in CP solving: explanation generation from constraint decomposition Arthur Gontier, Charlotte Truchet, Charles Prud'homme Workshop « From Constraint Programming to Trustworthy AI » de CP 2020, 26th International Conference on Principles and Practice of Constraint Programming, Louvain-la-Neuve, Belgique, septembre 2020 pdf slides code

Exposés invités

1. Trimming pseudo-Boolean proofs International Workshop on Highlights in Organizing and Optimizing Proof-logging Systems (WOOPS) 2026 slides
2. Progress on VeriPB proof trimming International Workshop on Highlights in Organizing and Optimizing Proof-logging Systems (WOOPS) 2025 slides exposé
3. First results on VeriPB proof trimming International Workshop on Highlights in Organizing and Optimizing Proof-logging Systems (WOOPS) 2024 slides exposé

Thèse de doctorat

1. Utilisation de solveurs génériques pour la cryptanalyse de chiffrements symétriques Arthur Gontier Thèse de doctorat, université de Rennes, 2023 pdf slides soutenance

Enseignement

Contact