Les codes localement corrigibles ont été introduits dans le but d'extraire une partie de l'information contenue dans un mot de code bruité, en effectuant un nombre limité de requêtes à ses symboles, ce nombre étant appelé la localité du code. Ces dernières années ont vu la construction de trois familles de tels codes, dont la localité est sous-linéaire en la taille du message, et le rendement est arbitrairement grand. Ce régime de paramètres est particulièrement intéressant pour des considérations pratiques.Dans cette thèse, nous donnons une rapide revue de littérature des codes localement corrigibles, avant d'en proposer un modèle combinatoire générique, à base de block designs. Nous définissons et étudions ensuite un analogue, dans le cas projectif, des relèvements affine de codes introduits par Guo, Kopparty et Sudan. Nous établissons par ailleurs plusieurs liens entre ces deux familles, pour finir par une analyse précise de la structure monomiale de ces codes dans le cas du relèvement plan.Une deuxième partie de la thèse se focalise sur l'application de ces codes à deux protocoles cryptographiques. D'abord, nous proposons un protocole de récupération confidentielle d'information (private information retrieval, PIR) à partir de codes basés sur des designs transversaux, dont la taille des blocs s'apparente à la localité d'un code localement corrigible. Les protocoles ainsi construits ont l'avantage de n'exiger aucun calcul pour les serveurs, et de présenter une faible redondance de stockage ainsi qu'une complexité de communication modérée. Ensuite, nous donnons une construction générique de preuve de récupérabilité (proof of retrievability, PoR) à base de codes admettant une riche structure d'équations de parité à petit poids. Nous en donnons finalement une analyse de sécurité fine ainsi que plusieurs instanciations fondées sur des codes à propriétés locales. / Locally correctable codes (LCCs) were introduced in order to retrieve pieces of information from a noisy codeword, by using a limited number of queries to its symbols, this number being called the locality. Three main families of LCCs reaching sublinear locality and arbitrarily high rate have been built so far. This specific range of parameters is of particular interest concerning practical applications of LCCs.In this thesis, after giving a state of the art for LCCs, we study how they can be built using block designs. We then give an analogue over projective spaces of the family of affine lifted codes introduced by Guo, Kopparty and Sudan. We exhibit several links between both families, and we give a precise analysis of the monomial structure of the code in the case of the lifting of order 2.The second part of the thesis focuses on the application of these codes to two cryptographic protocols. We first build a new private informatin retrieval (PIR) protocol from codes based on transversal designs, whose block size defines the locality of the code. Our construction features no computation on the server side, low storage overhead and moderate communication complexity. Then, we propose a new generic construction of proof-of-retrievability (PoR) that uses codes equipped with an elaborate structure of low-weight parity-check equations. We give a rigorous analysis of the security of our scheme, and we finally propose practical instantiations based on codes with locality.

