BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//LORIA - ECPv6.15.18//NONSGML v1.0//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-WR-CALNAME:LORIA
X-ORIGINAL-URL:https://www.loria.fr
X-WR-CALDESC:Évènements pour LORIA
REFRESH-INTERVAL;VALUE=DURATION:PT1H
X-Robots-Tag:noindex
X-PUBLISHED-TTL:PT1H
BEGIN:VTIMEZONE
TZID:Europe/Paris
BEGIN:DAYLIGHT
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
DTSTART:20240331T010000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
DTSTART:20241027T010000
END:STANDARD
BEGIN:DAYLIGHT
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
DTSTART:20250330T010000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
DTSTART:20251026T010000
END:STANDARD
BEGIN:DAYLIGHT
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
DTSTART:20260329T010000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
DTSTART:20261025T010000
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20251211T093000
DTEND;TZID=Europe/Paris:20251211T123000
DTSTAMP:20260405T215258
CREATED:20251118T104257Z
LAST-MODIFIED:20251118T124900Z
UID:28645-1765445400-1765456200@www.loria.fr
SUMMARY:Soutenance de thèse d'Élise Klein
DESCRIPTION:Élise Klein (Pesto)\, défendra sa thèse intitulée \nFormal Verification in Practice:\nReal-World Case Study and Enhanced Support for AC Operators in Tamarin .\nLa soutenance aura lieu en public le jeudi 11 décembre à 9h30\, au LORIA\, en salle A008. Elle sera suivie d’un pot. \nJury :\n\n Yannick Chevalier (rapporteur — MCF HDR à l’Université de Toulouse)\n Barbara Fila (rapportrice — MCF HDR à l’INSA de Rennes)\n David Baelde (examinateur — Prof ENS Rennes)\n Claudia Ignat (examinatrice — DR INRIA au Centre Inria de l’Université de Lorraine et LORIA)\n Ioana Boureanu (examinatrice — Prof University of Surrey\, UK)\n Steve Kremer (Directeur de thèse — DR INRIA au Centre Inria de l’Université de Lorraine et LORIA)\n Jannik Dreier (Directeur de thèse — MCF Université de Lorraine)\n\n  \nAbstract: \n« During my PhD\, I studied the Tamarin-prover\, a cryptographic protocol verification tool\, initially focusing on modeling and later on improving its internal mechanisms. I first used the Sapic+ platform\, integrated into Tamarin\, to model the draft 12 of the LAKE-EDHOC protocol\, designed for deployment on IoT devices. Sapic+ enables the translation of a single model into three different tools (Tamarin\, ProVerif\, and DeepSec)\, allowing us to leverage the strengths of each. This approach led to the discovery of several vulnerabilities\, and our proposed fixes were integrated into subsequent versions of the protocol. Later\, I extended Tamarin to support user-defined associative and commutative symbols. To achieve this\, I designed an algorithm along with new reduction rules to handle infinite chains of constructors/destructors\, which often arise from such symbols. This extension enabled the modeling of new cryptographic primitives\, such as re-encryption. » \nRésumé : \n » Durant ma thèse\, j’ai étudié le prouveur Tamarin\, un outil de vérification de protocoles cryptographiques\, en me concentrant d’abord sur la modélisation puis sur l’amélioration de ses mécanismes internes. J’ai d’abord utilisé la plateforme Sapic+\, intégrée à Tamarin\, pour modéliser la version 12 du protocole LAKE-EDHOC\, conçu pour être déployé sur des objets connectés. Sapic+ permet de traduire un même modèle vers trois outils différents (Tamarin\, ProVerif et DeepSec)\, ce qui nous permet de tirer parti des forces de chacun. Cette approche a conduit à la découverte de plusieurs vulnérabilités\, et les correctifs que nous avons proposés ont été intégrés dans les versions ultérieures du protocole. Par la suite\, j’ai intégré à Tamarin la prise en charge des symboles associatifs et commutatifs définis par l’utilisateur. Pour ce faire\, j’ai conçu un algorithme ainsi que de nouvelles règles de réduction pour gérer les chaînes infinies de constructeurs/destructeurs\, qui apparaissent souvent avec de tels symboles. Cette extension a permis la modélisation de nouvelles primitives cryptographiques\, telles que le rechiffrement. « 
URL:https://www.loria.fr/event/soutenance-de-these-delise-klein/
LOCATION:Loria
CATEGORIES:Soutenance
END:VEVENT
END:VCALENDAR