Information Security Seminar 

Electronic voting presents a challenging set of requirements, including verifiability of the result, and incoercibility of the voters. I will review some of the main ideas in the last decade. The body of the talk will focus on my work on formalising the idea of result verifiability. We distinguish three aspects, and use the applied pi calculus to define them. We show how those aspects can be evaluated for a range of election systems in the literature. Election verifiability intuitively appears to conflict with incoercibility; we show that our definition is compatible with our previous definition of coercion resistance and exhibit some systems that satisfy both. Joint work with Steve Kremer and Ben Smyth.

We present a framework for modeling adversaries in security protocol analysis, in which we define a hierarchy of adversary models. These models range from a Dolev-Yao style adversary to more powerful adversaries who can reveal different parts of principals' states during protocol execution. Our adversary models unify and generalize many existing security notions from both the computational and symbolic settings and lead to new, previously unexplored security notions. We extend an existing symbolic protocol-verification tool with our adversary models. This is the first tool that systematically supports notions such as weak perfect forward secrecy, key compromise impersonation, and adversaries capable of state-reveal queries. In extensive case studies, we automatically find new attacks and rediscover known attacks that previously required detailed manual analysis. Joint work with David Basin.

Authorization policies are not stand-alone objects: they are used to selectively permit actions that change the state of a system. Thus, it is desirable to have a framework for reasoning about the semantic consequences of policies. To this end, we extend a rewriting interpretation of linear logic with connectives for modeling affirmation, knowledge, and possession. To cleanly confine semantic effects to the rewrite sequence, we introduce a monad. The result is a richly expressive logic that elegantly integrates policies and their effects. After presenting this logic and its metatheory, we demonstrate its utility by proving properties that relate a simple file system's policies to their semantic consequences. This talk represents joint work with Henry DeYoung.

In the sequel of the talk of Cristina Sernadas we proceed by recognizing that, in some cases, a minimal model extending another can be obtained by iterating a certain construction, like for instance in the context of algebraically closed fields with the Artin's construction. We provide conditions that guarantee the existence of a $\omega$-limit functor identifying such an extension, when the theories are in ${\forall }_2$. The conditions are over the base functor and not the limit functor. The results are illustrated by showing that the theory of ACFs enjoy quantifier elimination. Joint work with Cristina Sernadas.

I give an overview of sequence logic, SL, which allows one to model and reason about agents which

1. are equipped with arbitrary internal logics and
2. can interact over linear time.

Changing the agents’ logic or the model of time can affect correctness of a protocol. Using simple examples, I show how this can be analysed in SL.

In our increasingly on-line world, sophisticated cryptographic protocols are becoming an integral part of the fabric of society. Consequently, it is imperative to be able to rigorously specify and assert the security properties of such protocols. Still, this task has been frustratingly elusive. One main source of difficulty is that security properties of protocols are very sensitive to the specific execution environment, and in particular to the other protocols running in the same system. This talk presents a paradigm for specifying and asserting composable security properties of protocols. These are properties that remain intact regardless of the other protocols running in the system. We review a number of advantages of this approach, including an application that allows to analyze the security of systems with unbounded number of protocol instances, in an efficient and fully automated way.

Offline guessing (or dictionary) attacks are one of the most common vulnerabilities of security protocols. Previous formalizations of offline guessing attacks are essentially extensions of the standard Dolev-Yao model for security protocol analysis with inference rules which model the attacker's guessing capability, such as those proposed by Lowe. However, as pointed out by Vigano et. al., such a set of rules is specialized to a particular set of cryptographic primitives and intruder capabilities, and it is difficult to convince oneself of its completeness. In line with this work, we propose a symbolic method based on equational theories and provide a simple yet general definition of offline guessing attack in our model. We also show that, for a particular but relevant class of equational theories, the problem of deciding whether an attacker can mount an offline guessing attack from a set of terms learned during protocol execution is decidable in polynomial-time, mimicking a result by Delaune and Jacquemard for Lowe's model.

In the context of global computing, information flow security must deal with the decentralized nature of security policies. This issue is particularly challenging when programs are given the flexibility to perform declassifying instructions. In this talk I point out potential unwanted behaviors that can arise in a context where such programs can migrate between computation domains with different security policies. I will then propose programming language techniques, for which soundness can be proven at the global computation level, in order to tackle such unwanted behaviors.