The Internet of Things has become an integral part of modern society and continues to grow and evolve. The devices are expected to operate in various conditions and environments while securely transmitting sensor data and keeping low manufacturing costs. Security for the Internet of Things is still in its infancy and a serious concern. Although there are several schemes and protocols for securing communication over insecure channels, they are deemed too costly to perform on these constrained devices. As a result, substantial effort has been committed to developing secure protocols and adapting existing ones to be more lightweight. What remains seemingly absent in protocol specifications and key management schemes, however, is how to bootstrap and secure the initial communication. While it is possible to use pre-shared keys, such solutions are problematic with security and administrative overhead in mind. When the sensor networks grow in scale, with an increasing number of devices, this becomes especially problematic as autonomous deployment becomes necessary. By reviewing proposed bootstrapping techniques and evaluating suitable candidates, this work aims to provide an overview of approaches, their trade-offs and feasibility. Results of the study show that advancements in high-speed, lightweight and elliptic curve implementations have made public-key cryptography a viable option even on the very constrained platform, with session keys established within the minute. When analysing the node’s capability to generate randomness, a cornerstone of cryptographic security, initial findings indicate that it is not well equipped for the task. Consequently, sources of entropy must be evaluated thoroughly in resource-constrained devices before use and dedicated hardware for randomness might be necessary for the most constrained nodes if any security is to be guaranteed. / Sakernas internet har blivit en central del i dagens samhälle och fortsätter att utvecklas och integreras allt mer. Enheterna förväntas fungera i många typer av miljöer och förhållanden samtidigt som de ska skicka data säkert och vara billiga att producera. Trots att utvecklingen gått framåt, är säkerheten fortfarande väldigt rudimentär och i behov av ytterligare utveckling. För vanliga nätverk finns det många väletablerade protokoll för att säkra kommunikation, men dessa anses oftast vara för komplicerade för de resursbegränsade enheterna. Till följd av detta har forskning inriktats på att effektivisera existerande protokoll men även på att utveckla enklare varianter. Det som fortfarande kvarstår som ett problem och ofta inte diskuteras, är hur den initiala distributionen av kryptografiska nycklar ska genomföras. Att använda sig utav förinstallerade nycklar är en möjlighet, men det brukar oftast bli problematiskt utifrån säkerhet och administrering när sensornätverken växer i storlek. Genom att granska och utvärdera föreslagna metoder för initial konfiguration av sensornätverk, ämnar detta arbete att ge en översikt i vilka olika metoder som finns tillgängliga och deras lämplighet. Resultat från arbetet visar att tack vare framsteg inom elliptisk kurvkryptografi är publik nyckelkryptografi ett rimligt alternativ att använda, då en sessionsnyckel kan etableras inom loppet av en minut. Vid utvärdering av enheternas förmåga att generera slumptal visar initiala resultat däremot att A/D-omvandlaren inte är en lämplig källa för detta då dess entropi är låg och genererad slumpdata har en dålig fördelning och hög upprepning. Det går därför att dra slutsatsen att om någon nivå av kryptografisk säkerhet ska erhållas, så måste källor till entropi utvärderas noggrant. De resursbegränsade enheterna kan även ha ett behov av dedikerad hårdvara för att generera slumptal.

We study the problem of secure key establishment. We critically examine the security models of Bellare and Rogaway (1993) and Canetti and Krawczyk (2001) in the computational complexity approach, as these models are central in the understanding of the provable security paradigm. We show that the partnership definition used in the three-party key distribution (3PKD) protocol of Bellare and Rogaway (1995) is flawed, which invalidates the proof for the 3PKD protocol. We present an improved protocol with a new proof of security. We identify several variants of the key sharing requirement (i.e., two entities who have completed matching sessions, partners, are required to accept the same session key). We then present a brief discussion about the key sharing requirement. We identify several variants of the Bellare and Rogaway (1993) model. We present a comparative study of the relative strengths of security notions between the several variants of the Bellare-Rogaway model and the Canetti-Krawczyk model. In our comparative study, we reveal a drawback in the Bellare, Pointcheval, and Rogaway (2000) model with the protocol of Abdalla and Pointcheval (2005) as a case study. We prove a revised protocol of Boyd (1996) secure in the Bellare-Rogaway model. We then extend the model in order to allow more realistic adversary capabilities by incorporating the notion of resetting the long-term compromised key of some entity. This allows us to detect a known weakness of the protocol that cannot be captured in the original model. We also present an alternative protocol that is efficient in both messages and rounds. We prove the protocol secure in the extended model. We point out previously unknown flaws in several published protocols and a message authenticator of Bellare, Canetti, and Krawczyk (1998) by refuting claimed proofs of security. We also point out corresponding flaws in their existing proofs. We propose fixes to these protocols and their proofs. In some cases, we present new protocols with full proofs of security. We examine the role of session key construction in key establishment protocols, and demonstrate that a small change to the way that session keys are constructed can have significant benefits. Protocols that were proven secure in a restricted Bellare-Rogaway model can then be proven secure in the full model. We present a brief discussion on ways to construct session keys in key establishment protocols and also prove the protocol of Chen and Kudla (2003) secure in a less restrictive Bellare-Rogaway model. To complement the computational complexity approach, we provide a formal specification and machine analysis of the Bellare-Pointcheval-Rogaway model using an automated model checker, Simple Homomorphism Verification Tool (SHVT). We demonstrate that structural flaws in protocols can be revealed using our framework. We reveal previously unknown flaws in the unpublished preproceedings version of the protocol due to Jakobsson and Pointcheval (2001) and several published protocols with only heuristic security arguments. We conclude this thesis with a listing of some open problems that were encountered in the study.

