This thesis focuses on issues related to authentication in low-cost radio frequency identification technology, more commonly referred to as RFID. This technology it is often referred to as the next technological revolution after the Internet. However, due to the very limited resources in terms of computation, memory and energy on RFID tags, conventional security algorithms cannot be implemented on low-cost RFID tags making security and privacy an important research subject today. First of all, we investigate the scalability in low-cost RFID systems by developing a ns-3 module to simulate the universal low-cost RFID standard EPC Class-1 Generation-2 in order to establish a strict framework for secure identification in low-cost RFID systems. We show that, the symmetrical key cryptography is excluded from being used in any scalable low-cost RFID standard. Then, we propose a scalable authentification protocol based on our adaptation of the famous public key cryptosystem NTRU. This protocol is specially designed for low-cost RFID systems, it can be efficiently implemented into low-cost tags. Finally, we consider the zero-knowledge identification i.e. when the no secret sharing between the tag and the reader is needed. Such identification approaches are very helpful in many RFID applications when the tag changes constantly the field of administration. We propose two lightweight zero-knowledge identification approaches based on GPS and randomized GPS schemes. The proposed approaches consist in storing in the back-end precomputed values in the form of coupons. So, the GPS-based variant can be private and the number of coupons can be much higher than in other approaches thus leading to higher resistance to denial of service attacks for cheaper tags

La sécurité est une exigence cruciale dans les applications basées sur l'information et la technologie de communication, surtout quand un réseau ouvert tel que l'Internet est utilisé. Pour assurer la sécurité dans ces applications des protocoles cryptographiques ont été développé. Cependant, la conception de protocoles de sécurité est notoirement difficile et source d'erreurs. Plusieurs failles ont été trouvées sur des protocoles qui se sont prétendus sécurisés. Par conséquent, les protocoles cryptographiques doivent être vérifiés avant d'être utilisés. Une approche pour vérifier les protocoles cryptographiques est l'utilisation des méthodes formelles, qui ont obtenu de nombreux résultats au cours des dernières années.Méthodes formelles portent sur l'analyse des spécifications des protocoles modélisées en utilisant, par exemple, les logiques dédiés, ou algèbres de processus. Les méthodes formelles peuvent trouver des failles ou permettent de prouver qu'un protocole est sécurisé sous certaines hypothèses par rapport aux propriétés de sécurité données. Toutefois, elles abstraient des erreurs de mise en ouvre et les attaques side-channel.Afin de détecter ces erreurs et la vérification des attaques d'exécution peut être utilisée pour analyser les systèmes ou protocoles exécutions. En outre, la vérification de l'exécution peut aider dans les cas où les procédures formelles mettent un temps exponentielle ou souffrent de problèmes de terminaison. Dans cette thèse, nous contribuons à la vérification des protocoles cryptographiques avec un accent sur la vérification formelle et l'automatisation. Tout d'abord, nous étudions les protocoles d'examen. Nous proposons des définitions formelles pour plusieurs propriétés d'authentification et de confidentialité dans le Pi-calcul Appliqué.Nous fournissons également une des définitions abstraites de propriétés de vérifiabilité. Nous analysons toutes ces propriétés en utilisant automatiquement ProVerif sur plusieurs études de cas, et avons identifié plusieurs failles. En outre, nous proposons plusieurs moniteurs de vérifier les exigences d'examen à l'exécution. Ces moniteurs sont validés par l'analyse d'un exécutions d'examen réel en utilisant l'outil MARQ Java.Deuxièmement, nous proposons un cadre formel pour vérifier les propriétés de sécurité de protocoles de monnaie électronique non transférable. Nous définissons la notion de vie privée du client et les propriétés de la falsification. Encore une fois, nous illustrons notre modèle en analysant trois études de cas à l'aide ProVerif, et confirmons plusieurs attaques connues.Troisièmement, nous proposons des définitions formelles de l'authentification, la confidentialité et les propriétés de vérifiabilité de protocoles de réputation électroniques. Nous discutons les définitions proposées, avec l'aide de ProVerif, sur un protocole de réputation simple. Enfin, nous obtenons un résultat sur la réduction de la vérification de la validité d'une route dans les protocoles de routage ad-hoc, en présence de plusieurs attaquants indépendants qui ne partagent pas leurs connaissances. / Security is a crucial requirement in the applications based on information and communication technology, especially when an open network such as the Internet is used.To ensure security in such applications cryptographic protocols have been used.However, the design of security protocols is notoriously difficult and error-prone.Several flaws have been found on protocols that are claimed secure.Hence, cryptographic protocols must be verified before they are used.One approach to verify cryptographic protocols is the use of formal methods, which have achieved many results in recent years.Formal methods concern on analysis of protocol specifications modeled using, e.g., dedicated logics, or process algebras.Formal methods can find flaws or prove that a protocol is secure under ``perfect cryptographic assumption" with respect to given security properties. However, they abstract away from implementation errors and side-channel attacks.In order to detect such errors and attacks runtime verification can be used to analyze systems or protocols executions.Moreover, runtime verification can help in the cases where formal procedures have exponential time or suffer from termination problems.In this thesis we contribute to cryptographic protocols verification with an emphasis on formal verification and automation.Firstly, we study exam protocols. We propose formal definitions for several authentication and privacy propertiesin the Applied Pi-Calculus. We also provide an abstract definitions of verifiability properties.We analyze all these properties automatically using ProVerif on multiple case studies, and identify several flaws.Moreover, we propose several monitors to check exam requirements at runtime. These monitors are validated by analyzing a real exam executions using MARQ Java based tool.Secondly, we propose a formal framework to verify the security properties of non-transferable electronic cash protocols.We define client privacy and forgery related properties.Again, we illustrate our model by analyzing three case studies using ProVerif, and confirm several known attacks.Thirdly, we propose formal definitions of authentication, privacy, and verifiability properties of electronic reputation protocols. We discuss the proposed definitions, with the help of ProVerif, on a simple reputation protocol.Finally, we obtain a reduction result to verify route validity of ad-hoc routing protocols in presence of multiple independent attackers that do not share their knowledge.

