Technical Program: Five minute talks
The strand space model is one of the most successful and widely used formalisms for analysing security protocols. This might seem surprising given that the model is not able to reflect choice points in a protocol execution: the key concept in the strand space model is that of a bundle, which models exactly one possible execution of a security protocol. Inspired by the branching processes of Petri nets, we show that branching can be introduced into the strand space model in a very natural way: bundles can be generalized to branching bundles, which are able to capture several conflicting protocol executions. Our investigations of the theory of branching bundles will motivate the concept of symbolic branching bundles, and culminate in the result that every protocol has a strand space semantics in terms of a largest symbolic branching bundle. We hope our results provide a strong theoretical basis for comparing models and providing process calculi semantics in security protocol analysis. Altogether our work is related but different to a series of works by Crazzolara and Winskel. Throughout we will profit from a close relationship of the strand space model to event structures, which has already been pointed out by these authors.
The design and verification of cryptographic protocols is a notoriously difficult task, even in abstract Dolev-Yao models. This is mainly due to several sources of unboundedness (size of messages, number of sessions, . . . ). In this paper, we characterize a class of protocols for which secrecy for an unbounded number of sessions is decidable. More precisely, we present a simple transformation which maps a protocol that is secure for a single session to a protocol that is secure for an unbounded number of sessions. Our result provides an effective strategy to design secure protocols: (i) design a protocol intended to be secure for one session (this can be verified with existing automated tools); (ii) apply our transformation and obtain a protocol which is secure for an unbounded number of sessions. The proof of our main result is closely tied to a particular constraint solving procedure by Comon-Lundh et al.
Civitas is an electronic voting system that guarantees verifiability and coercion resistance for remote voting. Civitas is based on a protocol due to Juels, Catalano, and Jakobsson (2005), which we extended to improve confidentiality, integrity, availability, and scalability. We implemented Civitas in Jif and evaluated the resulting security and performance. Civitas offers the strongest coercion resistance of any electronic remote voting system, and it is the first voting system to offer assurance through both cryptographic security proofs and information-flow analysis. Appeared in IEEE Symposium on Security and Privacy, 2008.
A state machine, viewed as a graph, can be distributed by removing any cut of the graph, so that the disconnected components run in parallel. Can we derive secure distributed implementations of state machines by this strategy? Intuitively, yes, by sharing keys among the vertices of the cut, encoding the values at the sources of the cut, and decoding them back at the destinations of the cut. However, we claim that in order to preserve safety and security properties by this strategy, one further needs logical clocks. Applications include an implementation of access control with capabilities; see our paper in FCS-ARSPA-WITS'08.
Instead of proving the (general, joint state) UC for one session of a protocol P, it might be much easier to prove that any number of parallel sessions of P are secure (in any environment). At the symbolic level, there are tools, such as ProVerif, which precisely prove such properties. In addition, P might be secure in the latter sense (which is satisfactory) while not being UC-secure.
We show how strategic rewriting and narrowing provide a foundational framework for the compositional design, maintenance and verification of security policies. Rewrite rules transform input terms representing policy requests into decision terms. Strategies are used to explicitly control the rule application. Parameterized queries are solved by narrowing. Relying on the correspondences between the properties of the rewrite system and the policy it implements, we are able to reuse existing proof techniques and analysis tools in the security policies context.
e present a computationally sound mechanized analysis of Kerberos~5, both with and without its public-key extension PKINIT. We prove authentication and key secrecy properties using the prover CryptoVerif, which works directly in the computational model; these are the first mechanical proofs of a full industrial protocol at the computational level. We also generalize the notion of key usability and use CryptoVerif to prove that this definition is satisfied by keys in Kerberos. (This work is published at AsiaCCS'08.)
We present Safer, a static analysis tool for detecting potential denial of service (DoS) vulnerabilities in software systems. Our approach focuses on software design flaws that can be exploited by a remote attacker to exhaust system resources such as CPU or the call stack. Our tool combines taint analysis with control dependency analysis to find program branches whose execution may be influenced by an attacker. This information is then utilized by resource-specific analyses to detect vulnerabilities. Using analysis of loops and recursive calls, our tool discovered several previously unknown vulnerabilities, including a new attack on the previously patched version of a popular FTP server software.
This research had the objective of giving an empirical evaluation of the security protocol specification language MSR (version 2.0). A student with no previous exposure to protocol specification was asked to represent the entire Clark-Jacob library using an existing prototype implementation of MSR 2.0. In the process of doing this, he was asked to keep notes of difficulties, shortcomings and bugs. The findings were that the MSR language is pretty good (succinct representation of protocols, easy to represent simple and complicated protocols), but the MSR implementation needs improvement. Type reconstruction failures, unclear error messages and a few bugs made the task of specifying some protocols more involved than necessary. The secondary goal was to find how easy MSR 2.0 is to use by non-experts. The student learned the basics and could specify protocols by examples in a matter of hours; it took longer to acquire the necessary confidence to represent protocols that deviated from previously seen patterns.
Relating the requirements and assumptions of security protocols to the properties of cryptographic security APIs is a challenge for formal security analysis. As Anderson notes,``Many protocols fail because their goals are not made sufficiently explicit; yet cryptoprocessors are sold as general-purpose machines, and may be used to enforce a very wide range of security policies. We don't yet really know how to formalise security policies, let alone track them back to crypto primitives.'' In this talk, I will highlight a number of examples of this problem, drawing on the emerging field of vehicle-to-vehicle ad-hoc networks (VANETs). I will highlight a pair of new attacks on protocols from the VANET literature whose practicability depends on detailed properties of the API of the tamper resistant device. I will make the case for a formal model for relating API requirements to protocol assumptions, and give some requirements for such a model. Development of such a model is the subject of ongoing research.
Mobile devices running Java MIDP use interactive access control to protect resources. I will present a mechanism for verifying statically that an application uses these access control mechanisms in a way that ensures that the application will not attempt to use more resources than authorized. This mechanism can be verified mchanically and executed on-device when down-loading new applications.
Single-Sign-On (SSO) protocols enable companies to establish a federated environment in which clients sign in the system once and yet are able to access to services offered by different companies. The Security Assertion Markup Language (SAML) Web Browser SSO Profile is the emerging standard in this context. In this paper, we provide formal models of the protocol corresponding to one of the most used use case scenario (the SP-Initiated SSO with Redirect/POST Bindings) and of the implementation used by SAML-based SSO for Google Applications. We have mechanically analysed these formal models with SATMC, a state-of-the-art model checker for security protocols. SATMC has revealed a severe security flaw in the Google's implementation that allows a dishonest service provider to impersonate a user and get unauthorized access to Google Applications (and viceversa). We have reproduced this attack in an actual deployment of the SAML-based SSO for Google Applications. To the best of our knowledge this security flaw of the SAML-based SSO for Google Applications was previously unknown.