Lorentz Center - Logic and information security from 22 Sep 2008 through 26 Sep 2008
  Current Workshop  |   Overview   Back  |   Home   |   Search   |     

    Logic and information security
    from 22 Sep 2008 through 26 Sep 2008

Speakers and abstracts


Speakers and abstracts

  • Speaker: Michael Albert, University of Otago
    : Design Theory and Card Deals
    Abstract: Some communications protocols between two agents (Alice and Bob) in the presence of an eavesdropper (Eve) allow the agents to learn in two rounds of communication their precise "assets" without revealing to the eavesdropper any particular asset held by either agent. This is accomplished by means of announcements that specify supersets of the assets held by one or the other of the agents; and deductions available to the agents based on their own holdings. Epistemic axioms describing such protocols can be translated into equivalent combinatorial axioms. These, in turn, are reminiscent of the defining properties of various types of set systems and combinatorial designs. We illustrate this connection with a number of simple examples, including a (very basic!) introduction to the essentials of design theory. For instance, the lines of the Fano plane (http://en.wikipedia.org/wiki/Fano_plane) form a particularly good announcement for Alice, holding three elements of a group of seven, to Bob who holds three other elements. This announcement contains the maximum possible number of elements that still permit Bob to infer Alice's holding, and in return to communicate his own, while even if Eve has full knowledge of both the remaining element and Alice's announcement, she cannot with certainty infer any single element held by Alice or Bob.
    Document: http://www.cs.otago.ac.nz/staffpriv/hans/theoryAJC.pdf , slides


  • Speaker: Alessandro Armando, University of Genova
    : LTL Model Checking for Security Protocol Analysis
    Abstract: In the last decade a new generation of model checking techniques specifically tailored for security protocols has emerged. As a result of this endeavour, a wide range of security protocols can now be analysed automatically by state-of-the-art tools. Most tools assume that communication between honest principals takes place over a Dolev-Yao channel, i.e. a communication channel controlled by a malicious agent capable to overhear, divert, and fake messages. This is too weak an assumption for many modern protocols. For instance, contract signing protocols usually assume for their functioning that communication with a trusted third party takes place over a resilient channel, whereas browser-based protocols often assume some messages are exchanged over SSL/TLS channels, i.e. channels providing some form of confidentiality and/or authenticity. I will show how LTL can be used to specify communication channels used by modern security protocols and present a SAT-based model technique that supports the automatic analysis of security protocols using these channels. I will also report on two previously unknown attacks on a patched version of the ASW fair exchange protocol and on a running implementation of a SAML Web Browser Single Sign-On Protocol that have been detected by using this technique.
    Document: http://www.ai-lab.it/armando/pub/csf20.pdf , slides


  • Speaker: Philippe Balbiani, University Paul Sabatier
    Title: Having the permission to know
    Abstract: In order to palliate the consequences of the inadequacies of the formal models based on modal logic for expressing a security policy able to talk about the right to know, we reconsider the question of the logical foundations of the right to know. We build the syntax of a language in which the writing of formulas saying that "it is obligatory that ..." and "it is known by agent i that ..." is possible. We describe some of the properties of the logical theories that correspond to this language.
    Document: (local copy, in French)


  • Speaker: Johan van Benthem, Universities of Amsterdam and Stanford
    Title: Information flow and procedural information (based on joint work with J. Gerbrandy, T. Hoshi & E. Pacuit)
    Abstract: Information flow involves factual information about the world as well as epistemic information about other agents. But the procedure which generates that information itself provides 'procedural information' about the 'how' rather than the 'that'. The latter notion is sui generis, and it deserves logical study. We will do this in the form of protocols for conversation, observation, or experiment. We discuss how this enrichment affects current dynamic epistemic logics, by providing new representation and completeness theorems linking them to branching temporal logics. We will also indicate how this extends to agents' beliefs, arguably just as important to security as knowledge. Moreover, we will discuss the explicit definition of protocols, and mechanisms for 'protocol update' as we learn more about, or really modify, some existing informational procedure.
    Document: (local copy)


  • Speaker: Cas Cremers, ETH Zurich
    Title 1: Moving from unbounded verification towards formal protocol proofs
    Abstract: We present a verification algorithm and corresponding tool for the verification of security protocols. The algorithm is guaranteed to terminate, after which the result is either falsification (an attack), bounded correctness, or unbounded correctness. The last outcome implies that no attack exists on the protocol within the model. We discuss how this result relates to having a formal (machine checkable) proof of correctness for the protocol. We show initial attempts at moving from this result towards generating a formal proof of correctness. We discuss the remaining hurdles, and the ultimate problems and merits of having such a proof.
    Document: not available

Title 2: On the Protocol Composition Logic PCL
Abstract: A recent development in formal security protocol analysis is the Protocol Composition Logic (PCL). We identify a number of problems with the core of this logic as well as with extensions of the logic. The identified problems imply strong restrictions on the scope of PCL, and imply that some claimed PCL proofs cannot be proven within the logic, or make use of unsound axioms. Additionally, some constructs used in proofs require semantics that cannot be captured in the underlying cord space model.  This includes the proofs of the CR protocol, the SSL/TLS and IEEE 802.11i protocols, and the IEEE 802.11s protocol.  Where possible, we propose solutions for these problems.


  • Speaker: Francien Dechesne, University of Eindhoven
    Title: Operational and Epistemic Approaches to Protocol Analysis: Bridging the Gap (joined work with MohammadReza Mousavi and Simona Orzan)
    Abstract: Operational models of (security) protocols, on one hand, are readable and conveniently match their implementation (at a certain abstraction level). Epistemic models, on the other hand, are appropriate for specifying knowledge-related properties such as anonymity or secrecy. These two approaches to specification and verification have so far developed in parallel and one has either to define ad hoc correctness criteria for the operational model or use complicated epistemic models to specify the operational behavior. We work towards bridging this gap by proposing a combined framework which allows for modeling the behavior of a protocol in a process language with an operational semantics and supports reasoning about properties expressed in a rich logic which combines temporal and epistemic operators.
    Document: http://www.win.tue.nl/~mousavi/pai.htm


  • Speaker: Hans van Ditmarsch, University of Otago
    : Unconditionally secure protocols employing card deals
    Abstract: We analyze and design security protocols for computationally unlimited agents using card deals. Consider three players, of which two (Alice and Bob) want to exchange a secret while the remaining player (Eve) can be considered eavesdropper. Alice, Bob, Eve hold a, b, and c cards, respectively: these parameters (a,b,c) characterize the card deal. Initially, players only know their own hand of cards.
    Typically, Alice and Bob wish to learn each others' actual hand of cards (in terms of interpreted systems: their local states), whereas this should be impossible for Eve. In the well-known Russian Cards problem (the case (3,3,1)) it is additionally required that Eve may not learn any of Alice's or Bob's cards.
    We will give a partial characterization for which (a,b,c) Alice and Bob can exchange their hands of cards, with the additional constraint that single card ownership may not be inferred either. (So far this concurs with Michael Albert's presentation.) Some such solutions allow Eve to guess a card with better than equal odds, even though she does not know that card to be held by Alice (or by Bob). We can counter these odds by a combinatorial constraint for announcements, or by adjusting the protocol producing the announcements. An open question was whether there are protocols of length essentially larger than two, i.e., after Alice's opening announcement and Bob's response, at least one further announcement by Alice is required to successfully conclude the communication of secrets. The answer to that is: yes, there are. I will show an example, and some general results for secure local state exchange in interpreted systems.
    Document: (Bias in cards cryptography, under submission - local copy) , slides


  • Speaker: Jan van Eijck & Yanjing Wang, University of Amsterdam
    Title: Dynamic Epistemic Modelling and Abstraction
    Abstract: Applications of dynamic epistemic modeling (e.g. on security protocols) may require huge Kripke/action models, which could cause the state space to explode, and thus create a problem for model checking.
    In this talk, we propose a property-preserving refinement/abstraction theory based on insights from dynamic epistemic modelling, in order to obtain compact but informative abstractions. To reason about the abstractions, we develop a 3-valued version of dynamic epistemic logic. We show that the abstraction relation allows safe checking of dynamic properties on the abstraction of a model instead of the original model. The core techniques of this approach are proposition/label mapping and rewriting, which we believe can be applied to model checking problems in general.
    We will demonstrate dynamic epistemic modelling without and with abstraction in an extension of the dynamic epistemic model checker DEMO.
    Document: http:://homepages.cwi.nl/~yanjing/ICTAC.pdf , http:://homepages.cwi.nl/~jve/papers/07/adoem/ADOEM.pdf


  • Speaker: Aaron Hunter, Simon Fraser University
    Title: Message Passing, Belief Change and Information Security
    Abstract: Logics of knowledge and belief have been employed for cryptographic protocol verification, because many protocols have goals that are explicitly related to the beliefs of the participants. However, in many cases, the logics employed have been static logics with little emphasis on the representation of belief change. A more accurate model of the evolving beliefs of a protocol participant can be obtained by introducing formal belief change operators. In this talk, we discuss an alternative approach to protocol verification in which a message passing system is extended with a non-monotonic belief change operator suitable for iterated belief revision. Although we frame the discussion in terms of protocol verification, we are more generally interested in modeling belief change for agents communicating through anonymous message passing. In this context, an agent must be able to retract beliefs in response to new information and also to postulate the most plausible event to explain new information. This kind of reasoning is particularly important when agents may have incorrect initial beliefs.
    Document: http://www.cs.sfu.ca/~hunter/personal/pubs/aaai07.pdf , slides


  • Speaker: Bart Jacobs, Radboud University Nijmegen
    Title: Smart cards in public transport: the Mifare Classic Case
    Abstract: The Mifare Classic chipcard has been dismantled. Between 1 and 2 billion copies have been sold worldwide. The card is mainly used for access to buildings and for public transport. The talk will give an overview of these developments and of the role of the Digital Security Group of the Radboud University Nijmegen.
    Document: http://www.ru.nl/ds/group/ds_group/


  • Speaker: Simon Kramer, Ecole Polytechnique
    Title: Reducing Provability to Knowledge in Multi-Agent Systems
    Abstract: We construct a new reduction of provability to a combination of four kinds of knowledge in multi-agent systems. These kinds are: individual knowledge (knowledge of messages), plain propositional knowledge (knowledge that a state of affairs is the case), common knowledge (propositional knowledge shared in a community of agents), and a new kind of knowledge, namely adductive knowledge (propositional knowledge contingent on the adduction of certain individual knowledge, e.g., through oracle invocation).
    Document: ftp://ftp.research.microsoft.com/pub/tr/TR-2008-90.pdf , slides


  • Speaker: Alessio Lomuscio, Imperial College
    Title: Symbolic model checking temporal epistemic logic and (possible!) applications to the automatic verification of security protocols
    Abstract: While symbolic model checking has a long and successful tradition in systems verification, its uses for richer logics has only been recently explored. In this talk I will summarise some of the work we have been engaged in OBDD- and SAT-based model checking for temporal epistemic logics, present a demonstration of a checker recently released, and try to argue how this methodology may possibly be extended for the verification of some security protocols.
    Document: http://www.doc.ic.ac.uk/~alessio/papers/08/FI-AL-WP.pdf , A. Lomuscio, W. Penczek. Symbolic model checking for temporal epistemic logic.


  • Speaker: Ron van der Meyden, University of New South Wales / NICTA
    Title: Distributed Knowledge and Information Flow Security
    Abstract: not available
    Document: slides


  • Speaker: Catuscia Palamidessi, Ecole Polytechnique
    Title: Formal approaches to Information-Hiding (based on joint work with Konstantinos Chatzikokolakis and Prakash Panangaden)
    Abstract: In this talk we consider the class of protocols for information-hiding which use randomization to obfuscate the link between the observables and the information to be protected. We focus on the problem of formalizing the notion of information hiding, and verifying that a given protocol achieves the intended degree of protection. We review and compare the main approaches that have been explored in literature: possibilistic, probabilistic, information-theoretic, and statistical. Finally, we show how to specify information-hiding protocols and verify them (in the various approaches) using language-based techniques. Slides
    Document: http://www.lix.polytechnique.fr/~catuscia/papers/ProbabilityError/full.pdf.         


Speaker: Ramaswamy Ramanujam & Suresh Salem Purushothaman, Institute of Mathematical Sciences, Chennai
Title: Decidability issues in epistemic logics for security protocols
Abstract: Any study of information security is easily seen to involve reasoning about knowledge and ignorance. However, formal attempts at epistemic reasoning about secure communications (or data) runinto all kinds of trouble, typically giving undecidable logics.The central issue is semantic in nature: if I receive a message mencrypted with a key K then do I know that I have received somemessage m' encrypted with some key K', even if I do not possess the corresponding decryption key? If we wish to retain the abstraction that logics of knowledge offer (along with its nice properties), we need a notion that is midway between the classical notion of knowledge and a notion that makes all undecryptable content indistinguishable. This means that the logic needs explicit primitives for talking about what is and what is not decipherable. Achieving such a design, while ensuring that the verification problem is decidable, is something of a challenge. Nevertheless, we argue that formal models of knowledge do help inspecifying security properties of protocols, and illustrate this claim in the context of protocols for electronic voting.
Document: http://www.imsc.res.in/~jam/tark05.ps.gz , http://www.imsc.res.in/~jam/tark07.pdf


  • Speaker: Michael Rusinowitch, University of Nancy
    : Towards extending constrained-based analysis of security protocols to web-services
    Abstract: We recall the principles of constrained-based analysis of security protocols and some formal results. Then we explain how this approach can be applied to web-service security problems. This is joint work with Yannick Chevalier.
    Document: http://hal.inria.fr/inria-00133996


  • Speaker: Mark Ryan, University of Birmingham
    Title: Verifying privacy-type properties of electronic voting protocols (joint work with Stephanie Delaune and Steve Kremer)
    Abstract: Electronic voting promises the possibility of a convenient, efficient and secure facility for recording and tallying votes in an election. Recently highlighted inadequacies of implemented systems have demonstrated the importance of formally verifying the underlying voting protocols. We study three privacy-type properties of electronic voting protocols: in increasing order of strength, they are vote-privacy, receipt-freeness, and coercion-resistance. We use the applied pi calculus, a formalism well adapted to modelling such protocols, which has the advantages of being based on well-understood concepts. The privacy-type properties are expressed using observational equivalence and we show in accordance with intuition that coercion-resistance implies receipt-freeness, which implies vote-privacy. We illustrate our definitions on three electronic voting protocols from the literature. Ideally, these three properties should hold even if the election officials are corrupt. However, protocols that were designed to satisfy receipt-freeness or coercion-resistance may not do so in the presence of corrupt officials. Our model and definitions allow us to specify and easily change which authorities are supposed to be trustworthy.
    Document: ftp://ftp.cs.bham.ac.uk/pub/authors/M.D.Ryan/07-jcs-voting.pdf


  • Speaker: Rineke Verbrugge, University of Groningen
    Title: Knowledge-based algorithm for multi-agent communication (joint work with Egon van Baars)
    Abstract: Using a knowledge-based approach, we derive a protocol for the sequence transmission problem from one agent to a group of agents. The knowledge-based protocol is correct for communication media where deletion and reordering errors may occur. Furthermore, it is shown that after k rounds the agents in the group attain depth k general knowledge about the members of the group and the values of the messages. Thus, the knowledge-based protocol may be used in cooperative problem solving in order to attain an approximation of common belief among agents in a team.
    Document: http://www.ai.rug.nl/alice/mas/macom/files/LOFT06.pdf


  • Speaker: Thomas Wilke, University of Kiel
    Title: Modal and Temporal Logics for Cryptographic Protocols
    Abstract: A basic requirement for a formal analysis of cryptographic protocols is a formal specification of the desired security properties. In many cases modal or temporal logics have been suggested and used as an appropriate specification formalism. In the talk, I will present some of the results that have been obtained along these lines.