Ce travail de thèse a été réalisé dans le cadre d'un contrat avec l'ANR (ANR-09-VERS-013 « THID ») et porte sur le développement d'une nouvelle génération de tags Chipless à bas coûts fonctionnant dans le domaine THz, pour des applications d'identification et/ou authentification unitaire des articles commerciaux, des papiers d'identités, des personnes pour le contrôle d'accès... Les structures proposées, constituées d'un empilement périodique de couches diélectriques d'indices de réfraction différents, utilisent les propriétés particulières des cristaux photoniques 1D de présenter une réponse électromagnétique entrecoupée de bandes interdites photoniques (BIP). Toute perturbation de la périodicité de la structure engendre des pics dans les bandes interdites qui sont utilisés pour coder une information binaire. Cette structuration particulière des matériaux permet donc de manipuler précisément une signature électromagnétique. Pour des raisons liées à l'industrialisation (facilité de fabrication en masse) et aussi de coût, nous avons retenu des matériaux de base déjà couramment utilisés dans l'industrie papetière : le papier et le polyéthylène. Le choix de ces matériaux, qui doivent allier contraste d'indice élevé et faible absorption, représente une étape cruciale dans ce travail. Ainsi, à partir des résultats expérimentaux obtenus par spectroscopie THz dans le domaine temporel (THz-TDS) sur un grand nombre de matériaux, nous avons pu concevoir deux familles de tags sur la base de ces différents matériaux. Par ailleurs, nous avons développé deux méthodes de codage d'une information binaire, toutes deux basées sur l'absence ou la présence de pics dans une BIP, pics dont la position et le nombre dépendent bien évidemment des défauts de périodicité introduits. Pour des applications liées à l'identification, des capacités de codage de près de 20 bits ont été démontrées. Nous avons aussi montré que la richesse d'information contenue dans la réponse électromagnétique de ces Tags THz peut être utilisée pour les applications liées à l'authentification unitaire, en utilisant comme critère de discrimination le coefficient d'autocorrélation. Nous avons ainsi pu évaluer les performances d'un test d'authentification basé sur ce critère dans différents domaines d'analyse : temporel, fréquentiel et temps-fréquence. Nous avons montré qu'une étude du spectrogramme (combinant temps et fréquence) est ainsi bien plus pertinente qu'une étude dans les seuls domaines temporel ou fréquentiel. / This thesis work deals with the development of a new generation of low-cost Chipless tags operating in the THz frequency domain, it has been supported by the french national agency for research (ANR-09-VERS-013 « THID » ). It covers a wide area of applications such as the identification and/or unitary authentication of commercial items, identity papers, access control…To manufacture these tags, we proposed to use a periodic stack of dielectric material layers with different refractive index and whose thickness is of the order of the wavelength, commonly known as a one dimensional photonic crystal. The electromagnetic signature of such a structure exhibits photonic bandgaps (PBG), i.e. frequency windows in which light propagation is prohibited. We suggested modifying the periodicity of the crystal to create defect levels (peaks) for example in the 1st PBG to encode binary information. This particular structure allows to precisely tuned an electromagnetic signature. To ensure a mass and cost effective industrialization, we retained basic materials which are widely used in the pulp and paper industry: paper and polyethylene. The choice of these materials, which must combine high index contrast and low absorption, represents the first and a crucial step in this work. We characterize a wide range of materials using classical THz time domain spectroscopy (THz-TDS) and we propose two families of tags based on paper and polyethylene. Furthermore, we developed two methods to encode binary information, both based on the absence or presence of peaks in a PBG, peaks whose number and position depend on the introduced defects of periodicity. In a real identification test, a coding capacity of nearly 20-bit has been demonstrated. We also showed that the information contained in the electromagnetic response of these THz tags can be used for other applications related to the unitary authentication and by using the correlation coefficient as criterion for discrimination of the different signatures. Therefore, we evaluate the performance of an authentication test based on this criterion in various analysis domains: time, frequency and time-frequency. We showed that a study of the spectrogram (combining time and frequency representation) is much more relevant than a study in the only time or frequency domain.

