Notes on Nominal Calculi for Security and Mobility

There is great interest in applying nominal calculi—computational formalisms that include dynamic name generation—to the problems of programming, specifying, and verifying secure and mobile computations. These notes introduce three nominal calculi—the pi calculus, the spi calculus, and the ambient calculus. We describe some typical techniques, and survey related work.