FCS-ARSPA on Tuesday, August 15th

Invited Talk (LICS) (09:00‑10:00)
Chair: Radha Jagadeesan
Location: Metropolitan A

09:00‑10:00

Andy Gordon (Microsoft Research) Provable Implementations of Security Protocols [ppt] Proving cryptographic security protocols has been a challenge ever since Needham and Schroeder threw down the gauntlet in their pioneering 1978 paper on authentication protocols: "The need for techniques to verify the correctness of such protocols is great, and we encourage those interested in such problems to consider this area." By now, there is a wide range of informal and formal methods that can catch most design errors. Still, as in other areas of software, the trouble is that while practitioners are typically happy for researchers to write formal models of their natural language specifications and to apply design principles, they are reluctant to do so themselves. In practice, specifications tend to be partial and ambiguous, and the implementation code is the closest we get to a formal description of most protocols. This motivates the subject of my talk: the relatively new enterprise of adapting formal methods for security protocols to work on code instead of abstract models. The goal is to lower the practical cost of security protocol verification by eliminating the need to write a separate formal model. I will describe current tools that partially address the problem, and discuss what remains to be done.

Break (10:00‑10:30)

Session 1: Protocols 1 (10:30‑12:30)
Chair: Jon Millen
Location: Cirrus

10:30‑11:00	Long Nguyen (Oxford University Computing Laboratory) Bill Roscoe (Oxford University Computing Laboratory) Efficient group authentication protocols based on human interaction We re-examine the needs of computer security in pervasive computing from first principles, specifically the problem of bootstrapping secure networks. We consider the case of systems that may have no shared secret information, and where there is no structure such as a PKI available. We propose several protocols which achieve a high degree of security based on a combination of human-mediated communication and an ordinary Dolev-Yao communication medium. In particular they resist combinatorial attacks on the hash values that have to be compared by human users, seemingly optimising the amount of security they can achieve for a given amount of human effort. We compare our protocols with recent pairwise protocols proposed by, for example, Hoepman and Vaudenay.
11:00‑11:30	Jonathan Millen (The MITRE Corporation) Joshua Guttman (The MITRE Corporation) John Ramsdell Justin Sheehy Brian Sniffen Call by Contract for Cryptographic Protocols Call by contract is a way to specify and use interchangeable services in secure protocols, so that protocols and services can be independently designed and verified. A selection algorithm is given to test whether a candidate service is uniformly selectable. To facilitate independent security verifications of the calling protocol and its services, contracts and requests also provide an NDA (Non-Disclosure Agreement). Informally, NDAs are confidentiality constraints on parameters.
11:30‑12:00	Aybek Mukhamedov (University of Birmingham) Mark Ryan (The University of Birmingham) On Asynchronous Multi-party Contract-Signing A multi-party contract signing protocol allows a set of participants to exchange messages with each other with a view to arriving in a state in which each of them has a pre-agreed contract text signed by all the others. ``Optimistic'' protocols allow parties to sign a contract initially without involving a trusted third party $T$. If all signers are honest and messages are not arbitrarily delayed, the protocol can conclude successfully without $T$'s involvement. Signers can ask $T$ to intervene if something goes amiss, for example, if an expected message is not received. We show an attack on Chadha, Kremer and Scedrov's revision of Garay and MacKenzie's protocol (1999), for any number $n > 4$ of signers. We argue that our attack shows that the message exchange structure of GM's main protocol is flawed: whatever the trusted party does will result in unfairness for some signer. This means that it is impossible to define a trusted party protocol for Garay and MacKenzie's main protocol; we call this ``resolve-impossibility''. We propose a new optimistic multi-party contract signing protocol, also based on private contract signatures. (In the full version) we present a proof that our protocol satisfies fairness and abuse freeness.
12:00‑12:30	Romain Janvier (Verimag) Yassine Lakhnech (Verimag) Laurent Mazaré (Verimag) Relating the Symbolic and Computational Models of Security Protocols Using Hashes In this paper, we consider a Dolev-Yao model with hash functions and establish its soundness with respect to the computational model. Soundness means that the absence of attacks in the Dolev-Yao model implies that the probability for an adversary to perform an attack in the computational model is negligible. Classical requirements for deterministic hash functions (e.g. one-wayness, collision freeness) are not sufficient for proving this result. Therefore we introduce new security requirements that are sufficient to prove the soundness result and that are verified by random oracles.

Lunch break (12:30‑14:00)

Session 2: Protocol logics (14:00‑15:30)
Chair: Santiago Escobar
Location: Cirrus