La croissance exponentielle dans l’utilisation du réseau Internet ainsi que l’apparition de nouveaux types d’applications ont augmenté les contraintes du réseau en termes de sécurité. Depuis quelques années, les techniques biométriques ont prouvé une grande précision et fiabilité et ont été utilisées dans plusieurs domaines afin de sécuriser l’accès à différentes ressources. Des solutions intégrant des agents et des systèmes multi-agents (SMA) ont aussi prouvé leur efficacité pour la résolution de nombreux problèmes dans les réeaux. Nous proposons un modèle « IrisCrptoAgentSystem » (ICAS) basé sur la méthode biométrique pour l’authentification utilisant l’iris de l’œil et la méthode de cryptographie asymétrique utilisant l’algorithme « Rivest-Shamir-Adleman » (RSA), et en intégrant des agents. Ce modèle doit assurer un accès sécurisé aux informations et garantir la protection des informations confidentielles. Notre travail porte sur la mise en place de nouvelles méthodes dans le modèle d’authentification biométrique afin de donner plus d’efficacité à notre modèle ICAS. Nous introduisons des aspects prétopologiques dans l’élaboration de la hiérarchie indexée pour classer les gabarits DHVA. Notre approche consiste à améliorer les méthodes relatives à la localisation des contours externe et interne de l’iris. / The exponential growth in the use of the Internet as well as the emergence of new types of applications has increased the network’s constraints in terms f security. Fort the last several years, biometric techniques have proven their applicability and reliability in providing secure access to shared resources in different domains. Furthermore, software agents and multi-agent systems (MAS) have evidently been efficient in resolving several problems in network. Therefore, the aim of this research is to propose a model “IrisCryptoAgentSystem” (ICAS) that is based on a biometric method for authentication using the iris of the eyes and an asymmetric cryptography method using “Rivest-Shamir-Adleman” (RSA) in an agent-based architecture. This model should provide secure access to information and ensure the protection of confidential information. Therefore, our work focuses on the development of new methods in biometric autheitcation in order to provide greater efficiency in the ICAS model. We introduce pretopological aspects in the development of the indexed hierarchy to classify DHVA templates. Our approach aims to improve the existing methods for the localization of the external and the internal edges of the iris.

