Avec la généralisation d'Internet, l'usage des protocoles cryptographiques est devenu omniprésent. Étant donné leur complexité et leur l'aspect critique, une vérification formelle des protocoles cryptographiques est nécessaire.Deux principaux modèles existent pour prouver les protocoles. Le modèle symbolique définit les capacités de l'attaquant comme un ensemble fixe de règles, tandis que le modèle calculatoire interdit seulement a l'attaquant derésoudre certain problèmes difficiles. Le modèle symbolique est très abstrait et permet généralement d'automatiser les preuves, tandis que le modèle calculatoire fournit des garanties plus fortes.Le fossé entre les garanties offertes par ces deux modèles est dû au fait que le modèle symbolique décrit les capacités de l'adversaire alors que le modèle calculatoire décrit ses limitations. En 2012 Bana et Comon ont proposé unnouveau modèle symbolique dans lequel les limitations de l'attaquant sont axiomatisées. De plus, si la sémantique calculatoire des axiomes découle des hypothèses cryptographiques, la sécurité dans ce modèle symbolique fournit desgaranties calculatoires.L'automatisation des preuves dans ce nouveau modèle (et l'élaboration d'axiomes suffisamment généraux pour prouver un grand nombre de protocoles) est une question laissée ouverte par l'article de Bana et Comon. Dans cette thèse nous proposons une procédure de décision efficace pour une large classe d'axiomes. De plus nous avons implémenté cette procédure dans un outil (SCARY). Nos résultats expérimentaux montrent que nos axiomes modélisant la sécurité du chiffrement sont suffisamment généraux pour prouver une large classe de protocoles. / With the rise of the Internet the use of cryptographic protocols became ubiquitous. Considering the criticality and complexity of these protocols, there is an important need of formal verification.In order to obtain formal proofs of cryptographic protocols, two main attacker models exist: the symbolic model and the computational model. The symbolic model defines the attacker capabilities as a fixed set of rules. On the other hand, the computational model describes only the attacker's limitations by stating that it may break some hard problems. While the former is quiteabstract and convenient for automating proofs the later offers much stronger guarantees.There is a gap between the guarantees offered by these two models due to the fact the symbolic model defines what the adversary may do while the computational model describes what it may not do. In 2012 Bana and Comon devised a new symbolic model in which the attacker's limitations are axiomatised. In addition provided that the (computational semantics) of the axioms follows from the cryptographic hypotheses, proving security in this symbolic model yields security in the computational model.The possibility of automating proofs in this model (and finding axioms general enough to prove a large class of protocols) was left open in the original paper. In this thesis we provide with an efficient decision procedure for a general class of axioms. In addition we propose a tool (SCARY) implementing this decision procedure. Experimental results of our tool shows that the axioms we designed for modelling security of encryption are general enough to prove a large class of protocols.

Abstract This dissertation investigates authentication techniques in some emerging areas. Specifically, authentication schemes have been proposed that are well-suited for embedded systems, and privacy-respecting pay Web sites. With embedded systems, a person could own several devices which are capable of communication and interaction, but these devices use embedded processors whose computational capabilities are limited as compared to desktop computers. Examples of this scenario include entertainment devices or appliances owned by a consumer, multiple control and sensor systems in an automobile or airplane, and environmental controls in a building. An efficient public key cryptosystem has been devised, which provides a complete solution to an embedded system, including protocols for authentication, authenticated key exchange, encryption, and revocation. The new construction is especially suitable for the devices with constrained computing capabilities and resources. Compared with other available authentication schemes, such as X.509, identity-based encryption, etc, the new construction provides unique features such as simplicity, efficiency, forward secrecy, and an efficient re-keying mechanism. In the application scenario for a pay Web site, users may be sensitive about their privacy, and do not wish their behaviors to be tracked by Web sites. Thus, an anonymous authentication scheme is desirable in this case. That is, a user can prove his/her authenticity without revealing his/her identity. On the other hand, the Web site owner would like to prevent a bunch of users from sharing a single subscription while hiding behind user anonymity. The Web site should be able to detect these possible malicious behaviors, and exclude corrupted users from future service. This dissertation extensively discusses anonymous authentication techniques, such as group signature, direct anonymous attestation, and traceable signature. Three anonymous authentication schemes have been proposed, which include a group signature scheme with signature claiming and variable linkability, a scheme for direct anonymous attestation in trusted computing platforms with sign and verify protocols nearly seven times more efficient than the current solution, and a state-of-the-art traceable signature scheme with support for variable anonymity. These three schemes greatly advance research in the area of anonymous authentication. The authentication techniques presented in this dissertation are based on common mathematical and cryptographical foundations, sharing similar security assumptions. We call them flexible digital authentication schemes.

