Andrew D. Gordon
University of Cambridge
Computer Laboratory
http://www.cl.cam.ac.uk/users/adg
Needham defines a pure name to be ``nothing but a bit pattern that is an identifier, and is only useful for comparing for identity with other bit patterns---which includes looking up in tables in order to find other information'' [13]. In this paper, we argue that pure names are relevant to both security and mobility. A nominal calculus is a computational formalism that includes a set of pure names and allows the dynamic generation of fresh, unguessable names. We survey recent work on nominal calculi with primitives representing location failure, process migration and cryptography, and suggest areas for further work.
Needham's definition treats pure names as atoms; on the other hand, an impure name has additional structure of some kind. Perhaps it is a combination of component names; or perhaps there are operations to generate one name from another. To illustrate this distinction, consider the treatment of memory pointers in different programming languages. In Java, for instance, memory pointers are pure names. The type system enforces Needham's abstract view of a bit pattern as a pure name; it allows programs to compare pointers for identity or to de-reference a pointer, but denies other operations, such as pointer arithmetic. On the other hand, in C, for instance, a memory pointer is an impure name; we have direct access to the bit pattern representing the pointer.
To see the relevance of names and nominal calculi to secure mobile code, we begin by considering the pi calculus, a language much smaller than Java or C, and hence a simpler starting point for experimenting with primitives for security or mobility.
The pi calculus of Milner, Parrow and Walker [12] is a nominal calculus in which computations consist of collections of parallel processes equipped with synchronous communication channels. If P and Q are processes, process P par Q consists of P and Q running in parallel, possibly communicating with each other or with the outside world along communication channels. Channels are represented by names. In fact, names are the only data that may be communicated on channels.
Although based on a handful of primitives, the pi calculus is astonishingly expressive. Functional programming may be reduced to the pi calculus, since the lambda calculus can be encoded. Similarly, a variety of formulations of imperative, object-oriented and concurrent programming may be reduced to the pi calculus [10,17,20]. All these encodings depend on the presence of pure names and name generation.
A restriction in the pi calculus is a process of the form (new n)P, which means ``make a fresh, unguessable name n, and then run P.'' Restriction represents name generation in the pi calculus. The name n in the restriction is a bound identifier, whose scope is P. Restricted names are unguessable; you can only learn a restricted name if someone tells you.
A major innovation of the pi calculus is its collection of equational laws for restricted names. (These were inspired, in part, by the earlier work of Engberg and Nielsen [6].) For example, one law asserts that the processes (new n)(P par Q) and P par (new n)Q are the same, provided that the name n does not occur in process P. This law allows the scope of a restricted name to vary. Left to right, it allows scope contraction; right to left, it allows scope expansion. A series of applications of this law, together with other laws, allows the scope of a name to expand and contract as it is passed from one process to another during the course of a computation. In this sense, the scope of a restricted name is mobile. The pi calculus was published as a ``A Calculus of Mobile Processes'' [12] because, unlike almost all previous process calculi, its mobile restrictions can model the passage of knowledge of a communications channel from one process to another.
Several authors observe that stronger senses of process mobility are important for modelling distributed and mobile systems. In summary, the observation is that the primitives of the pi calculus are location transparent, that is, its formal semantics is such that if it were correctly implemented in a distributed system, there would be no way to tell where processes or channels reside.
Amadio and Prasad [3] point out that the pi calculus does not directly model location failure, where a location is a node (for instance, a server or a workstation) in a distributed system. Amadio and Prasad propose a new nominal calculus, the pi-L calculus, in which processes and channels have locations, and in which processes may fail. Names identify locations. They use their calculus to verify a distributed algorithm, intended to withstand location failure.
Synchronisation on global channels is the basic communication primitive of the pi calculus. Many authors note that this is an expensive primitive to implement in a distributed system. One response is to trim the most problematic primitives from the original pi calculus to obtain the choice-free asynchronous pi calculus [9,15]. Another is to drop channel-based communication in favour of other primitives [7].
Let a mobile system be a distributed system in which processes may migrate between locations. Languages for mobile systems include Java, Obliq and Telescript. Process migration is not one of the primitives of the pi calculus. There are, however, nominal calculi, without locations, in which processes may be communicated as values [16,18], and there are recent nominal calculi with process migration as a primitive [2,8].
Having considered mobility, we turn now to the relevance of pure names and nominal calculi to security.
Cryptography is an important way of achieving security in distributed and mobile systems. Generation of fresh random numbers, made from enough bits to be effectively unguessable, is an essential primitive. Such random numbers are pure names; all that matters is their identity. They are used in cryptographic protocols as encryption keys, as nonces---stamps used to prove freshness of a message.
Lampson observes that a cryptographic channel---a channel whose content is encrypted---is identified by the key used for encryption. This observation leads in the pi calculus to modelling keys as names, key generation by restriction, and communication on a cryptographic channel by communication on its key. Unfortunately this encoding is too secure in the sense that it fails to model certain attacks on cryptographic communications: there is no possibility of another process eavesdropping on the channel or of transmitting replayed or spoof messages. Moreover, Abadi observes that communication in the pi calculus enjoys forward secrecy; the secrecy of completed communications is not compromised by the subsequent disclosure of a previously secret channel.
The spi calculus [1] is a version of the pi calculus that allows communication on a cryptographic channel to be modelled as communication on a public channel of a term that represents a ciphertext. The name of the communications channel is public; the name representing the secret encryption key is restricted. An attacker intent on disrupting a protocol is modelled as an arbitrary process that runs alongside the protocol, and which can send or receive on the public channels used by the protocol. The encoding is realistic in that it allows for message replay, and forward secrecy fails. If you transmit a ciphertext on a public channel and then publish the key, the attacker can obtain the plaintext.
There are varieties of the spi calculus with primitives for shared-key cryptography, hashing and public-key cryptography. The spi calculus has been used to specify and verify secrecy and authenticity properties of several cryptographic protocols. The spi calculus is lower level than some well known formalisms for security protocols, such as the BAN logic [4], but it has the advantage that specifications are executable, and that its formal foundations are clear and precise.
We have surveyed the work of many researchers connecting names, security and mobility. We claim that to research secure mobile code, as well as building experimental implementations, there is much to be gained by experimenting with nominal calculi that model the semantics of such implementations.
We can take the pi calculus as a paradigm: start with a syntax of processes, express behaviour via a primitive operational semantics, and represent name generation by the restriction operator. As we have seen, the pi calculus is based on invulnerable and centralized communication channels. Processes are mobile by convention only. But it has been augmented, experimentally, with more realistic primitives for distribution, process migration and cryptography. In the future, we expect to see more such experiments.
As we have seen, this line of work is already well underway. Questions for further work include the following. How can we apply the body of work on timed concurrent calculi to model the timestamps found in cryptographic protocols? How can we model access control mechanisms, such as capabilities? Can we provide a formal foundation for logics of belief such as BAN [4] via operational models such as the spi calculus? Can we model cryptographic certification of the integrity of mobile code? Can we adapt model-checking tools for the pi calculus [19] to proving properties of secure mobile code?
Here are some stylistic issues:
Finally, we expect research into nominal calculi to have several applications:
Conversations with Alan Jeffrey, Robin Milner, Roger Needham and Peter Sewell helped to clarify some of my initial thoughts on this subject. Martín Abadi, Luca Cardelli, Alan Jeffrey, Ole Jensen, Fabio Massacci, Benjamin Pierce and Ian Stark suggested improvements to a draft. This work was supported by a University Research Fellowship awarded by the Royal Society.