le 16 mars 2023 à 14:00
Des protocoles cryptographiques partout - Sommes-nous bien protégés ?
Les protocoles de sécurité sont largement utilisés aujourd’hui pour sécuriser les transactions qui ont lieu sur des canaux publics comme l’internet. Les fonctionnalités typiques sont le transfert d’un numéro de carte de crédit ou l’authentification d’un utilisateur sur un système. En raison de leur omniprésence croissante dans de nombreuses applications importantes (par exemple, le commerce électronique, les smartphones, les cartes d’identité délivrées par le gouvernement…), un défi de recherche très important consiste à développer des méthodes et des outils de vérification pour accroître notre confiance dans les protocoles de sécurité, et donc dans les applications qui s’appuient sur eux.
Les méthodes symboliques formelles offrent un moyen d’analyser soigneusement les protocoles de sécurité grâce au développement de techniques de preuve et d’outils spécifiques, par exemple ProVerif et Tamarin. Ces méthodes s’appuient sur des techniques de vérification de modèles, de raisonnement automatisé et de théorie de la concurrence. Nous expliquerons comment les protocoles de sécurité ainsi que les propriétés de sécurité qu’ils sont censés atteindre sont formalisés dans ces modèles symboliques. Nous passerons en revue les résultats existants et soulignerons leurs principales limites. Ensuite, nous présenterons brièvement le prouveur Squirrel, un outil interactif récent développé en partie par l’équipe Spicy. Cet outil est basé sur le modèle dit computationnel et offre des garanties de sécurité plus fortes que celles obtenues dans le cadre symbolique.
En savoir plus...Amphi Ircica – 50 avenue Halley – Haute Borne – Villeneuve d’Ascq
français
English