StatVerif: Modelling protocols that involve persistent state
7 December 2011
Protocol Analysis

ProVerif's process calculus is extended with constructs for explicit state, in order to be able to reason about protocols that manipulate global state. Global state is required by protocols used in hardware devices (such as smart cards and the TPM), as well as by protocols involving databases that store persistent information.

Cloud Computing Security
6 February 2012
Protocol Analysis

Cloud computing means entrusting data to computers that are managed by third parties on remote servers, raising new privacy and confidentiality concerns. We propose a general technique, based on key translations and mixes in web browsers, for designing protocols that allows servers to see only encrypted data, while still allowing it to perform data-dependent computations. We focus on the particular cloud computing application of conference management.

The Future of Privacy (given at the University of Canberra)
February 2012

Computers have brought about enormous changes in all aspects of our lives over the last 20 years. The next 20 years are likely to see changes of even bigger magnitude. Soon, every fact about us, and every one of our movements, our utterances, and perhaps even our thoughts, will be routinely recorded by computers. Controlling who has access to this information is becoming a great technological challenge, as mobile and cloud-based services are adopted widely. The information may be deliberately or inadvertently made available on a wide scale. The lecture discusses these problems and some relevant research.

Big Brother and Little Brother: The Future of Privacy (Inaugural Lecture)
17 May 2011

Computers have brought about enormous changes in all aspects of our lives over the last 20 years. The next 20 years are likely to see changes of even bigger magnitude. Soon, every fact about us, and every one of our movements, our utterances, and perhaps even our thoughts, will be routinely recorded by computers. Controlling who has access to this information is becoming a great technological challenge, as mobile and cloud-based services are adopted widely. The information may be deliberately or inadvertently made available on a wide scale. The lecture discusses these problems and some relevant research.

Caveat Coercitor
6 April 2011
Electronic Voting

Recently proposed voting systems aim to satisfy strong forms of incoercibility and verifiability, but in doing so it may be argued that they compromise usability.

We present a voting system called Caveat Coercitor that tries to be more pragmatic than, for example, JCJ/Civitas, placing only what we consider realisable requirements on voters, and giving voters a high degree of usability and flexibility about how they participate in the process. The system has some features to avoid coercion; more specifically, the best that a coercer can achieve is forced-abstention. Moreover, Caveat Coercitor has the unusual feature of coercion evidence.

Privacy-supporting cloud-based conference systems: protocol and verification
2011

Cloud computing raises privacy and confidentiality concerns because the service provider necessarily has access to users' data, and could accidentally or deliberately disclose it. We show that, for a significant class of systems, the requirement of cloud-side data processing is small enough that it is possible to use client-side encryption on the sensitive data, while revealing just enough insensitive data to the cloud provider to enable it to perform the required processing.

Formal analysis of electronic voting systems
September 2009
Electronic Voting

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. The applied pi calculus is a formalism for modelling such protocols, and allows us to verify properties by using automatic tools, and to rely on manual proof techniques for cases that automatic tools are unable to handle. We model a known protocol for elections known as FOO 92 in the applied pi calculus, and we formalise three of its expected properties, namely fairness, eligibility, and privacy. We use the ProVerif tool to prove that the first two properties are satisfied. In the case of the third property, ProVerif is unable to prove it directly, because its ability to prove observational equivalence between processes is not complete. We provide a manual proof of the required equivalence.

Verifying Cryptographic Protocols in the Applied Pi Calculus
April 2010
Protocol Analysis

The applied pi calculus is a language for modelling security protocols. It is an extension of the pi calculus, a language for studying concurrency and process interaction. This chapter presents the applied pi calculus in a tutorial style. It describes reachability, correspondence and observational equivalence properties, with examples showing how to model secrecy, authentication and privacy aspects of protocols.

Towards Verified C specification for TPM API
April 2009
Trusted Computing

Abstract. We develop a reference implementation for a fragment of the API for a Trusted Platform Module. Our code is written in a functional language, suitable for verification with various tools, but is automatically translated to a subset of C, suitable for interoperability testing with production code, and for inclusion in a specification or standard for the API. One version of our code corresponds to the widely deployed TPM 1.2 specification, and is vulnerable to a recently discovered dictionary attack; verification of secrecy properties of this version fails producing an attack trace and highlights an ambiguity in the specification that has security implications. Another version of our code corresponds to a suggested amendment to the TPM 1.2 specification; verification of this version succeeds. From this case study we conclude that recent advances in tools for verifying implementation code for cryptographic APIs are reaching the point where it is viable to develop verified reference implementations. Moreover, the published code can be in a widely understood language like C, rather than one of the specialist formalisms aimed at modelling cryptographic protocols.

Solution to ensure TPM resistance to offline dictionary attack
June 2008
Trusted Computing

The Trusted Platform Module (TPM) is a hardware chip designed to enable PCs achieve greater security. Proof of possession of values known as authData is required by user processes in order to use TPM keys. We show that in certain circumstances dictionary attacks can be performed offline on authdata. In this way, an attacker can circumvent some crucial operations of the TPM, and impersonate the TPM owner to the TPM, or the TPM to its owner. For example, he can unbind data or migrate keys without possessing the required authorisation data, or fake the creation of TPM keys. This means that any application that relies on the TPM may be vulnerable to attack. We propose a new solution and some modifications to the TPM specification to prevent the offline attacks, and we also provide the way to integrate these modifications into the TPM command architecture with minimal change. With our solution, the user can use a password-type of weak secret as their authData, and the TPM system will be still safe.

