Classification, Formalization and Automatic Verification of Untraceability in RFID Protocols

Les protocoles sécurité RFID sont des sous-ensembles des protocoles cryptographiques mais avec des fonctions cryptographiques légères. Leur objectif principal est l'identification à l'égard de certaines propriétés de intimité comme la non-traçabilité et la confidentialité de l'avant. La intimité est un point essentielle de la société d'aujourd'hui. Un protocole d'identification RFID devrait non seulement permettre à un lecteur légitime d'authentifier un tag, mais il faut aussi protéger la intimité du tag. Des failles de sécurité ont été découvertes dans la plupart de ces protocoles, en dépit de la quantité considérable de temps et d'efforts requis pour la conception et la mise en œuvre de protocoles cryptographiques. La responsabilité de la vérification adéquate devient cruciale. Les méthodes formelles peuvent jouer un rôle essentiel dans le développement de protocoles de sécurité fiables. Les systèmes critiques qui nécessitent une haute fiabilité tels que les protocoles de sécurité sont difficiles à évaluer en utilisant les tests conventionnels et les techniques de simulation. Cela a eu comme effet de concentrer les recherches sur les techniques de vérification formelle de tels systèmes pour assurer un degré élevé de fiabilité. Par conséquent, certaines recherches ont été faites dans ce domaine, mais une définition explicite de certaines de ces propriétés de sécurité n'ont pas encore été donnée. L'objectif principal de cette thèse est de démontrer l'utilisation de méthodes formelles pour analyser les propriétés de intimité du protocole RFID. Plusieurs définitions sont données dans la littérature pour les propriétés non-traçabilité, mais il n'y a pas d'accord sur sa définition exacte. Nous avons introduit trois niveaux différents pour cette propriété en ce qui concerne les expériences de intimité existantes. Nous avons également classé toutes les définitions existantes avec différents points forts de la propriété non-traçabilité dans la littérature. De plus, notre approche utilise spécifiquement les techniques de calculs de processus pi calcul appliqués pour créer un modèle pour un protocole. Nous démontrons les définitions formelles de nos niveaux de non-traçabilité proposées et l'applique à des études de cas sur les protocoles existants.