14:00‑14:30	Johannes Borgström (TU Berlin) Simon Kramer (EPFL) Uwe Nestmann (TU Berlin) Calculus of Cryptographic Communication We define C3, a model-based formalism that is one half of a whole framework for the modelling, specification, and verification of cryptographic protocols. C3 consists of a language of distributed processes and an associated (SOS) notion of concurrent execution. The other half of our framework is a property-based formalism, i.e., a logic, for the specification and verification of such protocols, called CPL. The two primary features of the co-design of C3 and CPL are that reduction constraints of C3-processes are checkable via CPL-satisfaction, and that C3 ’s notion of observational equivalence and CPL’s notion of propositional knowledge have a common definitional basis, namely structurally indistinguishable protocol histories. Moreover, this co-design permits separation of the concerns of protocol and property description, within the same framework. Other important features of C3 are explicit out-of-band communication and history-based key lookup, which together give a concrete foundation for authentication and key establishment protocols.
14:30‑15:00	Prateek Gupta (UT) Vitaly Shmatikov (The University of Texas at Austin) Key confirmation and adaptive corruptions in the protocol security logic Cryptographic security for key exchange and secure session establishment protocols is usually defined in the so called ``adaptive corruptions'' model. Even if the adversary corrupts one of the participants in the middle of the protocol execution and obtains the victim's secrets such as the private signing key, the victim must be able to detect this and abort the protocol. This is usually achieved by adding a \emph{key confirmation} message to the protocol. Conventional symbolic methods for protocol analysis assume unforgeability of digital signatures, and thus cannot be used to reason about security in the adaptive corruptions model. We present a symbolic protocol logic for reasoning about authentication and key confirmation in key exchange protocols. We demonstrate that the logic is cryptographically sound: a symbolic proof of authentication and secrecy implies that the protocol is cryptographically secure in the adaptive corruptions model. We illustrate our method by formally proving security of an authenticated Diffie-Hellman protocol with key confirmation.
15:00‑15:30	Philippe Balbiani (IRIT) Yannick Chevalier (Institut de Recherche en Informatique de Toulouse) mounira kourjieh (phd student) Reasoning about Actions and Obligations There are numerous languages that have been devised to express security policies in a distributed environment. Some of these languages permit also to express obligations that have to be fulfilled by someone performing an action. However when only an operational semantics (how permissions to accomplish actions are granted and which obligations have to be satisfied after the execution of an action) is given, it is difficult to reason on security policies expressed in these languages. We present here of logic in which security policies are considered as first class objects, as is the case e.g. in Web Services. This permits to express properties on the actions performed by some individuals as well as on the security policy of these individuals. This model corresponds to the one used for Web Services, where security policies can be sent from one service to another. This integration is performed via adding modal operators expressing obligations and permissions imposed by a service to dynamic modalities expressing actions. The possible actions of services are modelled by necessity and possibility modalities. We give here an axiomatisation of this logic and provide preliminary answers concerning the complexity of its satisfiability problem.

Break (15:30‑16:00)

Session 3: Authentication (16:00‑17:00)
Chair: Andre Scedrov
Location: Cirrus

16:00‑16:30

Matthias Anlauff (Kestrel Institute) Dusko Pavlovic (Kestrel Institute) Richard Waldinger (SRI International) Stephen Westfold (Kestrel Institute) Proving Authentication Properties in the Protocol Derivation Assistant We present a formal framework for incremental reasoning about authentication protocols, supported by the Protocol Derivation Assistant (PDA). A salient feature of our derivational approach is that proofs of properties of complex protocols are factored into simpler proofs of properties of their components, combined with proofs that the relevant refinement and composition operations preserve the proven properties or transform them in the desired way. In the present paper, we introduce an axiomatic theory of authentication suitable for the automatic proof of authentication properties. We describe a proof of the authentication property of a simple protocol, as derived in PDA, for which the the proof obligations have been automatically generated and discharged. Producing the proof forced us to spell out previously unrecognized assumptions, on which the correctness of the protocol depends.

16:30‑17:00

DongGook Park (SunChon National University) Colin Boyd (Queensland University of Technology) Byoungcheon Lee (Joongbu University) Hwankoo Kim (Hoseo University) Responsibility and Credit: New Members of the Authentication Family? There are several goals or properties which authentication protocols may have; some of them are key freshness, far-end aliveness, key confirmation, etc. Most of them have extensively been discussed and studied so far in the literature. "Responsibility" and "credit", which were first raised by Abadi as additional goals [Abad98, Abad00], received quite an exceptional treatment; there were little response from researchers about these new goals. It is surprising to see that these two properties have slipped through any investigation, successfully achieving the positions as the goals for authentication protocols. In this paper, we investigate these two new properties and their relations to authentication protocols, and answer to the question: what brings us credit and responsibility. With clearer understanding of these two notions, we also suggest a new angle from which to investigate the identity and the key.