Composition of Password-based Protocols
June 2008
Protocol Analysis

We investigate the composition of protocols that share a common secret. This situation arises when users employ the same password on different services. More precisely we study whether resistance against guessing attacks composes when the same password is used. We model guessing attacks using a common definition based on static equivalence in a cryptographic process calculus close to the applied pi calculus. We show that resistance against guessing attacks composes in the presence of a passive attacker. However, composition does not preserve resistance against guessing attacks for an active attacker. We therefore propose a simple syntactic criterion under which we show this composition to hold. Finally, we present a protocol transformation that ensures this syntactic criterion and preserves resistance against guessing attacks.

Direct Anonymous Attestation (DAA): Ensuring privacy with corrupt administrators
February 2007
Trusted Computing

The Direct Anonymous Attestation (DAA) scheme provides a means for remotely authenticating a trusted platform whilst preserving the user's privacy. The protocol has been adopted by the Trusted Computing Group (TCG) in the latest version of its Trusted Platform Module (TPM) specification. In this paper we show DAA places an unnecessarily large burden on the TPM host. We demonstrate how corrupt administrators can exploit this weakness to violate privacy. The paper provides a fix for the vulnerability. Further privacy issues concerning linkability are identified and a framework for their resolution is developed. In addition an optimisation to reduce the number of messages exchanged is proposed.

Improved multi-party contract signing
May 2007
Protocol Analysis

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. Such 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. Two multi-party contract signing protocols have been proposed so far. One solution to this problem was proposed by Garay and MacKenzie based on private contract signatures, but it was subsequently shown to be fundamentally flawed (it fails the fairness property). more efficient protocol was proposed by Baum-Waidner and Waidner. It has not been compromised, but it is based on a non-standard notion of a signed contract. In this paper, we propose a new optimistic multi-party contract signing protocol based on private contract signatures. It does not use a non-standard notion of a signed contract and has half the message complexity of the previous solution.

Resolve-impossibility for a contract signing protocol
July 2006
Protocol Analysis

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. Such a protocol was introduced by Garay and MacKenzie in 1999; it consists of a main protocol and a sub-protocol involving a trusted party. Their protocol was shown to have a flaw by Chadha, Kremer and Scedrov in CSFW 2004. Those authors also presented a fix - a revised sub-protocol for the trusted party. In our work, we show an attack on the revised protocol for any number n > 4 of signers. Furthermore, we generalise our attack to show that the message exchange structure of Garay and MacKenzie'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".

Anonymity with Identity Escrow
March 2006
Protocol Analysis

Anonymity with identity escrow attempts to allow users of a service to remain anonymous, while providing the possibility that the service owner can break the anonymity in exceptional circumstances, such as to assist in a criminal investigation. A protocol for achieving anonymity with identity escrow has been presented by Marshall and Molina-Jiminez. In this paper, we show that that protocol suffers from some serious flaws. We also identify some other less significant weaknesses of the protocol, and we present an improved protocol which fixes these flaws. Our improved protocol guarantees anonymity even if all but one of the escrow holders are corrupt.

Coercion-Resistance and Receipt-Freeness in Electronic Voting
August 2006
Electronic Voting

In this paper we formally study important properties of electronic voting protocols. In particular we are interested in coercion-resistance and receipt-freeness. Intuitively, an election protocol is coercion-resistant if a voter A cannot prove to a potential coercer C that she voted in a particular way. We assume that A cooperates with C in an interactive fashion. Receipt-freeness is a weaker property, for which we assume that A and C cannot interact during the protocol: to break receipt-freeness, A later provides evidence (the receipt) of how she voted. While receipt-freeness can be expressed using observational equivalence from the applied pi calculus, we need to introduce a new relation to capture coercion-resistance. Our formalization of coercion-resistance and receipt-freeness are quite different. Nevertheless, we show in accordance with intuition that coercion-resistance implies receipt-freeness, which implies privacy, the basic anonymity property of voting protocols, as defined in previous work. Finally we illustrate the definitions on a simplified version of the Lee et al. voting protool.

Some issues in verifying e-voting systems
June 2005
Electronic Voting
(no abstract)
Evaluating Access Control Policies through Model Checking
September 2005
Access Control Systems

We present a model-checking algorithm which can be used to evaluate access control policies, and a tool which implements it. The evaluation includes not only assessing whether the policies give legitimate users enough permissions to reach their goals, but also checking whether the policies prevent intruders from reaching their malicious goals. Policies of the access control system and goals of agents must be described in the access control description and specification language introduced as RW in our earlier work. The algorithm takes a policy description and a goal as input and performs two modes of checking. In the assessing mode, the algorithm searches for strategies consisting of reading and writing steps which allow the agents to achieve their goals no matter what states the system may be driven into during the execution of the strategies. In the intrusion detection mode, a weaker notion of strategy is used, reflecting the willingness of intruders to guess the value of attributes which they cannot read.