Adopting a programming-language perspective, we study the problem of implementing authentication in a distributed system. We define a process calculus with constructs for authentication and show how this calculus can be translated to a lower-level language using marshalling, multiplexing, and cryptographic protocols. Authentication serves for identity-based security in the source language and enables simplifications in the translation. We reason about correctness relying on the concepts of observational equivalence. (This is joint work with Martin Abadi and Georges Gonthier)

The increased technical availability provided by mobile communication necessitates support for users so that they can control their personal reachability (personal reachability management). This talk reports on a PDA and mobile phone based prototype functioning primarily as a reachability manager to avoid annoying calls and overcome the CallerID problem. Its core functionality is to enable parties to negotiate, e.g. the urgency of a telephone call, and by that maintain security that respects the interests of all involved parties (multilateral security).

The RSA cryptosystem is very widely used. A particularly visible application is to protect and authenticate e-commerce transactions and it has been estimated that about 95% of all web-based e-commerce uses 512-bit RSA keys. As the security of RSA is no better than the difficulty of factoring a key's public modulus, progress in integer factorisation directly measures the security of RSA keys of any particular size.

Smart cards can be formalised realistically within Paulson's inductive approach for security protocols. The cards can be stolen and/or cracked by an eavesdropper. The kernel of their built-in algorithm works correctly, so they can't be used as oracles, but their I/O interface doesn't, so they send correct outputs unreliably.

In the past few years elliptic curve cryptography has moved from a fringe activity to a major challenger to the dominant RSA/DSA systems. Elliptic curves offer major advances on older systems such as increased speed, less memory and smaller key sizes. As digital signatures become more and more important in the commercial world the use of elliptic curve-based signatures will become all pervasive.

Model checking is a method of formally verifying properties of finite state machines. By describing operating system structure and system authorization policies using finite state machines, model checking may be used to verify useful properties of policies, improving the chances of developing a secure system. The technique is demonstrated on authorization systems from an Active Network, and from a simplified UNIX-like environment.

Modern interconnected computer systems handling classified information can be built using Windows NT. The architecture provides each user with a private desktop in which to work, along with services for sharing data. Within a desktop, the user is helped to attach security labels to their data. When data is shared, labelling prevents accidental compromise, but other measures defend against other forms of compromise.

Most approaches to formal verification of authentication protocols assume encryption to have the property that parts of a message cannot be extracted without knowledge of the encrypting key. In practice, implementations are not perfect in this sense and the correctness of a protocol may depend on the algebraic properties of encryption.

Traditionally, cryptographic protocols are described in terms of a sequence of steps, each of which sees one principal sending a message to another principal. It is implicitly assumed that the fundamental communication primitive is necessarily one-to-one and protocols addressing anonymity tend to resort to a highly redundant composition of multiple elementary transmissions in order to frustrate traffic analysis. This talk, building on the case study of an anonymous auction between mistrustful principals with no trusted arbitrator, presents "anonymous broadcast" as a new protocol building block. This lower-level primitive is, in its class of cases, a more accurate model of what actually happens in local area networking and, with certain restrictions, can be used as a particularly efficient implementation technique for many anonymity-related protocols.

A large variety of encryption schemes, or modes, have been proposed to date, and some of these are known to be secure against adaptive, chosen-plaintext attacks. In this presentation, I define a joint condition on any such secure scheme and any high-performance Manipulation Detection Code (hpMDC) function, such as XOR, CRC-32, modular addition, or simply a constant, to counter adaptive chosen-message attacks, namely both adaptive chosen-plaintext and chosen-ciphertext attacks, that lead to message forgeries. I also illustrate two applications of the joint condition in practice, namely (1) the design of fast encryption-with-integrity schemes and (2) the optimal selection of a hpMDC function for a given encryption scheme.

Rivest suggested the idea of multi-grade cryptography, which lets a cryptosystem present multiple levels of security under different circumstances. For instance, to an external law enforcement agent, the cryptosystems of the users in an organisation might show a high level of security (e.g., equivalent to a 64-bit key-search). Once this high-level security ``shell'' is broken with a non-tivial effort, each user's key becomes an easier computational problem (e.g., 40-bit key-search). To any other parties who cannot afford to break the shell, user security is an intractable problem. An important point in muti-grade cryptgraphy is that the external law enforcement agent should only need to break the an organisation's shell once.