Είναι ευρέως αποδεκτό ότι η ασφάλεια δεδομένων έχει ήδη ξεκινήσει να διαδραματίζει κεντρικό ρόλο στον σχεδιασμό μελλοντικών συστημάτων τεχνολογίας πληροφορίας (IT – Information Technology). Μέχρι πριν από λίγα χρόνια, ο υπολογιστής αποτελούσε την κινητήρια δύναμη της ψηφιακής επικοινωνίας. Πρόσφατα, ωστόσο, έχει γίνει μια μετατόπιση προς τις εφαρμογές τεχνολογίας πληροφορίας που υλοποιούνται σαν ενσωματωμένα συστήματα. Πολλές από αυτές τις εφαρμογές στηρίζονται σε μεγάλο βαθμό σε μηχανισμούς ασφαλείας, περιλαμβάνοντας την ασφάλειας για ασύρματα τηλέφωνα, φαξ, φορητούς υπολογιστές, συνδρομητική τηλεόραση, καθώς και συστήματα προστασίας από αντιγραφή για audio / video καταναλωτικά προϊόντα και ψηφιακούς κινηματογράφους. Το γεγονός ότι ένα μεγάλο μέρος των ενσωματωμένων εφαρμογών είναι ασύρματο, καθιστά το κανάλι επικοινωνίας ιδιαίτερα ευάλωτο και φέρνει στο προσκήνιο την ανάγκη για ακόμη μεγαλύτερη ασφάλεια. Παράλληλα με τα ενσωματωμένα συστήματα, η εκρηκτική ανάπτυξη των ψηφιακών επικοινωνιών έχει επιφέρει πρόσθετες προκλήσεις για την ασφάλεια. Εκατομμύρια ηλεκτρονικές συναλλαγές πραγματοποιούνται κάθε μέρα, και η ταχεία ανάπτυξη του ηλεκτρονικού εμπορίου κατέστησε την ασφάλεια ένα θέμα ζωτικής σημασίας για πολλές καταναλωτές. Πολύτιμες επιχειρηματικές ευκαιρίες , καθώς επίσης και πολλές υπηρεσίες πραγματοποιούνται κάθε μέρα μέσω του Διαδικτύου και πλήθος ευαίσθητων δεδομένων μεταφέρονται από ανασφαλή κανάλια επικοινωνίας σε όλο τον κόσμο. Η επιτακτική ανάγκη για την αντιμετώπιση αυτών των προβλημάτων, κατέστησε πολύ σημαντική την συμβολή της κρυπτογραφίας, και δημιούργησε μια πολύ υποσχόμενη λύση, με την οποία ενσωματωμένα συστήματα σε συνδυασμό με κρυπτογραφικά πρωτόκολλα, θα μπορούσαν να μας οδηγήσουν στην εξασφάλιση των επιθυμητών αποτελεσμάτων. Στην παρούσα εργασία, παρουσιάζουμε την υλοποίηση ενός ενσωματωμένου συστήματος, εμπλουτισμένο με κρυπτογραφικά πρωτόκολλα, που ουσιαστικά μεταμορφώνει έναν κοινό ηλεκτρονικό υπολογιστή σε ένα ισχυρό Crypto System PC, και έχει σαν κύρια αρμοδιότητα να μπορεί να επικοινωνεί με ένα υπολογιστικό σύστημα και να στέλνει πληροφορίες για την κατάσταση του μέσω ασφαλούς σύνδεσης διαδικτύου σε κάποιον απομακρυσμένο υπολογιστή ελέγχου/καταγραφής συμβάντων σε ώρες που δεν είναι εφικτή η παρουσία εξειδικευμένου προσωπικού για τον έλεγχο του. Αξιολογούμε την απόδοση του και την λειτουργία του με την εκτέλεση διάφορων πειραμάτων, ενώ επίσης προτείνουμε λύσεις για πιο ιδανικές και αποδοτικές συνθήκες λειτουργίας για μελλοντικές εφαρμογές. / It is widely recognized that data security already plays a central role in the design of future IT systems.Until a few years ago, the PC had been the major driver of the digital economy. Recently, however, there has been a shift towards IT applications realized as embedded systems.Many of those applications rely heavily on security mechanisms, including security for wireless phones, faxes, wireless computing, pay-TV, and copy protection schemes for audio/video consumer products and digital cinemas. Note that a large share of those embedded applications will be wireless, which makes the communication channel especially vulnerable and the need for security even more obvious. In addition to embedded devices, the explosive growth of digital communications also brings additional security challenges. Millions of electronic transactions are completed each day, and the rapid growth of eCommerce has made security a vital issue for many consumers. Valuable business opportunities are realized over the Internet and megabytes of sensitive data are transferred and moved over insecure communication channels around the world. The urgent need to face these problems has made the contribution of cryptography very important , and created a very promising solution, in which embedded systems in combination with cryptographic protocols, could lead us to obtain the desired results. In this paper, we present the implementation of an embedded system, enriched with cryptographic protocols, which turns a common computer into a powerful Crypto System PC, and has as its primary responsibility to be able to communicate with a computer system and send information for its situation through secure internet connections to a remote computer which is responsible for recording of events, when there is not qualified staff to control the computer system. We evalauate its performance and operation, by executing various experiments and we also suggest solutions for more optimal and efficient operating conditions for future applications.