Le développement des réseaux de communication digitaux tel Internet a rendu omniprésents les protocoles de communication. Les différents appareils électroniques que nous utilisons au quotidien doivent interagir les uns avec les autres afin de réaliser les taches nombreuses et variées qui sont devenues courantes, comme d'utiliser d'un téléphone portable, envoyer ou recevoir des messages électroniques, faire des achats en ligne et ainsi de suite. Pour ces applications, la sécurité est une notion cruciale. Par exemple, dans le cas des achats en ligne, il faut que la transaction ait lieu sans divulguer les informations personnelles de l'acheteur à un tiers. Les protocoles de communications contiennent les règles qui régissent ces interactions. Afin de s'assurer qu'ils garantissent un certain niveau de sécurité, on souhaite pouvoir les analyser. Une analyse manuelle, ou leur faire subir des tests, n'est pas suffisant, les attaques pouvant se révéler subtiles. Certains protocols ont été utilisés pendant des années avant qu'une attaque soit découverte contre eux. Étant donnée leur ubiquité croissante dans de nombreuses applications importantes, comme le commerce électronique, un des défis importants auquel la recherche doit faire face consiste à développer des méthodes et des outils de vérification pour augmenter notre confiance dans les protocoles sécurisés, et dans les applications qui dépendent de ces protocoles. Par exemple, plus de 28 milliards d'euros sont dépensés en France au cours de transactions sur Internet, et cette quantité ne cesse d'augmenter. De plus, de nouveaux types de protocoles apparaissent continuellement afin de relever de nouveaux défis technologiques et de société, e.g. le vote électronique, le passeport numérique pour n'en citer que quelques-uns. / With the development of digital networks, such as Internet, communication protocols are omnipresent. Digital devices have to interact with each other in order to perform the numerous and complex tasks we have come to expect as commonplace, such as using a mobile phone, sending or receiving electronic mail, making purchases online and so on. In such applications, security is important. For instance, in the case of an online purchase, the right amount of money has to be paid without leaking the buyer personal information to outside parties. Communication protocols are the rules that govern these interactions. In order to make sure that they guarantee a certainlevel of security, it is desirable to analyze them. Doing so manually or by testing them is not enough, as attacks can be quite subtle. Some protocols have been used for years before an attack was discovered. Because of their increasing ubiquity in many important applications, e.g. electronic commerce, a very important research challenge consists in developing methods and verification tools to increase our trust on security protocols, and so on the applications that rely on them. For example, more than 28 billion Euros were spent in France using Internet transactions, and the number is growing. Moreover, new types of protocols are continuously appearing in order to face new technological and societal challenges, e.g. electronic voting, electronic passport to name a few.

This thesis deals with issues of secure authentication and key management in the Internet of Things. It describes basic protocols used in IoT, cryptographic primitives, communication technologies in IoT and end elements. It also includes a measuring the performance of cryptographic primitives on Raspberry Pi and selecting the appropriate LPWAN simulation technology. The conclusion of the work is devoted to the simulation of a LoRaWAN network