Cette thèse aborde la conception et les contremesures permettant d'améliorer le calcul cryptographique matériel léger. Parce que la cryptographie (et la cryptanalyse) sont de nos jours de plus en plus omniprésentes dans notre vie quotidienne, il est crucial que les nouveaux systèmes développés soient suffisamment robustes pour faire face à la quantité croissante de données de traitement sans compromettre la sécurité globale. Ce travail aborde de nombreux sujets liés aux implémentations cryptographiques légères. Les principales contributions de cette thèse sont : - Un nouveau système d'accélération matérielle cryptographique appliqué aux codes BCH ; - Réduction de la consommation des systèmes embarqués et SoCs ; - Contre-mesures légères des attaques par canal auxiliaire applicables à l'algorithme de chiffrement reconfigurable AES ;- CSAC : Un pare-feu sécurisé sur la puce cryptographique ; - Attaques par analyse fréquentielle ; - Un nouveau protocole à divulgation nulle de connaissance appliquée aux réseaux de capteurs sans fil ; - OMD : Un nouveau schéma de chiffrement authentifié. / This thesis addresses lightweight hardware design and countermeasures to improve cryptographic computation. Because cryptography (and cryptanalysis) is nowadays becoming more and more ubiquitous in our daily lives, it is crucial that newly developed systems are robust enough to deal with the increasing amount of processing data without compromising the overall security. This work addresses many different topics related to lightweight cryptographic implementations. The main contributions of this thesis are: - A new cryptographic hardware acceleration scheme applied to BCH codes; - Hardware power minimization applied to SoCs and embedded devices; - Timing and DPA lightweight countermeasures applied to the reconfigurable AES block cipher; - CSAC: A cryptographically secure on-chip firewall; - Frequency analysis attack experiments; - A new zero-knowledge zero-knowledge protocol applied to wireless sensor networks; - OMD: A new authenticated encryption scheme.

Thesis describes design and implementation of a web browser game, which can be played by multiple players via the internet. The main goal is to manage the economy, although players can cooperate (trading) or play against each other (battles). NoSQL database is used for persistent storage of progress, which is also described in the thesis. Apart from human players there are also agents/bots, which play the game autonomously via state machines generated by genetic algorithms. Paper describes design and functionality of either the genetic algorithms, but also the state machines.

