Paul Laurent

Doctorant CNRS en vérification formelle

Paul Laurent, doctorant CNRS à l'IRISA, Rennes : vérification formelle de protocoles cryptographiques avec ProVerif. Thèse, parcours et projets.

  • Doctorat

    CNRS · IRISA, 2026-2029

    Thèse de doctorat sur la vérification formelle de protocoles en présence d'opérateurs associatifs-commutatifs

    • Dans l'équipe SPICY de l'IRISA, à Rennes
    • Travail sur ProVerif, un outil de vérification automatique de protocoles
    • Dirigée par Stéphanie Delaune et co-encadrée par Vincent Cheval

  • Master recherche

    INSA Rennes, 2025-2026

    Master Sciences InFormatiques (SIF)

    • Master recherche commun à l'Université de Rennes, l'ENS Rennes, CentraleSupélec et l'INSA Rennes
    • master.irisa.fr

  • Diplôme d'ingénieur

    INSA CVL, 2021-2026

    Diplôme d'ingénieur, département Sécurité des Technologies de l'Information

    • Deux ans de prépa intégrée puis trois ans de cycle ingénieur
    • Option méthodes formelles pour la cybersécurité en 4e année
    • Option arts plastiques pendant deux ans

  • Paper Centurion

    Une application web pour convertir des modèles 3D en patrons de papier à découper, plier et coller

    • Le patron s'exporte en PDF, avec les languettes de collage
    • Fonctionne dans le navigateur, sans rien installer

  • Centurion Scrabble

    Un Scrabble en français, à jouer dans le navigateur contre une IA ou à deux

    • Cinq niveaux d'adversaire, du débutant au joueur de club
    • Pour jouer à deux, il suffit d'envoyer un lien, sans créer de compte

  • Centurion Poker

    Un Texas hold'em en français, à jouer dans le navigateur contre des IA ou entre amis

    • Cinq niveaux d'adversaire, du débutant qui paie pour voir au joueur qui calcule tout
    • Jusqu'à six à la même table, il suffit d'envoyer un lien

  • Stage de M2

    IRISA, équipe LogicA, 2026

    Formaliser l'abstraction entre systèmes et attaques pour la synthèse d'arbres d'attaque

    • Relier formellement une attaque sur un système abstrait à ses déclinaisons sur des systèmes plus concrets
    • En tirer des bibliothèques de raffinements, à partir desquelles synthétiser des arbres d'attaque
    • Stage de master dans l'équipe LogicA, encadré par Sophie Pinchinat

  • Stage de M1

    IRT SystemX, Palaiseau, 2025

    Génération automatisée de scénarios de conduite à partir de simulations

    • Repérer des situations de conduite dans des simulations de trafic, pour tester des véhicules autonomes
    • Dans le cadre du projet européen SYNERGIES

  • PhD

    CNRS · IRISA, 2026-2029

    PhD on the formal verification of protocols in the presence of associative-commutative operators

    • In the SPICY team at IRISA, in Rennes
    • Work on ProVerif, an automatic protocol verification tool
    • Supervised by Stéphanie Delaune, co-supervised by Vincent Cheval

  • Research master

    INSA Rennes, 2025-2026

    Research Master in Computer Science (SIF)

    • Joint research master between the University of Rennes, ENS Rennes, CentraleSupélec and INSA Rennes
    • master.irisa.fr

  • Engineering degree

    INSA CVL, 2021-2026

    Engineering degree, Information Technology Security department

    • Two years of integrated prep, then three years of engineering
    • Formal methods for cybersecurity option in the fourth year
    • Fine arts option for two years

  • Paper Centurion

    A web app that turns 3D models into paper patterns to cut out, fold and glue

    • Exports the pattern as a PDF, with glue tabs
    • Runs in the browser, nothing to install

  • Centurion Scrabble

    French Scrabble in the browser, against an AI or with a friend

    • Five levels of opponent, from beginner to club player
    • To play with a friend, just send them a link, no account needed

  • Centurion Poker

    Texas hold'em in the browser, against AIs or with friends

    • Five levels of opponent, from the beginner who calls too much to the player who works everything out
    • Up to six at the same table, just send a link

  • M2 internship

    IRISA, LogicA team, 2026

    Formalising abstraction between systems and attacks for attack tree synthesis

    • Formally relating an attack on an abstract system to its counterparts on more concrete systems
    • Deriving libraries of refinements from it, from which attack trees can be synthesised
    • Master's internship in the LogicA team, supervised by Sophie Pinchinat

  • M1 internship

    IRT SystemX, Palaiseau, 2025

    Automated generation of driving scenarios from simulations

    • Finding driving situations in traffic simulations, to test self-driving cars
    • Part of the European project SYNERGIES

GitHub