The novel field of quantum computing and quantum information has gathered significant impetus in the last few years, and it has the potential to radically impact the future of information technology. While the successful construction of a large-scale quantum computer may be some years away, secure communication involving quantum cryptography has already been implemented, and equipment for quantum cryptography is commercially available. The major selling point of quantum cryptography is unconditional security. But can this be guaranteed in practice? Even when protocols have been mathematically proved to be secure, it is notoriously difficult to achieve robust and reliable implementations of secure systems. Techniques based on formal verification are now widely used by industry to ensure that (classical) systems meet their specifications. In this talk, I will give an overview of our ongoing work in using such techniques for the modelling and analysis of quantum protocols and, eventually, their implementations. Joint work with Simon Gay and Nick Papanikolaou.

A widespread design approach in distributed applications based on the service-oriented paradigm, such as web-services, consists of clearly separating the enforcement of authorization policies and the workflow of the applications, so that the interplay between the policy level and the workflow level is abstracted away. While such an approach is attractive because it is quite simple and permits one to reason about crucial properties of the policies under consideration, it does not provide the right level of abstraction to specify and reason about the way the workflow may interfere with the policies, and vice versa. For example, the creation of a certificate as a side effect of a workflow operation may enable a policy rule to fire and grant access to a certain resource; without executing the operation, the policy rule should remain inactive. Similarly, policy queries may be used as guards for workflow transitions. In this talk, we present a two-level formal verification framework to overcome these problems and formally reason about the interplay of authorization policies and workflow in service-oriented architectures. This allows us to define and investigate some verification problems for SO applications and give sufficient conditions for their decidability. This is joint work with Michele Barletta and Silvio Ranise.

The notion of the random key graph (now, a.k.a “uniform random intersection graph”) was defined for probabilistic key pre-distribution in wireless sensor networks. Recently, these graphs have been used for a variety of applications, such as recommender systems using global filtering and clustering analysis. While random key graphs are not Erdös-Renyi random graphs (e.g., the probabilities that graph edges exist are not independent of each other), they have similar connectivity properties under the assumption of “full visibility”; i.e., they obey a similar “zero-one” law as Erdös-Renyi graphs for some scaling of their parameters, whenever each node is within communication range of other nodes. In this presentation we explore various applications of random key graphs ranging from mobile networks, to trust establishment, to social networks. This is joint work with Haowen Chan and Adrian Perrig.

Network hacking is a growing as a nightmare for security engineers. Apart from the traditional single machine hacking, attackers use the network in a distributed way to both carry out and hide their attacks. In this talk, an overview of current network hacking techniques and trends is given. Some cases of study will be explained and discussed. Finally, defense techniques are also highlighted.

There are two main approaches to the analysis of security protocols. The first is a computational approach: a message is a bit string, an attacker is modeled as a probabilistic polynomial-time interactive Turing machine, and security properties are defined as an indistinguishability game. The analysis of protocols in this approach is based on computational complexity theory and takes account of the probability that the attacker breaks the security of cryptographic primitives. The second is a symbolic approach: a message is abstracted into a symbolic expression, an attacker is a symbolic process, and security properties, such as anonymity, can be expressed by the observational equivalence of processes. The analysis in this approach assumes ideally secure cryptographic primitives and is simple to automate. Starting with the seminal work of Abadi and Rogaway, there have been several results showing the computational soundness of the symbolic approach: security proofs in the symbolic approach imply strong security guarantees based on computational complexity theory. We extend Comon-Lundh and Cortier's recent work to show the computational soundness of the applied pi-calculus for a public-key encryption scheme and a ring signature scheme in the presence of active adversaries: the observational equivalence between two processes in the applied pi-calculus implies the computational indistinguishability between the computational executions of the two processes. Our proof for computational soundness is different from all existing studies in that it does not use a computable parsing function from bitstrings to terms. With the primitives that are considered here, it would not be a big additional hypothesis to assume such a parsing function. However, conceptually, this yields different proofs, which may allow us to obtain other soundness results such as XOR or hashing, while such proofs could not be conducted in a simulatability framework called the BPW model.

We reduce the problem of factoring a Blum integer to the problem of (numerically) integrating a certain meromorphic function. We provide two algorithms to address this problem, one based on the residue theorem and the other in the (generalized) Cauchy's argument principle. In the former algorithm, we show that computing the residue of the function at a certain pole leads to obtain the factors of a Blum integer. In the latter, we consider a contour integral that simplifies to an integral over the real numbers for which we are able to obtain an analytical solution with several branches. The computational hardness amounts to discovering the branch of the solution that gives the precise integral. Joint on going work with Vitor Rocha Vieira.

