ABSTRACT. In this talk I'll describe how our research project into adapting formal analysis technqiues for cryptographic protocols to security APIs turned into an industry collaboration and finally a spin-off company, Cryptosense, that was created in September 2013. Though the company is still in its early stages, we've already learned a lot about the journey from academic results to commercial product. I'll talk about what we're doing now, what we're developing for the future, and what its like to transition from full time researcher to start-up CEO.

ABSTRACT. Cryptographic protocols rely on message-passing to coordinate activity among principals. Each principal maintains local state in individual local sessions only as needed to complete that session. However, in some protocols a principal also uses state to coordinate its different local sessions. Sometimes the non-local, mutable state is used as a means, for example with smart cards or Trusted Platform Modules. Sometimes it is the purpose of running the protocol, for example in commercial transactions.

Many richly developed tools and techniques, based on well-understood foundations, are available for design and analysis of pure message-passing protocols. But the presence of cross-session state poses difficulties for these techniques.

In this paper we provide a framework for modeling stateful protocols. We define a hybrid analysis method. It leverages theorem-proving -- in this instance, the PVS prover -- for reasoning about computations over state. It combines that with an "enrich-by-need" approach -- embodied by CPSA -- that focuses on the message-passing part. As a case study we give a full analysis of the Envelope Protocol, due to Mark Ryan.

ABSTRACT. Constructive cryptography, an alternative paradigm for designing cryptographic protocols and proving their security, is reviewed in this talk and contrasted with other approaches.  In constructive cryptography, a cryptographic scheme (e.g. encryption) is seen as constructing a certain resource (e.g. a secure channel) from another resource (e.g. an authenticated channel and a secret key), for a well-defined notion of construction.  The construction notion is composable, which allows to design complex protocols in a modular, layered manner. The security proofs of the modules (e.g. encryption, authentication, key agreement, or signatures) directly compose to a security proof for the entire protocol. A treatment in constructive cryptography comes with several advantages, among them:

 - Simplicity and reusability due to the modular design.

 - The semantics of security definitions are clear in the sense that one knows how a scheme satisfying a given definition can be used. This allows to compare security definitions.

 - The treatment is at an abstract level, freed from artefacts like Turing machines, asymptotics, polynomial-time, communication tapes, etc. 

 - Information-theoretic and computational security are different instantiations of the same security statement.

 - It appears better amenable to a treatment by formal methods.

ABSTRACT. In this paper we describe a tool automating the computationally complete symbolic attacker model provided by Bana and Comon at POST'12. This model offers soundness guarantees without the usual computational soundness restrictions such as tagging, key cycles... This models allows to find attacks relying on implementation mistakes. Using our tool, we discovered a such new attack on Andrew's secure RPC, we hope to find more attacks in the next few months.

ABSTRACT. Computational indistinguishability (CI in the following) is one of the most central concepts in modern cryptography, and many other definitions (e.g. pseudorandomness, security of cryptoschemes) can be rephrased in terms of CI. We present the results of a study directed towards giving a direct and precise characterization of computational indistinguishability in an higher-order functional language for polynomial time computability, in which tools from implicit computational complexity and coinduction both play a central role.