Private set intersection(PSI) is a two party protocol where both parties possess a private set and at the end of the protocol, one party (client) learns the intersection while other party (server) learns nothing. Motivated by some interesting practical applications, several provably secure and efficient PSI protocols have appeared in the literature in recent past. Some of the proposed solutions are secure in the honest-but-curious (HbC) model while the others are secure in the (stronger) malicious model. Security in the latter is traditionally achieved by following the classical approach of attaching a zero knowledge proof of knowledge (ZKPoK) (and/or using the so-called cut-and-choose technique). These approaches prevent the parties from deviating from normal protocol execution, albeit with significant computational overhead and increased complexity in the security argument, which includes incase of ZKPoK, knowledge extraction through rewinding. We critically investigate a subset of the existing protocols. Our study reveals some interesting points about the so-called provable security guarantee of some of the proposed solutions. Surprisingly, we point out some gaps in the security argument of several protocols. We also discuss an attack on a protocol when executed multiple times between the same client and server. The attack, in fact, indicates some limitation in the existing security definition of PSI. On the positive side, we show how to correct the security argument for the above mentioned protocols and show that in the HbC model the security can be based on some standard computational assumption like RSA and Gap Diffie-Hellman problem. For a protocol, we give improved version of that protocol and prove security in the HbC model under standard computational assumption. For the malicious model, we construct two PSI protocols using deterministic blind signatures i.e., Boldyreva’s blind signature and Chaum’s blind signature, which do not involve ZKPoK or cut-and-choose technique. Chaum’s blind signature gives a new protocol in the RSA setting and Boldyreva’s blind signature gives protocol in gap Diffie-Hellman setting which is quite similar to an existing protocol but it is efficient and does not involve ZKPoK.

