In this thesis we present two new type systems for verifying the security of cryptographic protocol models expressed in a spi-calculus and, respectively, of protocol implementations expressed in a concurrent lambda calculus. In this thesis we present two new type systems for verifying the security of cryptographic protocol models expressed in a spi-calculus and, respectively, of protocol implementations expressed in a concurrent lambda calculus. The two type systems combine prior work on refinement types with union and intersection types and with the novel ability to reason statically about the disjointness of types. The increased expressivity enables the analysis of important protocol classes that were previously out of scope for the type-based analyses of cryptographic protocols. In particular, our type systems can statically analyze protocols that are based on zero-knowledge proofs, even in scenarios when certain protocol participants are compromised. The analysis is scalable and provides security proofs for an unbounded number of protocol executions. The two type systems come with mechanized proofs of correctness and efficient implementations.
José Bacelar Almeida, Manuel Barbosa, Endre Bangerter, Gilles Barthe · 6 authors
Developers building cryptography into security-sensitive applications face a daunting task. Not only must they understand the security guarantees delivered by the constructions they choose, they must also implement and combine them correctly and efficiently. Cryptographic compilers free developers from having to implement cryptography on their own by turning high-level specifications of security goals into efficient implementations. Yet, trusting such tools is risky as they rely on complex mathematical machinery and claim security properties that are subtle and difficult to verify. In this paper, we present ZKCrypt, an optimizing cryptographic compiler that achieves an unprecedented level of assurance without sacrificing practicality for a comprehensive class of cryptographic protocols, known as Zero-Knowledge Proofs of Knowledge. The pipeline of ZKCrypt tightly integrates purpose-built verified compilers and verifying compilers producing formal proofs in the CertiCrypt framework. By combining the guarantees delivered by each stage in the pipeline, ZKCrypt provides assurance that the implementation it outputs securely realizes the high-level proof goal given as input. We report on the main characteristics of ZKCrypt, highlight new definitions and concepts at its foundations, and illustrate its applicability through a representative example of an anonymous credential system.
Abstract Distributed applications are difficult to program reliably and securely. Dependently typed functional languages promise to prevent broad classes of errors and vulnerabilities, and to enable program verification to proceed side-by-side with development. However, as recursion, effects, and rich libraries are added, using types to reason about programs, specifications, and proofs becomes challenging. We present F*, a full-fledged design and implementation of a new dependently typed language for secure distributed programming. Our language provides arbitrary recursion while maintaining a logically consistent core; it enables modular reasoning about state and other effects using affine types; and it supports proofs of refinement properties using a mixture of cryptographic evidence and logical proof terms. The key mechanism is a new kind system that tracks several sub-languages within F* and controls their interaction. F* subsumes two previous languages, F7 and Fine. We prove type soundness (with proofs mechanized in Coq) and logical consistency for F*. We have implemented a compiler that translates F* to .NET bytecode, based on a prototype for Fine. F* provides access to libraries for concurrency, networking, cryptography, and interoperability with C#, F#, and the other .NET languages. The compiler produces verifiable binaries with 60% code size overhead for proofs and types, as much as a 45x improvement over the Fine compiler, while still enabling efficient bytecode verification. We have programmed and verified nearly 50,000 lines of F* including new schemes for multi-party sessions; a zero-knowledge privacy-preserving payment protocol; a provenance-aware curated database; a suite of web-browser extensions verified for authorization properties; a cloud-hosted multi-tier web application with a verified reference monitor; the core F* typechecker itself; and programs translated to F* from other languages such as F7 and JavaScript.
L'interpretazione astratta è una teoria che formalizza l'approssimazione conservativa della semantica di sistemi informatici hardware e software, focalizzandosi su alcune proprietà, che espresse mediante opportune strutture algebriche (domini astratti) possono essere calcolate in modo corretto (anche se non completo). Una grande varietà di domini astratti può essere elaborata, a aseconda dei contesti di applicazione, e con scelta dei domini astratti è possibile modulare in modi diversi precisione e complessità computazionale. Questa tesi considera l'applicazione di tecniche di Interpretazione Astratta in tre diversi scenari: Program slicing; Watermarking di database relazionali; Watermarking del codice sorgente di programmi. Relativamente al Program slicing, viene proposto un raffinamento delle tecniche tradizionali già presenti in letteratura. Molto spesso, siamo interessati a una specifica proprietà delle variabili in un criterio di slicing, piuttosto che ai suoi effettivi valori. Questo è il caso, ad esempio, quando si analizza la non-interferenza in language-based security, dove le astrazioni entrano in gioco per modellare il potere osservativo degli attaccanti. In questo scenario, lo slicing tiene in considerazione le proprietà astratte delle variabili e le dipendenze astratte. Questo approccio allo slicing, non è solo la generalizzazione della tecnica tradizionale, ma offre nuovi spunti nelle relazioni tra diverse aree di ricerca dell'informatica. Un secondo scenario di applicazione delle tecniche di Interpretazione Astratta è la progettazione di watermarking di database relazionali, la cui rilevanza è legata al fatto che in Internet è molto importante preservare i diritti di proprietà nei database relazionali mantenuti in outsourcing. In tale ambito, viene proposta una tecnica di watermarking senza distorsione, che migliora la verifica dell'integrità dei database relazionali utilizzando un meccanismo di autenticazione pubblica. L'ultimo scenario considerato è quello del Watermarking del codice sorgente di programmi: all'aumentare della quantità di codice sorgente distribuito sul web, la protezione e il rilevamento delle proprietà del software è diventata una questione importante. Nella tesi, viene presentato uno schema di watermarking software a chiave pubblica (watermarking asimmetrico), basato su tecniche di trasformazione che preservano la semantica, e che è simile nello spirito alle zero-knowledge proofs. L'approccio proposto si pone come un'alternativa alla cifratura e l'autenticazione software piuttosto che come uno strumento per la protezione del copyright.
We propose a coin-flip protocol which yields a string of strong, random coins and is fully simulatable against poly-sized quantum adversaries on both sides. It can be implemented with quantum-computational security without any set-up assumptions, since our construction only assumes mixed commitment schemes which we show how to construct in the given setting. We then show that the interactive generation of random coins at the beginning or during outer protocols allows for quantum-secure realizations of classical schemes, again without any set-up assumptions. As example applications we discuss quantum zero-knowledge proofs of knowledge and quantum-secure two-party function evaluation. Both applications assume only fully simulatable coin-flipping and mixed commitments. Since our framework allows to construct fully simulatable coin-flipping from mixed commitments, this in particular shows that mixed commitments are complete for quantum-secure two-party function evaluation. This seems to be the first completeness result for quantum-secure two-party function evaluation from a generic assumption.
Imad Fakhri Taha Alshaikhli, Rusydi Hasan Makarin, Siti Khairunnisa Mohd Bakri, Nur Dalilah More Yusoff · 5 authors
Much of the current innovation in advanced materials is occurring at the nanoscale, specifically in manufactured nanomaterials (MNs). MNs display unique attributes and behaviors, and may be biologically and physically unique, making them valuable across a wide range of applications. However, as the number, diversity and complexity of MNs coming to market continue to grow, assessing their health and environmental risks with traditional animal testing approaches is too time- and cost-intensive to be practical, and is undesirable for ethical reasons. New approaches are needed that meet current requirements for regulatory risk assessment while reducing reliance on animal testing and enabling safer-by-design product development strategies to be implemented. The adverse outcome pathway (AOP) framework presents a sound model for the advancement of MN decision making. Yet, there are currently gaps in technical and policy aspects of AOPs that hinder the adoption and use for MN risk assessment and regulatory decision making. This review outlines the current status and next steps for the development and use of the AOP framework in decision making regarding the safety of MNs. Opportunities and challenges are identified concerning the advancement and adoption of AOPs as part of an integrated approach to testing and assessing (IATA) MNs, as are specific actions proposed to advance the development, use and acceptance of the AOP framework and associated testing strategies for MN risk assessment and decision making. The intention of this review is to reflect the views of a diversity of stakeholders including experts, researchers, policymakers, regulators, risk assessors and industry representatives on the current status, needs and requirements to facilitate the future use of AOPs in MN risk assessment. It incorporates the views and feedback of experts that participated in two workshops hosted as part of an Organization for Economic Cooperation and Development (OECD) Working Party on Manufactured Nanomaterials (WPMN) project titled, "Advancing AOP Development for Nanomaterial Risk Assessment and Categorization", as well as input from several EU-funded nanosafety research consortia.
Endre Bangerter, Stephan Krenn, Ahmad‐Reza Sadeghi, Thomas Schneider · 5 authors
Abstract. Zero-knowledge proofs of knowledge (ZK-PoK) play an important role in many cryptographic applications. Direct anonymous attestation (DAA) and the identity mixer anonymous authentication system are first real world applications using ZK-PoK as building blocks. But although being used for many years now, design and implementation of sound ZK-PoK remains challenging. In fact, there are security flaws in various protocols found in literatur. Especially for non-experts in the field it is often hard to design ZK-PoK, since a unified and easy to use theoretical framework on ZK-PoK is missing. With this paper we overcome important challenges and facilitate the design and implementation of efficient and sound ZK-PoK in practice. First, Camenisch et al. have presented at EUROCRYPT 2009 a first unified and modular theoretical framework for ZK-PoK. This is compelling, but makes use of a rather inefficient 6-move protocol. We extend and improve their framework in terms of efficiency and show how to realize it using efficient 3-move Σ-protocols. Second, we perform an exact security and efficiency analysis for our new protocol and various protocols found in the literature. The analysis yields novel- and perhaps surprising- results and insights. It reveals for instance that using a 2048 bit RSA modulus, as specified in the DAA standard, only guarantees an upper bound on the success probability of a malicious prover between 1/2 4 and 1/2 24. Also, based on that analysis we show how to select the most efficient protocol to realize a given proof goal. Finally, we also provide low-level support to a designer by presenting a compiler realizing our framework and optimization techniques, allowing easy implementation of efficient and sound protocols.
Nowadays it is widely accepted to formulate the security of a protocol carrying out a given task via the "trusted-party paradigm," where the protocol execution is compared with an ideal process where the outputs are computed by a trusted party that sees all the inputs. A protocol is said to securely carry out a given task if running the protocol with a realistic adversary amounts to "emulating" the ideal process with the appropriate trusted party. In the Universal Composability (UC) framework the program run by the trusted party is called an ideal functionality. While this simulation-based security formulation provides strong security guarantees, its usefulness is contingent on the properties and correct specification of the ideal functionality, which, as demonstrated in recent years by the coexistence of complex, multiple functionalities for the same task as well as by their "unstable" nature, does not seem to be an easy task. In this paper we address this problem, by introducing a general methodology for the sound specification of ideal functionalities. First, we introduce the class of canonical ideal functionalities for a cryptographic task, which unifies the syntactic specification of a large class of cryptographic tasks under the same basic template functionality. Furthermore, this representation enables the isolation of the individual properties of a cryptographic task as separate members of the corresponding class. By endowing the class of canonical functionalities with an algebraic structure we are able to combine basic functionalities to a single final canonical functionality for a given task. Effectively, this puts forth a bottom-up approach for the specification of ideal functionalities: first one defines a set of basic constituent functionalities for the task at hand, and then combines them into a single ideal functionality taking advantage of the algebraic structure. In our framework, the constituent functionalities of a task can be derived either directly or, following a translation strategy we introduce, from existing game-based definitions; such definitions have in many cases captured desired individual properties of cryptographic tasks, albeit in less adversarial settings than universal composition. Our translation methodology entails a sequence of steps that derive a corresponding canonical functionality given a game-based definition. In this way, we obtain a well-defined mapping of game-based security properties to their corresponding UC counterparts. Finally, we demonstrate the power of our approach by applying our methodology to a variety of basic cryptographic tasks, including commitments, digital signatures, zero-knowledge proofs, and oblivious transfer. While in some cases our derived canonical functionalities are equivalent to existing formulations, thus attesting to the validity of our approach, in others they differ, enabling us to "debug" previous definitions and pinpoint their shortcomings.
In this paper, we prove classical coin-flipping secure in the presence of quantum adversaries. The proof uses a recent result of Watrous [Wat09] that allows quantum rewinding for protocols of a certain form. We then discuss two applications. First, the combination of coin-flipping with any non-interactive zero-knowledge protocol leads to an easy transformation from non-interactive zero-knowledge to interactive quantum zero-knowledge. Second, we discuss how our protocol can be applied to a recently proposed method for improving the security of quantum protocols [DFL+09], resulting in an implementation without set-up assumptions. Finally, we sketch how to achieve efficient simulation for an extended construction in the common-reference-string model.
The selective decommitment problem can be described as follows: assume an adversary receives a number of commitments and then may request openings of, say, half of them. Do the unopened commitments remain secure? Although this question arose more than twenty years ago, no satisfactory answer could be presented so far. We answer the question in several ways: 1. If simulation-based security is desired (i.e., if we demand that the adversary's output can be simulated by a machine that does not see the unopened commitments), then security is not achievable for non-interactive or perfectly binding commitment schemes via black-box reductions to standard cryptographic assumptions. However, we show how to achieve security in this sense with interaction and a non-black-box reduction to one-way permutations. 2. If only indistinguishability of the unopened commitments from random commitments is desired, then security is not achievable for (interactive or non-interactive) perfectly binding commitment schemes, via black-box reductions to standard cryptographic assumptions. However, any statistically hiding scheme does achieve security in this sense. Our results give an almost complete picture when and how security under selective openings can be achieved. Applications of our results include: • Essentially, an encryption scheme must be non-committing in order to achieve provable security against an adaptive adversary. • When implemented with our secure commitment scheme, the interactive proof for graph 3-coloring due to Goldreich et al. becomes zero-knowledge under parallel composition. On the technical side, we develop a technique to show very general impossibility results for black-box proofs.
Concurrent executions of a zero-knowledge protocol by a single prover (with one or more verifiers) may leak information and may not be zero-knowledge in toto . In this article, we study the problem of maintaining zero-knowledge.We introduce the notion of an (α, β) timing constraint : for any two processors P 1 and P 2 , if P 1 measures α elapsed time on its local clock and P 2 measures β elapsed time on its local clock, and P 2 starts after P 1 does, then P 2 will finish after P 1 does. We show that if the adversary is constrained by an (α, β) assumption then there exist four-round almost concurrent zero-knowledge interactive proofs and perfect concurrent zero-knowledge arguments for every language in NP . We also address the more specific problem of Deniable Authentication , for which we propose several particularly efficient solutions. Deniable Authentication is of independent interest, even in the sequential case; our concurrent solutions yield sequential solutions without recourse to timing , that is, in the standard model.
We look at the question of how powerful a prover must be to give a zero-knowledge proof.We present the first unconditional bounds on the complexity of a statistical ZK prover.The result is that if a language possesses a statistical zero-knowledge then it also possesses a statistical zero-knowledge proof in which the prover runs in probabilistic, polynomial time with an NP oracle.Previously this was only known given the existence of one-way permutations. Extendingthese techniques to protocols of knowledge complexity k(n) >0, we derive bounds on the time complexity of languages of "small" knowledge complexity.Underlying these results is a technique for efficiently generating an "almost" random element of a set S E P.Namely, we construct a probabilistic machine with an NP oracle which, on input 1" and 6 > 0 runs in time polynomial in n and lg 6-1, and outputs a random string from a distribution within distance 6 of the uniform distribution on S n {O, l}~.
While the intuition underlying a zero knowledge proof system [GMR85] is that no “knowledge” is leaked by the prover to the verifier, researchers are just beginning to analyze such proof systems in terms of formal notions of knowledge. In this paper, we show how interactive proof systems motivate a new notion of practical knowledge, and we capture the definition of an interactive proof system in terms of practical knowledge. Using this notion of knowledge, we formally capture and prove the intuition that the prover does not leak any knowledge of any fact (other than the fact being proven) during a zero knowledge proof. We extend this result to show that the prover does not leak any knowledge of how to compute any information (such as the factorization of a number) during a zero knowledge proof. Finally, we define the notion of a weak interactive proof in which the prover is limited to probabilistic, polynomial-time computations, and we prove analogous security results for such proof systems. We show that, in a precise sense, any nontrivial weak interactive proof must be a proof about the prover's knowledge, and show that, under natural conditions, the notions of interactive proofs of knowledge defined in [TW87] and [FFS87] are instances of weak interactive proofs.