ABSTRACT. Accurate blame assignment for security violations is essential in a wide range of settings. For example, protocols for authentication and key exchange, electronic voting, auctions, and secure multiparty computation (in the semi-honest model) ensure desirable security properties if protocol parties follow their prescribed programs. However, if they deviate from their prescribed programs and a security property is violated, determining which agents should be blamed and appropriately punished is important to deter agents from committing future violations. This work proposes actual causation (i.e., identifying which agents' deviations caused a specific violation) as a useful building block for blame-assignment. The central contribution of this work is formalizing and reasoning about actual causation in decentralized multi-agent systems, in particular, to formalize programs (rather than events) as actual causes of security violations and to deal with non-deterministic systems.

ABSTRACT. Metrics for quantifying information leakage assume that an adversary’s gain is the defender’s loss. We demonstrate that this assumption does not always hold via a class of scenarios. We describe how to extend quantification to account for a defender with goals distinct from adversary failure. We implement the extension and experimentally explore the impact on the measured information leakage of the motivating scenario.

ABSTRACT. Preventing implicit information flows by dynamic program analysis requires coarse approximations that result in false positives, because a dynamic monitor sees only the executed trace of the program. One widely deployed method is the no-sensitive-upgrade check, which terminates a program whenever a variable's taint is upgraded (made more sensitive) due to a control dependence. Although sound, this method is impermissive, e.g., it terminates the program even if the upgraded variable is never used subsequently. To counter this, Austin and Flanagan introduced the permissive-upgrade check, which allows a variable upgrade due to control dependence, but marks the variable "partially-leaked". The program is stopped later if it tries to use (case-analyze) the partially-leaked variable. Permissive-upgrade handles the dead-variable assignment problem and remains sound. However, Austin and Flanagan develop permissive-upgrade only for a two-point (low-high) security lattice and indicate a generalization to pointwise products of such lattices. In this paper, we develop a non-trivial and non-obvious generalization of permissive-upgrade to arbitrary lattices. The key difficulty lies in finding a suitable notion of partial leaks that is both sound and permissive and in developing a suitable definition of memory equivalence that allows an inductive proof of soundness.

ABSTRACT. Today's computer systems are distressingly insecure. A host of vulnerabilities arise from the violation of known, but in-practice unenforceable, safety and security policies, including high-level programming models and critical invariants of low-level programs. This project is aimed at showing that a rich and valuable set of _micro-policies_ can be efficiently enforced by a new generic hardware-software mechanism and result in more secure and robust computer systems. In particular we aim to come up with a clean formal framework in Coq for expressing, composing, and verifying arbitrary micro-policies, and to instantiate this framework on a diverse set of interesting examples.

ABSTRACT. We considered the problem the computational indistinguishability of two bounded protocols. We designed a symbolic model that is amenable to automated deduction, and such that an inconsistency proof implies computational indistinguishability. Conversely, symbolic models of distinguishability provide clues for likely computational attacks. The idea is to define a computationally complete symbolic attacker in order to achieve unconditional computational soundness of the symbolic analysis. Following our previous work on reachability properties, we achieve this by axiomatizing what an attacker cannot violate. By adding computationally sound, modular axioms, a library of axioms can be built. Despite additional difficulties stemming from equivalences, the models and proofs are much simpler than in the case of reachability properties.

ABSTRACT. We introduce the class of well-founded protocols, and explain why leakiness is decidable for it. We hope that this will help to unify our understanding of a group of results that obtain decidability by imposing conditions that make encrypted messages context-explicit.

ABSTRACT. We explain the connection between Fitting's embedding of classical logic in S4 and the non-Tarskian computational semantics that Bana and Comon defined to interpret first-order formulas for their computationally complete symbolic attacker.

ABSTRACT. Many security protocols rely on the assumptions on the physical properties in which its protocol sessions will be carried out. For instance, Distance Bounding Protocols take into account the round trip time of messages and the transmission velocity to infer an upper bound of the distance between two agents. We classify such security protocols as cyber-physical. The key elements of such protocols are the use of cryptographic keys, nonces and time. This paper investigates timed models for the verification of such protocols. Firstly, we introduce a multiset rewriting framework with continuous time and fresh values. We demonstrate that in this framework one can specify distance bounding protocols and intruder models for cyber-physical security protocols that take into account the physical properties of the environment. Then we prove that models with discrete time are not able to expose as many security flaws as models with continuous time. This is done by proposing a protocol and demonstrating that there is no attack to this protocol when using the model with discrete time, but there is an attack when using the model with continuous time. For the important class of Bounded Memory Cyber-Physical Security Protocols with a Memory Bounded Intruder the reachability problem is PSPACE-complete if the size of terms is bounded.