Mobile values, new names, and secure communication

We study the interaction of the "new" construct with a rich but common form of (first-order) communication. This interaction is crucial in security pr otocols, which are the main motivating examples for our work; it also appea rs in other programming-language contexts. Specifically, we introduce a sim ple, general extension of the pi calculus with value passing, primitive fun ctions, and equations among terms. We develop semantics and proof technique s for this extended language and apply them in reasoning about some securit y protocols.