Cryptography allows us to do magical things ranging from private communication over a public channel to securely evaluating functions among distrusting parties. For the real-world implementation of these tasks, efficiency is usually one of the most desirable objectives. In this work, we advance our understanding of efficient cryptographic constructions on several fronts.<div><br></div><div>Non-malleable codes are a natural generalization of error-correcting codes. It provides a weaker yet meaningful security guarantee when the adversary may tamper with the codeword such that error-correcting is impossible. Intuitively, it guarantees that the tampered codeword either encodes the original message or an unrelated one. This line of research aims to construct non-malleable codes with a high rate against sophisticated tampering families. In this work, we present two results. The first one is an explicit rate1 construction against all tampering functions with a small locality. Second, we present a rate-1/3 construction for three-split-state tampering and two-lookahead tampering.</div><div><br></div><div>In multiparty computation, fair computation asks for the most robust security, namely, guaranteed output delivery. That is, either all parties receive the output of the protocol, or no party does. By relying on oblivious transfer, we know how to construct MPC protocols with optimal fairness. For a long time, however, we do not know if one can base optimal fair protocol on weaker assumptions such as one-way functions. Typically, symmetric-key primitives (e.g., one-way functions) are much faster than public-key primitives (e.g., oblivious transfer). Hence, understanding whether one-way functions enable optimal fair protocols has a significant impact on the efficiency of such protocols. This work shows that it is impossible to construct optimal fair protocols with only black-box uses one-way functions. We also rule out constructions based on public-key encryptions and f-hybrids, where f is any incomplete function.</div><div><br></div><div>Collective coin-tossing considers a coin-tossing protocol among n parties. A Byzantine adversary may adaptively corrupt parties to bias the output of the protocol. The security ε is defined as how much the adversary can change the expected output of the protocol. In this work, we consider the setting where an adversary corrupts at most one party. 10 Given a target security ε, we wish to understand the minimum number of parties n required to achieve ε-security. In this work, we prove a tight bound on the optimal security. In particular, we show that the insecurity of the well-known threshold protocol is at most two times the optimal achievable security. </div>

At the end of 70th of last century the concept began to emerge, now is referred as a cryptographic hash function. Currently, these functions are associated especially with a digital signature. In 2005, the worldwide most used function SHA-1 was broken. This fact led in 2007 NIST announced a public competition to create a new secure hash algorithm. This Thesis deals with issues of cryptographic hash functions from the beginning of their theoretical formulation to current events in this area. Key words: Cryptographic hash functions, SHA-1, MD5, NIST competition

Mobile technologies have the potential to improve patient monitoring, medical decision making and in general the efficiency and quality of health delivery. They also pose new security and privacy challenges. The objectives of this work are to (i) Explore and define security and privacy requirements on the example of a post-surgical care application, and (ii) Develop and test a pilot implementation Post-Surgical Care Studies of surgical out- comes indicate that timely treatment of the most common complications in compliance with established post-surgical regiments greatly improve success rates. The goal of our pilot application is to enable physician to optimally synthesize and apply patient directed best medical practices to prevent post-operative complications in an individualized patient/procedure specific fashion. We propose a framework for a secure protocol to enable doctors to check most common complications for their patient during in-hospital post- surgical care. We also implemented our construction and cryptographic protocols as an iPhone application on the iOS using existing cryptographic services and libraries.