Les avancées technologiques permettent d'intégrer des capteurs et des modules de communication dans les objets du quotidien pour les rendre intelligents et faciliter leur intégration sur l'Internet. L'Internet du futur sera sans nul doute celui des objets connectés. Les objets connectés génèrent, collectent, stockent et partagent des informations entre eux et aussi avec les serveurs d'authentification centralisés. La plupart des informations collectées doivent être protégées pendant le stockage et le transfert. Par le passé, divers protocoles assurant une sécurité robuste basés sur la cryptographie asymétrique et d’autres sur la cryptographie symétrique ont été proposés dans la littérature. Du fait que les objets connectés possèdent de faibles capacités de calcul, de mémoire et d'énergie, et que l'accès au medium radio est très consommateur en ressources, les protocoles cryptographiques traditionnels ne sont pas adaptés aux objets connectés. Il y a lieu donc d'adapter ou de concevoir des protocoles propres et conformes à leurs exigences. Dans cette thèse, nous abordons les défis de sécurité et de vie privée pertinents aux systèmes pervasifs avec des contraintes de ressources strictes. Nous regardons les protocoles d'authentification serverless, qui sont des mécanismes d'authentification qui ne nécessitent pas la présence du serveur central au cours de la phase d'authentification entre deux objets connectés. Tout d'abord, nous fournissons les caractéristiques et les besoins pour les protocoles serverless. Grâce à ces besoins et caractéristiques, nous avons fait des recherches, des analyses complètes et des comparaisons des protocoles serverless existants en termes de sécurité, de vie privée et de performances. Nous examinons leurs capacités à résister à diverses attaques et leurs aptitudes à minimiser l’usage des ressources. Après quoi, notre objectif est de proposer des protocoles de sécurité serverless permettant aux objets de s’authentifier tout en garantissant efficacité, passage à l’échelle et efficacité énergétique, l'énergie étant une ressource très critique qui a une influence directe sur la durée de vie d’un objet connecté. Trois nouvelles contributions sont proposées dans cette thèse. Notre première contribution est un protocole léger serverless d'authentification mutuelle pour les objets connectés hétérogènes. La première contribution fournit trois avantages par rapport aux protocoles existants. Cette contribution répond aux exigences des systèmes pervasifs. La validation de notre proposition a été faite en utilisant l'outil AVISPA et la validation informelle en utilisant sécurité et de vie privée des jeux. Notre deuxième contribution comprend deux protocoles complémentaires dans le domaine des technologies RFID. Le premier protocole vise à l'authentification de masse entre un lecteur RFID et un groupe d'étiquettes tandis que le deuxième protocole effectue une recherche sécurisée pour une étiquette cible parmi un groupe d'étiquettes dans le voisinage du lecteur. Les deux protocoles proposés tiennent compte des contraintes de ressources des étiquettes RFID. Après une étude approfondie des protocoles serverless, nous avons proposé une troisième contribution, un guide pour la conception des protocoles serverless sécurisé et efficaces pour les systèmes pervasifs. Le guide contient six principes et six meilleures pratiques en vue d'élaborer des protocoles serverless. Le guide est destiné à aider à la conception de protocoles serverless efficaces, sécurisés et simples en évitant des erreurs couramment faites dans les protocoles existants / This thesis addresses the security and privacy challenges relevant to the resource constrained devices in the era of pervasive computing. Pervasive computing, a term coined by Schechter to describe the idea of computing services available anytime, anywhere and on demand, is characterized by seamless interactions between heterogeneous players in the Internet. This phenomenon allows intelligent chips, sensors or microcontrollers to be embedded into everyday objects to enable them generate, communicate and share information. Pervasive computing accelerates technological evolution by integrating small and resource constrained devices to the Internet arena, eventually opening doors to new services requiring seamless interactions and integrations with the existing technologies, infrastructures and services. The nature of the information generated, stored and shared by resource constrained devices may require proper security and privacy guarantees. Towards that end, the classical security solutions are not ideal candidates to solve the security and privacy challenges in pervasive systems for two reasons. First, classical security protocols require a lot of resources from the host devices while most of the pervasive devices have very strict resource constraints. Second, most classical security solutions work in a connected mode, which requires constant communication between devices and centralized servers for authentication and authorization purposes. However, pervasive devices may be working in isolated areas with intermittent network coverage and connectivity. Thus, it is ideal to come up with alternative solutions suitable for heterogeneous pervasive devices to smoothly interact, authenticate and securely share information. One of the suitable alternative solutions is the serverless protocols. The term “serverless protocol” refers to the mechanism of enabling centrally controlled devices to autonomously authenticate one another, or other heterogeneous devices, without an active participation of the centralized authentication or authorization servers. Serverless protocols prioritize on securing proximity communication between heterogeneous devices while optimizing on the little resources available. In this thesis, we tackle the challenges of pervasive systems by proposing lightweight and efficient serverless protocols for authenticating heterogeneous pervasive devices during proximity communication. Our proposed protocols derive their originality from the fact that they do not require the communicating parties to have prior relationships with each other, nor to have any previously shared authentication information with each other. Moreover, our proposed solutions incorporate context information to enforce automatic parameter expiry. This property is not supported by most of the earlier versions of the serverless protocol schemes, hence making them vulnerable to different attacks. Three novel contributions are proposed in this thesis. First, we propose a serverless lightweight mutual authentication protocol for heterogeneous devices. The first contribution includes a formal validation using the AVISPA tool. Second, we propose two complementing protocols using RFID (Radio-Frequency Identification) as a core technology. The first protocol performs mass authentication between an RFID reader and a group of tags and the second protocol performs a secure search for a target tag among a group of tags. The second contribution includes two formal validations; one is done using the AVISPA tool and the other is done using the CryptoVerif tool. After a thorough study of serverless protocols, we propose our third contribution, a concise guide on how to develop secure and efficient serverless protocols relevant to the pervasive systems

