Véronique Cortier
On the use of formal models for proving cryptographic security notions

Abstract: Since the 1980s, two approaches have been developed for analyzing security protocols. One of the approaches relies on a computational model that considers issues of complexity and probability. This approach captures a strong notion of security, guaranteed against all probabilistic polynomial-time attacks. The other approach relies on a symbolic model of protocol executions in which cryptographic primitives are treated as black boxes. Since the seminal work of Dolev and Yao, it has been realized that this latter approach enables significantly simpler and often automated proofs. However, the guarantees that it offers have been quite unclear. In this talk, we present several approaches that enable to obtain the best of both worlds: fully automated proofs and strong, clear security guarantees.

Back to WITS'07 Program

Thomas Jensen
Certified access control on mobile interactive devices

Abstract: We present a formal model of the access control mechanism for Java-enabled mobile interactive devices (mobile telephones, in particular). Being somewhat restricted, we propose a more flexible extension to this model based on the notion of user-granted access control permissions with multiplicities. Based on this model, we develop static permission flow analysis with which it is possible to engineer a formal proof that an applet will not consume resources for which it does not have permissions. From such proofs we construct compact certificates, allowing the receiving device to verify the resource consumption behaviour of a down-loaded applet.

Back to WITS'07 Program

Han Gao, Pierpaolo Degano, Chiara Bodei and Hanne Riis Nielson.
Detecting Replay Attacks by Freshness Annotations

Abstract: We present a reduction semantics for the LYSA calculus extended with session information and a static analysis for it. If a protocol passes the analysis then it is free of replay attacks.

Back to WITS'07 Program

Laurent Mazare. Computationally Sound Analysis of Protocols using Bilinear Pairings

Abstract: In this paper, we introduce a symbolic model to analyse protocols that use a bilinear pairing between two cyclic groups. This model consists in an extension of the Abadi-Rogaway logic and we prove that the logic is still computationally sound: symbolic indistinguishability implies computational indistinguishability provided that the Bilinear Decisional Diffie-Hellman assumption is verified and that the encryption scheme is IND-CPA secure. We illustrate our results on classical protocols using bilinear pairing like Joux tripartite Diffie-Hellman protocol or the TAK-2 and TAK-3 protocols.

Back to WITS'07 Program

Gavin Lowe. On information flow and refinement-closure

Abstract: The question of information flow considers whether a high-level user of a multi-level security system can pass information to a low-level user. One family of information flow properties is non-deducibility on compositions: that for all possible high-level
behaviours, the low-level user's view is the same. Unfortunately, this family suffers from the refinement paradox: that a process can be classified as secure, yet a refinement can be classified as insecure. In this paper we consider the property that classifies a process as secure if all of its refinements satisfy non-deducibility on compositions.This property correctly classifies all processes for which we have performed thought experiments. The property appears, at first sight, very difficult to test automatically, because of the quantifications over all high-level behaviours and all refinements. However, we prove that it is equivalent to an operational property, and hence derive a test that can be carried out using a model checker such as FDR. We also compare the property with existing properties. We show that it is stronger than Focardi and Gorrieri's strong bisimulation non-deducibility on compositions, but weaker than Roscoe's lazy independence property. Finally we show that the strength of the equivalence is independent of whether the low-level user's ability to distinguish processes is based upon stable failures or bisimulation.

Back to WITS'07 Program

Christopher Dilloway and Gavin Lowe. On the Specification of Secure Channels

Abstract: Security architectures often make use of secure transport protocols to protect network messages: the transport protocols provide secure channels between hosts. In this paper we present a hierarchy of specifications for secure channels. We give trace specifications capturing a number of different confidentiality and authentication properties that secure channels might satisfy, and compare their strengths. We give examples of transport layer protocols that we believe satisfy the channel specifications.

Back to WITS'07 Program

Catalin Dima and Constantin Enea. Nondeduciblity on strategies in the temporal logic of knowledge

Abstract: We provide a syntactic characterization of Nondeducibility on Strategies in CTL$^*$ with knowledge and past time operators, based on prior work by Halpern and O'Neill. Our characterization is provided by means of a number of axioms that have to be satisfied by formulas specifying sets of strategies.

Back to WITS'07 Program

Erik Poll and Aleksy Schubert. Verifying an implementation of SSH

Abstract: We present a case study in the formal verification of an open source Java implementation of SSH.  We discuss the security flaws we found and fixed by means of formal specification and verification -- using the specification language JML and the program verification tool ESC/Java2 -- and by more basic manual code inspection. Of more general interest is the methodology we propose to formalise security protocols such as SSH using finite state machines. This provides a precise but accessible formal specification, that is not only useful for formal verification, but also for development, testing, and for clarification of official specification in natural
language.

