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.

Abstract

RFID protocols are subsets of cryptographic protocols but with lightweight cryptographic functions. Their main objective is identification with respect to some privacy properties, like anonymity, untraceability and forward secrecy. Privacy is the essential part of today's society. An RFID identification protocol should not only allow a legitimate reader to authenticate a tag but also it should protect the privacy of the tag. Although design and implementation of cryptographic protocols are tedious and time consuming, security flaws have been discovered in most of these protocols. Therefore the responsibility for reliable and proper verification becomes crucial. Formal methods can play an essential role in the development of reliable security protocols. Critical systems which require high reliability such as security protocols are difficult to be evaluated using conventional tests and simulation techniques. This has encouraged the researchers to focus on the formal verification techniques to ensure a high degree of reliability in such systems. In spite of the studies which have been carried out in this field, an explicit definition for some of these security properties is still missing.