We propose a generic modelling technique that can be used to extend existing frameworks for the theoretical security analysis of cryptographic protocols in order to formally capture the use of timestamps. For concreteness, we apply this technique to two of the most popular models adopted in literature: the family of models stemming from the work of Bellare and Rogaway (BR) and the model proposed by Canetti and Krawczyk (CK). We analyse previous results obtained using these models in light of the proposed extensions, and demonstrate their application to a new class of protocols. In the timed CK model we concentrate on modular design and analysis of protocols. We show that the original authenticated and unauthenticated models are not made redundant by their timed variants: one can still use them to analyse time-independent protocols, and the results naturally carry over to the timed models. Moreover, we propose a more efficient timed authenticator relying on timestamps. The structure of this new authenticator and the security proof we provide imply that a signature-based unilateral authentication mechanism standardised in ISO-9798 is secure for message authentication. Finally, we use our timed extension to the BR model to establish the security of an efficient ISO protocol for key transport and unilateral entity authentication, for which no proof of security was previously available.

In recent years, a number of works have appeared that provide formal definitions of the notion of channel and how different kinds of channels (e.g. authentic, confidential, secure) can be employed in security protocols and web services as a means of securing the communication. In this talk, I will present work that allows us to specify the properties of message exchanges over different kinds of channels, either as an assumption or as a goal, and where communicating agents can use their real names or some pseudonyms. Joint work with Sebastian Moedersheim.

In the research of the relationship between the symbolic and the computational view of cryptography, a recent approach uses static equivalence from cryptographic pi calculi as a notion of symbolic indistinguishability. Previous work has shown that this yields the soundness of natural interpretations of some interesting equational theories, such as certain cryptographic operations and a theory of XOR. However, we argue that static equivalence is too coarse to allow sound interpretations of many natural and useful equational theories. We illustrate this with several explicit examples in which static equivalence fails to work. To fix the problem, we propose a notion of symbolic indistinguishability that is more flexible than static equivalence. We provide general results, and then discuss how this new notion works for the explicit examples where static equivalence fails to ensure soundness. Joint work with P. Mohassel and T. Stegers.

Memory models define an interface between programs written in some language and their implementation, determining which behaviour the memory (and thus a program) is allowed to have in a given model. A minimal guarantee memory models should provide to the programmer is that well-synchronized, that is, data-race free code has a standard semantics. Traditionally, memory models are defined axiomatically, setting constraints on the order in which memory operations are allowed to occur, and the programming language semantics is implicit as determining some of these constraints. In this work we propose a new approach to formalizing a memory model in which the model itself is part of a weak operational semantics for a (possibly concurrent) programming language. We formalize in this way a model that allows write operations to the store to be buffered. This enables us to derive the ordering constraints from the weak semantics of programs, and to prove, at the programming language level, that the weak semantics implements the usual interleaving semantics for data-race free programs, hence in particular that it implements the usual semantics for sequential code.

It is common knowledge that cryptographic schemes are constructed to resist attacks guided by malicious attempts to deviate some intended functionality. However, very little is known about the level of security that we get by using cryptographic schemes in different environments, since security depends on the strength of the adversary. How much can we assume about an unknown adversary without compromising security? On one hand, many works that aim at proving that programs which use cryptography are secure assume specific strategies that the adversary may or may not use when attacking the system. Unfortunately, experience shows that limitations to the power of the adversary are not always realistic. On the other hand, the area of provable or computational cryptography that started to develop since the early 90s proposes that the only assumptions on the adversary that can be justified are his/her computational abilities. Reasoning with arbitrary adversaries involves the handling of polynomial and probabilistic hypotheses on complex programs. Can we let the programmer specify security policies at an abstract level and let the compiler implement them using provable cryptography? This talk will describe work in progress with Cedric Fournet and Gurvan Le Guernic on programming language abstractions for provable cryptography, and a compiler that implements it. A preliminary result of this work appeared in POPL'08.

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. In the context of the AVANTSSAR project, we have techanically 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. This work was carried out by A. Armando, R. Carbone, L. Compagna, J. Cuellar, L. Tobarra Abad in the context of the FP7 Project AVANTSSAR coordinated by L. Viganò