Let us consider the case of the company president who delegates the power to sign certain documents to her secretary. If the president never cheats, then many existing mechanisms are sufficient to implement this. But what if the president suddenly announces that her secretary has been sacked because of a mistake in a very important document? It may well be that the secretary did not made a mistake: but with almost all the existing mechanisms, she has no way of demonstrating that it was the president, and not she, who created or authorised the disputed document.

IBM has been working in the field of Secure Cryptographic Coprocessors since the early 1980's. This talk will briefly discuss the history of IBM's efforts, then go on to discuss the hardware architecture in and the physical security design.

The hardware architecture will be shown from a performance standpoint, discussing the ideas that worked and the ones that didn't.

The physical security design was the first ever to be validated at FIPS 140-1 level 4. The principles of the design will be described and the manufacturing implications will be discussed.

Presentation material

As the value of data on computing systems increases and operating systems become more secure, physical attacks on computing systems to steal or modify assets become more likely. This technology requires constant review and improvement, just as other competitive technologies need review to stay at the leading edge.

This talk describes known physical attacks ranging from simple attacks which require little skill or resource, to complex attacks which require trained, technical people and considerable resources. Physical security methods to deter or prevent these attacks are presented. The intent is to match protection methods with the attack methods in terms of complexity and cost. In this way cost effective protection can be produced across a wide range of systems and needs.

Specific technical mechanisms now in use will be discussed, as well as mechanisms proposed for future use. Common design problems and solutions are discussed with consideration for manufacturing.

Presentation material

This talk is an overview of the Oasis access control architecture. This provides both a means for specifying complex authorisation information in an open distributed environment, and an efficient implementation.

Recent years have seen a great proliferation of papers on watermarking of digital data. These have usually started from a very generalised view of the nature of the data and concentrated on the quality of the security algorithm.

The recent synthesis of quantum physics with computer science has led to a new paradigm for computation which is in principle physically realisable, yet not fully encompassed by the standard (e.g. Turing) notion of computability. A quantum computer cannot compute any non-Turing-computable function but it appears to be able to perform some computations exponentially faster than any classical device. The pre-eminent example is the existence of a polynomial-time quantum algorithm for integer factorisation - a problem for which there is no known classical (even randomised) efficient algorithm. In recent developments, quantum physics also gives rise to new modes of communication and an associated quantum information theory.

In this talk I will introduce the essential principles of quantum computation and outline the structure of some fundamental quantum algorithms. I will discuss the relation of quantum computation to various classical complexity classes and finally consider some recent issues of current interest.

This talk will be held in the Babbage Lecture Theatre. Maps and travelling directions are at http://www.cl.cam.ac.uk/site-maps/site-maps.html.

It is a popular conjecture that the design of authentication is an error prone and hence difficult task. Once again, I will try to explain how this situation may have come about.

As a general observation, one may note that in many areas of science progress in the understanding of fundamental concepts has gone hand in hand with the development of a language for discussing these concepts. The difficulty of giving good definitions for authentication bears witness to this problem. In a specific observation on authentication, I will illustrate that the term authentication is used in a number of different security paradigms, a fact that can only add further confusion.

Not surprisingly, I will argue that more precision in the discourse about authentication is required. In this respect, designers and attackers have been equally culpable so far.

In its Advanced Encryption Standard (AES) programme the US National Institute of Standards and Technology has selected 15 algorithms for consideration as candidates to replace the now obsolescent DES standard.

This talk will look at some of the issues that the author has faced in implementing all 15 candidates from scratch. The coverage will focus on implementation and performance rather than on security or cryptanalysis. In particular the issues involved in using algorithm specifications as a basis for implementation in C will be discussed, as will some of the surprises involved in running such code on modern pipelined/semi-parallel architecures such as the Pentium II. The talk will also cover an interesting aspect of performance optimisation for Serpent.

Presentation material

The richest, strongest, most electronically-vulnerable nation on earth persists in a policy that effectively restricts the use of encryption technology domestically as well as abroad. Even while the security of transactions over telephone and computer networks has become a source of wide public concern, the US government continues to work against the proliferation of unbreakable cryptography (and thus perfectly concealable communications).

In this talk we present a brief history of wiretap law and privacy rulings in the United States, and we put current crypto policy in the context of decisions made over the last twenty years.