Quantum cryptography is arguably the most successfully applied area of quantum information theory. In this work, We invsetigate the role of quantum indistinguishability in random number generation, quantum temporal correlations, quantum nonlocality and counterfactuality for quantum cryptography. We study quantum protocols for key distribution, and their security in the conventional setting, in the counterfactual paradigm, and finally also in the device-independent scenario as applied to prepare-and-measure schemes. We begin with the interplay of two essential non-classical features like quantum indeterminism and quantum indistinguishability via a process known as bosonic stimulation is discussed. It is observed that the process provides an efficient method for macroscopic extraction of quantum randomness. Next, we propose two counterfactual cryptographic protocols, in which a secret key bit is generated even without the physical transmission of a particle. The first protocol is semicounterfactual in the sense that only one of the key bits is generated using interaction-free measurement. This protocol departs fundamentally from the original counterfactual key distribution protocol in not encoding secret bits in terms of photon polarization. We discuss how the security in the protocol originates from quantum single-particle non-locality. The second protocol is designed for the crypto-task of certificate authorization, where a trusted third party authenticates an entity (e.g., bank) to a client. We analyze the security of both protocols under various general incoherent attack models. The next part of our work includes study of quantum temporal correlations. We consider the use of the Leggett-Garg inequalities for device-independent security appropriate for prepare-and-measure protocols subjected to the higher dimensional attack that would completely undermine standard BB84. In the last part, we introduce the novel concept of nonlocal subspaces constructed using the graph state formalism, and propose their application for quantum information splitting. In particular, we use the stabilizer formalism of graph states to construct degenerate Bell operators, whose eigenspace determines the nonlocal subspace, into which a quantum secret is encoded and shared among an authorized group of agents, or securely transmitted to a designated secret retriever. The security of our scheme arises from the monogamy of quantum correlations. The quantum violation of the Bell-type inequality here is to its algebraic maximum, making this approach inherently suitable for the device-independent scenario.

The area of formal analysis of cryptographic protocols has been an active one since the mid 80’s. The idea is to verify communication protocols that use encryption to guarantee secrecy and that use authentication of data to ensure security. Formal methods are used in protocol analysis to provide formal proofs of security, and to uncover bugs and security flaws that in some cases had remained unknown long after the original protocol publication, such as the case of the well known Needham-Schroeder Public Key (NSPK) protocol. In this thesis we tackle problems regarding the three main pillars of protocol verification: modelling capabilities, verifiable properties, and efficiency. This thesis is devoted to investigate advanced features in the analysis of cryptographic protocols tailored to the Maude-NPA tool. This tool is a model-checker for cryptographic protocol analysis that allows for the incorporation of different equational theories and operates in the unbounded session model without the use of data or control abstraction. An important contribution of this thesis is relative to theoretical aspects of protocol verification in Maude-NPA. First, we define a forwards operational semantics, using rewriting logic as the theoretical framework and the Maude programming language as tool support. This is the first time that a forwards rewriting-based semantics is given for Maude-NPA. Second, we also study the problem that arises in cryptographic protocol analysis when it is necessary to guarantee that certain terms generated during a state exploration are in normal form with respect to the protocol equational theory. We also study techniques to extend Maude-NPA capabilities to support the verification of a wider class of protocols and security properties. First, we present a framework to specify and verify sequential protocol compositions in which one or more child protocols make use of information obtained from running a parent protocol. Second, we present a theoretical framework to specify and verify protocol indistinguishability in Maude-NPA. This kind of properties aim to verify that an attacker cannot distinguish between two versions of a protocol: for example, one using one secret and one using another, as it happens in electronic voting protocols. Finally, this thesis contributes to improve the efficiency of protocol verification in Maude-NPA. We define several techniques which drastically reduce the state space, and can often yield a finite state space, so that whether the desired security property holds or not can in fact be decided automatically, in spite of the general undecidability of such problems. / Santiago Pinazo, S. (2015). Advanced Features in Protocol Verification: Theory, Properties, and Efficiency in Maude-NPA [Tesis doctoral]. Universitat Politècnica de València. https://doi.org/10.4995/Thesis/10251/48527

