CLASSIFICATION, FORMALIZATION AND AUTOMATIC VERIFICATION OF UNTRACEABILITY IN RFID PROTOCOLS
Ali Khadem Mohtaram · 2013
Resume Les protocoles securite RFID sont des sous-ensembles des protocoles cryptographiques mais avec des fonctions cryptographiques legeres. Leur objectif principal est l'identification a l'egard de certaines proprietes de intimite comme la non-tracabilite et la confidentialite de l'avant. La intimite est un point essentielle de la societe d'aujourd'hui. Un protocole d'identification RFID devrait non seulement permettre a un lecteur legitime d'authentifier un tag, mais il faut aussi proteger la intimite du tag. Des failles de securite ont ete decouvertes dans la plupart de ces protocoles, en depit de la quantite considerable de temps et d'efforts requis pour la conception et la mise en œuvre de protocoles cryptographiques. La responsabilite de la verification adequate devient cruciale. Les methodes formelles peuvent jouer un role essentiel dans le developpement de protocoles de securite fiables. Les systemes critiques qui necessitent une haute fiabilite tels que les protocoles de securite sont difficiles a evaluer en utilisant les tests conventionnels et les techniques de simulation. Cela a eu comme effet de concentrer les recherches sur les techniques de verification formelle de tels systemes pour assurer un degre eleve de fiabilite. Par consequent, certaines recherches ont ete faites dans ce domaine, mais une definition explicite de certaines de ces proprietes de securite n'ont pas encore ete donnee. L'objectif principal de cette these est de demontrer l'utilisation de methodes formelles pour analyser les proprietes de intimite du protocole RFID. Plusieurs definitions sont donnees dans la litterature pour les proprietes non-tracabilite, mais il n'y a pas d'accord sur sa definition exacte. Nous avons introduit trois niveaux differents pour cette propriete en ce qui concerne les experiences de intimite existantes. Nous avons egalement classe toutes les definitions existantes avec differents points forts de la propriete non-tracabilite dans la litterature. De plus, notre approche utilise specifiquement les techniques de calculs de processus pi calcul appliques pour creer un modele pour un protocole. Nous demontrons les definitions formelles de nos niveaux de non-tracabilite proposees et l'applique a des etudes 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.