Modélisation et vérification des protocoles de sécurité avec le calcul Pi appliqué et ProVerif

Titre original :

Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif

Contenu du livre :

La vérification des protocoles de sécurité est un domaine de recherche actif depuis les années 1990. Ce sujet est intéressant pour plusieurs raisons.

Les protocoles de sécurité sont omniprésents : ils sont utilisés pour le commerce électronique, les réseaux sans fil, les cartes de crédit, le vote électronique, entre autres. La conception des protocoles de sécurité est notoirement sujette aux erreurs. Ces erreurs peuvent également avoir des conséquences graves.

C'est pourquoi la vérification formelle ou la preuve des protocoles est particulièrement souhaitable.

Cette étude se concentre sur la vérification des spécifications des protocoles dans le modèle symbolique. Bien qu'il soit assez abstrait, ce niveau de vérification est pertinent en pratique car il permet de découvrir de nombreuses attaques.

ProVerif est un vérificateur automatique de protocoles symboliques. Il prend en charge une large gamme de primitives cryptographiques, définies par des règles de réécriture ou par des équations. Il peut prouver diverses propriétés de sécurité : secret, authentification et équivalences de processus, pour un espace de messages non borné et un nombre non borné de sessions.

Il prend en entrée une description du protocole à vérifier dans un dialecte du calcul pi appliqué, une extension du calcul pi avec la cryptographie. Il traduit automatiquement cette description de protocole en clauses de Horn et détermine si les propriétés de sécurité souhaitées sont respectées par résolution sur ces clauses. Cette étude présente une vue d'ensemble de la recherche sur ProVerif et constitue le texte le plus complet disponible sur le sujet.

Autres informations sur le livre :

• ISBN : 9781680832068
• Auteur : Bruno Blanchet
• Éditeur : New Publ Inc
• Langue : anglais
• Reliure : Broché