View: session overviewtalk overviewside by side with other conferences
08:45  Cryptosense: Formal Analysis of Security APIs from Research to SpinOff SPEAKER: Graham Steel 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 spinoff 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 startup CEO. 
10:45  Constructive Cryptography and Security Proofs SPEAKER: Ueli Maurer 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 welldefined 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, polynomialtime, communication tapes, etc.  Informationtheoretic and computational security are different instantiations of the same security statement.  It appears better amenable to a treatment by formal methods.

12:00  A tool for automating the computationally complete symbolic attacker SPEAKER: unknown 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. 
12:20  Towards a Coinductive Characterization of Computational Indistinguishability SPEAKER: unknown 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 higherorder functional language for polynomial time computability, in which tools from implicit computational complexity and coinduction both play a central role. 
12:40  Actual Causes of Security Violations SPEAKER: Divya Sharma 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 semihonest 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 blameassignment. The central contribution of this work is formalizing and reasoning about actual causation in decentralized multiagent systems, in particular, to formalize programs (rather than events) as actual causes of security violations and to deal with nondeterministic systems. 
14:30  Adversary Gain vs. Defender Loss in Quantified Information Flow SPEAKER: Piotr Mardziel 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. 
15:00  Generalizing PermissiveUpgrade in Dynamic Information Flow Analysis SPEAKER: unknown 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 nosensitiveupgrade 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 permissiveupgrade check, which allows a variable upgrade due to control dependence, but marks the variable "partiallyleaked". The program is stopped later if it tries to use (caseanalyze) the partiallyleaked variable. Permissiveupgrade handles the deadvariable assignment problem and remains sound. However, Austin and Flanagan develop permissiveupgrade only for a twopoint (lowhigh) security lattice and indicate a generalization to pointwise products of such lattices. In this paper, we develop a nontrivial and nonobvious generalization of permissiveupgrade 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. 
15:30  MicroPolicies: Formally Verified LowLevel Tagging Schemes for Safety and Security (Short Paper) SPEAKER: Catalin Hritcu ABSTRACT. Today's computer systems are distressingly insecure. A host of vulnerabilities arise from the violation of known, but inpractice unenforceable, safety and security policies, including highlevel programming models and critical invariants of lowlevel programs. This project is aimed at showing that a rich and valuable set of _micropolicies_ can be efficiently enforced by a new generic hardwaresoftware 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 micropolicies, and to instantiate this framework on a diverse set of interesting examples. 
16:30  Protocol Indistinguishability and the Computationally Complete Symbolic Attacker SPEAKER: unknown 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. 
16:50  On WellFounded Security Protocols SPEAKER: Sibylle Froeschle ABSTRACT. We introduce the class of wellfounded 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 contextexplicit. 
17:10  Fitting's Embedding of Classical Logic in S4 and Trace Properties in the Computational Model SPEAKER: unknown ABSTRACT. We explain the connection between Fitting's embedding of classical logic in S4 and the nonTarskian computational semantics that Bana and Comon defined to interpret firstorder formulas for their computationally complete symbolic attacker. 
17:30  Towards Timed Models for CyberPhysical Security Protocols SPEAKER: unknown 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 cyberphysical. 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 cyberphysical 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 CyberPhysical Security Protocols with a Memory Bounded Intruder the reachability problem is PSPACEcomplete if the size of terms is bounded. 