Back to WITS'07 Program

Wan Fokkink, Mohammad Torabi Dashti and Anton Wijs. Partial Order Reduction for Branching Security Protocols

Abstract: We extend the partial order reduction algorithm of Clarke et al.\ \cite{clarke} to handle branching security protocols, such as optimistic fair exchange protocols. Applications of the proposed algorithm in both model checking and constraint solving approaches are discussed. We also report some experimental results using a $\mu$CRL implementation of the algorithm.

Back to WITS'07 Program

Ran Canetti, Ling Cheung, Nancy Lynch and Olivier Pereira. On the Role of Scheduling in Simulation-Based Security

Abstract: In a series of papers, Küsters et al. investigated the relationships between various notions of simulation-based security. Two main factors, the placement of a ``master process'' and the existence of ``forwarder processes'', were found to affect the equivalence between different definitions.  In this extended abstract, we add a new dimension to the analysis of simulation-based security, namely, the scheduling of concurrent processes. We show that, when we move from sequential scheduling (as used in previous studies) to task-based scheduling, the same logical statement gives rise to incomparable notions of security.  Under task-based scheduling, the hierarchy based on placement of ``master process'' becomes obsolete, because no such designation is necessary to obtain meaningful runs of a system.  On the other hand, the existence of ``forwarder processes'' remains an important factor.

Back to WITS'07 Program

Michael Backes, Agostino Cortesi and Matteo Maffei. Causality-based Abstraction of Multiplicity in Security  Protocols

Abstract: This paper presents a novel technique for analyzing security protocols based on an abstraction of the program semantics. This technique is based on a novel structure called  causal net which captures the causality  among program events within a finite graph. A core property of causal nets is that they abstract away from the multiplicity of protocol sessions,  hence constituting a concise tool for reasoning about an even infinite number of concurrent protocol sessions; deciding security only requires a traversal of the causal net, thus yielding a decidable, and typically very efficient, approach for security protocol analysis. Additionally, causal nets allow for dealing with different security properties such as secrecy and authenticity in a uniform manner. Both the construction of the causal net from a given protocol description and the subsequent analysis are fully automated.

Back to WITS'07 Program

Joshua Guttman, Shaddin Doghmi and F. Javier Thayer. Skeletons and the Shapes of Bundles

Abstract: Skeletons model partial information about regular (honest) behavior in an execution of a cryptographic protocol. A homomorphism between skeletons is an information-preserving map.  Much protocol analysis may be regarded as an exploration of the properties of the category of skeletons and homomorphisms.  In particular, the strand space authentication tests are special homomorphisms.  These ideas suggest an approach to mechanizing protocol analysis.

Back to WITS'07 Program

Arnab Roy, Anupam Datta, Ante Derek and John Mitchell. Inductive Trace Properties Imply Computational Security

Abstract: Protocol authentication properties are generally trace-based, meaning that authentication holds for the protocol if authentication holds for individual traces (runs of the protocol and adversary). Computational secrecy conditions, on the other hand, often are not trace based: the ability to computationally distinguish a system that transmits a secret from one that does not is measured by overall success on the \textit{set} of all traces of each system. This presents a challenge for inductive or compositional methods: induction is a natural way of reasoning about traces of a system, but it does not appear applicable to non-trace properties. We therefore investigate the semantic connection between trace properties that could be established by induction and non-trace-based security requirements. Specifically, we prove that a certain trace property implies computational secrecy and authentication properties, assuming the encryption scheme provides chosen ciphertext security and ciphertext integrity. We also prove a similar theorem for computational secrecy assuming Decisional Diffie-Hellman and a chosen plaintext secure encryption scheme.

Back to WITS'07 Program

Michael Backes, Agostino Cortesi, Riccardo Focardi and Matteo Maffei. A Calculus of Challanges and Responses

Abstract: This paper presents a novel approach for concisely abstracting authentication protocols and for subsequently analyzing those abstractions in a sound manner, i.e., deriving authentication guarantees for protocol abstractions suffices for proving these guarantees for the actual protocols. The abstractions are formalized in a novel calculus which constitutes a higher-level abstraction of the r-spi calculus and is specifically tailored towards reasoning about challenge-response mechanisms within authentication protocols. Furthermore, it allows for expressing protocols without having to include details on the specific structure of exchanged messages. This in particular entails that many authentication protocols share a common abstraction so that a single validation of this abstraction already gives rise to security guarantees for all these protocols. Such an abstract validation can be automatically performed using static analysis techniques based on an effect system proposed in this paper. Finally, extensions to abstractions of additional protocol classes immediately enjoy a soundness theorem provided that these extensions satisfy certain explicit, easily checkable conditions.

Back to WITS'07 Program