Cette thèse s'inscrit dans le domaine de la vérification de protocoles cryptographiques dans le modèle symbolique. Plus précisément, il s'agit de s'assurer à l'aide de méthodes formelles que de petits programmes distribués satisfont à des propriétés d'indistinguabilité, c'est-à-dire qu'un attaquant n'est pas capable de deviner quelle situation (parmi deux)il observe. Ce formalisme permet d'exprimer des propriétés de sécurité comme le secret fort, l'intraçabilité ou l'anonymat. De plus, les protocoles sont exécutés simultanément par un grand nombre d'agents, à plusieurs reprises si bien que nous nous heurtons très rapidement à des résultats d'indécidabilité. Dès lors, il faut ou bien tenir compte du nombre arbitraire de sessions et rechercher des méthodes de semi-décision ou identifier des classes décidables ;ou bien établir des procédures de décision pour un nombre fini de sessions. Au moment où nous avons commencé les travaux présentés dans cette thèse les outils de vérification de propriétés d'indistinguabilité pour un nombre borné de sessions ne permettaient de traiter que très peu de sessions :dans certains cas il était tout juste possible de modéliser un échange complet. Cette thèse présente des procédures de décision efficaces dans ce cadre. Dans un premier temps, nous établissons des résultats de petite attaque. Pour des protocoles déterministes nous démontrons qu'il existe une attaque si, et seulement s’il existe une attaque bien typée lorsque toute confusion entre les types des variables est évitée. De plus, nous prouvons que, lorqu'il existe une attaque l'attaquant peut la trouver en utilisant au plus trois constantes. Dans un second temps, nous traduisons le problème d'indistinguabilité en termes d'accessibilité dans un système de planification qui est résolu par l'algorithme du graphe de planification associé à un codage SAT. Nous terminons en confirmant l'efficacité de la démarche ,à travers l'implémentation de l'outil SAT-Equivet sa comparaison vis-à-vis des outils analogues. / This thesis presents methods to verify cryptographic protocolsin the symbolic model: formal methods allowto verify that small distributed programssatisfy equivalence properties.Those properties state that an attackercannot decide what scenario is beeing played.Strong secrecy, and privacy type properties, like anonymityand unlinkeability, can be modelled through this formalism.Moreover, protocols are executed simultaneouslyby an unbounded number of agents, for an unbounded numberof sessions,which leads to indecidability results.So, we have either to consider an arbitrary number of sessions,and search for semi-decision proceduresand decidable classes;or to establish decision procedures for a finite numberof sessions.When we started the work presented in this thesis,the existing equivalence checkers in the bounded modelwere highly limited. They could only handlea~very small number of sessions (sometimes no more than three).This thesis presents efficient decision proceduresfor bounded verification of equivalence properties.Our first step is to provide small attack results.First, for deterministic processes, there existsan attack if, and ony if, there is a well-typed attack,assuming that there is no confusion between variable types.Second, when there exists a flaw,the attacker needs at most three constants to find it.Then, our second step is to translatethe indistinguishability problem as a reachability problemin a planning system. We solve this second problemthrough planning graph algorithm and SAT encoding.In a final step, we present the implementation ofthe SAT-Equiv tool, which allows us to evaluate our approach.In particular, a benchmark with comparable tools provesthe efficiency of SAT-Equiv.

京都大学 / 0048 / 新制・論文博士 / 博士(情報学) / 乙第13184号 / 論情博第94号 / 新制||情||116(附属図書館) / (主査)教授 石田 亨, 教授 中村 佳正, 教授 岡部 寿男, 教授 岡本 龍明 / 学位規則第4条第2項該当 / Doctor of Informatics / Kyoto University / DGAM

With the rapid growth of Internet-of-Things (IoT), billions of devices are expected to be interconnected to provide various services appealing to users. Many devices will get an access to valuable information which is likely to increase the number of malicious attacks on these devices in the future. Therefore, security is considered as one of the most critical challenges in the development of IoT. In order to secure resource-constrained devices such as sensors or radio frequency identification (RFID) tags which form the backbone of IoT, lightweight cryptographic algorithms are required. This thesis focuses on the problem of message authentication. To authenticate a message means to verify that the message: (1) comes from the right sender (i.e. its authenticity), and (2) has not been modified (i.e. its integrity). It is challenging to use traditional message authentication methods in resource-constrained devices because typically they can allocate only a few hundred gates for implementing security due to their limited computing, storage and energy resources. To address these needs, a new message authentication algorithm based on a Cryptographic Cyclic Redundancy Check (C-CRC) was developed by KTH in collaboration with Ericsson. In this thesis, we implemented C-CRC and compared it with KECCAK Message Authentication Code (KMAC) standardized by the National Institute of Standards and Technology (NIST) in 2016. First, MATLAB and Verilog versions were developed for both algorithms. The comparison of these two versions allowed us to verify the correctness of algorithms functionality. After that, the Verilog descriptions were simulated in ModelSim and synthesized using Synopsys design compiler. Finally, placement and routing was performed using Cadence SoC Encounter. The evaluation results show that C-CRC outperforms KMAC in terms of area, power, throughput per area, and energy per bit. However, C-CRC is worse than KMAC in terms of latency. We have also investigated several different options of implementing C-CRC, including producing more than one bit of output per clock cycle. We found that such a technique improves throughput of C-CRC with the minimal penalty in area and power consumption