Tesis por compendio / [ES] La herramienta criptográfica Maude-NPA es un verificador de modelos especializado para protocolos de seguridad criptográficos que tienen en cuenta las propiedades algebraicas de un sistema criptográfico. En la literatura, las propiedades criptográficas adicionales han descubierto debilidades de los protocolos de seguridad y, en otros casos, son parte de los supuestos de seguridad del protocolo para funcionar correctamente. Maude-NPA tiene una base teórica en la rewriting logic, la unificación ecuacional y el narrowing para realizar una búsqueda hacia atrás desde un patrón de estado inseguro para determinar si es alcanzable o no. Maude-NPA se puede utilizar para razonar sobre una amplia gama de propiedades criptográficas, incluida la cancelación del cifrado y descifrado, la exponenciación de Diffie-Hellman, el exclusive-or y algunas aproximaciones del cifrado homomórfico. En esta tesis consideramos nuevas propiedades criptográficas, ya sea como parte de protocolos de seguridad o para descubrir nuevos ataques. También hemos modelado diferentes familias de protocolos de seguridad, incluidos los Distance Bounding Protocols or Multi-party key agreement protocolos. Y hemos desarrollado nuevas técnicas de modelado para reducir el coste del análisis en protocolos con tiempo y espacio. Esta tesis contribuye de varias maneras al área de análisis de protocolos criptográficos y muchas de las contribuciones de esta tesis pueden ser útiles para otras herramientas de análisis criptográfico. / [CA] L'eina criptografica Maude-NPA es un verificador de models especialitzats per a protocols de seguretat criptogràfics que tenen en compte les propietats algebraiques d'un sistema criptogràfic. A la literatura, les propietats criptogràfiques addicionals han descobert debilitats dels protocols de seguretat i, en altres casos, formen part dels supòsits de seguretat del protocol per funcionar correctament. Maude-NPA te' una base teòrica a la rewriting lògic, la unificació' equacional i narrowing per realitzar una cerca cap enrere des d'un patró' d'estat insegur per determinar si es accessible o no. Maude-NPA es pot utilitzar per raonar sobre una amplia gamma de propietats criptogràfiques, inclosa la cancel·lació' del xifratge i desxifrat, l'exponenciacio' de Diffie-Hellman, el exclusive-or i algunes aproximacions del xifratge homomòrfic. En aquesta tesi, considerem noves propietats criptogràfiques, ja sigui com a part de protocols de seguretat o per descobrir nous atacs. Tambe' hem modelat diferents famílies de protocols de seguretat, inclosos els Distance Bounding Protocols o Multi-party key agreement protocols. I hem desenvolupat noves tècniques de modelització' de protocols per reduir el cost de l'analisi en protocols amb temps i espai. Aquesta tesi contribueix de diverses maneres a l’àrea de l’anàlisi de protocols criptogràfics i moltes de les contribucions d’aquesta tesi poden ser útils per a altres eines d’anàlisi criptogràfic. / [EN] The Maude-NPA crypto tool is a specialized model checker for cryptographic security protocols that take into account the algebraic properties of the cryptosystem. In the literature, additional crypto properties have uncovered weaknesses of security protocols and, in other cases, they are part of the protocol security assumptions in order to function properly. Maude-NPA has a theoretical basis on rewriting logic, equational unification, and narrowing to perform a backwards search from an insecure state pattern to determine whether or not it is reachable. Maude-NPA can be used to reason about a wide range of cryptographic properties, including cancellation of encryption and decryption, Diffie-Hellman exponentiation, exclusive-or, and some approximations of homomorphic encryption. In this thesis, we consider new cryptographic properties, either as part of security protocols or to discover new attacks. We have also modeled different families of security protocols, including Distance Bounding Protocols or Multi-party key agreement protocols. And we have developed new protocol modeling techniques to reduce the time and space analysis effort. This thesis contributes in several ways to the area of cryptographic protocol analysis and many of the contributions of this thesis can be useful for other crypto analysis tools. / This thesis would not have been possible without the funding of a set of research projects. The main contributions and derivative works of this thesis have been made in the context of the following projects: - Ministry of Economy and Business of Spain : Project LoBaSS Effective Solutions Based on Logic, Scientific Research under award number TIN2015-69175-C4-1-R, this project was focused on using powerful logic-based technologies to analyze safety-critical systems. - Air Force Office of Scientific Research of United States of America : Project Advanced symbolic methods for the cryptographic protocol analyzer Maude-NPA Scientific Research under award number FA9550-17-1-0286 - State Investigation Agency of Spain : Project FREETech: Formal Reasoning for Enabling and Emerging Technologies Scientific I+D-i Research under award number RTI2018-094403-B-C32 / Aparicio Sánchez, D. (2022). Modeling and Analysis of Advanced Cryptographic Primitives and Security Protocols in Maude-NPA [Tesis doctoral]. Universitat Politècnica de València. https://doi.org/10.4995/Thesis/10251/190915 / Compendio