Security of communications is a major requirement for Mobile Adhoc NETworks(MANETs) since they use wireless channel for communications which can be easily tapped, and physical capture of MANET nodes is also quite easy. From the point of view of providing security in MANETs, there are basically two types of MANETs, viz., authoritarian MANETs, in which there exist one or more authorities who decide the members of the network, and self-organized MANETs, in which there is no such authority. Ensuring security of communications in the MANETs is a challenging task due to the resource constraints and infrastructure-less nature of these networks, and the limited physical security of MANET nodes. Attacks on security in a MANET can be launched by either the external attackers which are not legitimate members of the MANET or the internal attackers which are compromised members of the MANET and which can hold some valid security credentials or both. Key management and authentication protocols(KM-APs)play an important role in preventing the external attackers in a MANET. However, in order to prevent the internal attackers, an intrusion detection system(IDS) is essential. The routing protocols running in the network layer of a MANET are most vulnerable to the internal attackers, especially to the attackers which launch packet dropping attack during data packet forwarding in the MANET. For an authoritarian MANET, an arbitrated KM-AP protocol is perfectly suitable, where trusts among network members are coordinated by a trusted authority. Moreover, due to the resource constraints of a MANET, symmetric key management protocols are more efficient than the public key management protocols in authoritarian MANETs. The existing arbitrated symmetric key management protocols in MANETs, that do not use any authentication server inside the network are susceptible to identity impersonation attack during shared key establishments. On the other hand, the existing server coordinated arbitrated symmetric key management protocols in MANETs do not differentiate the role of a membership granting server(MGS) from the role of an authentication server, and so both are kept inside the network. However, keeping the MGS outside the network is more secure than keeping it inside the network for a MANET. Also, the use of a single authentication server inside the network cannot ensure robustness against authentication server compromise. In self-organized MANETs, public key management is more preferable over symmetric key management, since the distribution of public keys does not require a pre-established secure channel. The main problem for the existing self-organized public key management protocols in MANETs is associated with the use of large size certificate chains. Besides, the proactive certificate chaining based approaches require each member of a MANET to maintain an updated view of the trust graph of the entire network, which is highly resource consuming. Maintaining a hierarchy of trust relationships among members of a MANET is also problematic for the same reason. Evaluating the strength of different alternative trust chains and restricting the length of a trust chain used for public key verification is also important for enhancing the security of self-organized public key management protocols. The existing network layer IDS protocols in MANETs that try to defend against packet dropping attack use either a reputation based or an incentive based approach. The reputation based approaches are more effective against malicious principals than the incentive based approaches. The major problem associated with the existing reputation based IDS protocols is that they do not consider the protocol soundness issue in their design objectives. Besides, most of the existing protocols incorporate no mechanism to fight against colluding principals. Also, an IDS protocol in MANETs should incorporate some secure and efficient mechanism to authenticate the control packets used by it. In order to mitigate the above mentioned problems in MANETs, we have proposed new models and designed novel security protocols in this thesis that can enhance the security of communications in MANETs at lesser or comparable cost. First, in order to perform security analysis of KM-AP protocols, we have extended the well known strand space verification model to overcome some of its limitations. Second, we have proposed a model for the study of membership of principals in MANETs with a view to utilize the concept for analyzing the applicability and the performance of KM-AP protocols in different types of MANETs. Third and fourth, we have proposed two novel KM-AP protocols, SEAP and CLPKM, applicable in two different types of MANET scenarios. The SEAP protocol is an arbitrated symmetric key management protocol designed to work in an authoritarian MANET, whereas the CLPKM protocol is a self-organized public key management protocol designed for self-organized MANETs. Fifth, we have designed a novel reputation based network layer IDS protocol, named EVAACK protocol, for the detection of packet dropping misbehavior in MANETs. All of the three proposed protocols try to overcome the limitations of the existing approaches in their respective categories. We have provided rigorous mathematical proofs for the security properties of the proposed protocols. Performance of the proposed protocols have been compared with those of the other existing similar approaches using simulations in the QualNet simulator. In addition, we have also implemented the proposed SEAP and CLPKM protocols on a real MANET test bed to test their performances in real environments. The analytical, simulation and experimentation results confirm the effectiveness of the proposed schemes.