Calculi and verification techniques for security and mobility, 1999-2001

The family of pi-calculi provides a rich mathematical theory for studying the properties of systems whose communication properties change dynamically. An important spin-off of this theory is the Mobility Workbench, an automatic software tool for verifying properties of pi-calculus processes. Recently, Abadi, Gordon and others have used the closely related {\em spi-calculus} to describe the behaviour of security protocols. The project has as a main goal that of developing the theory of the spi-calculus and to use it in the construction of a software tool for verifying properties of security protocols, and subsequently integrating this tool with the Mobility Workbench, if possible. The project is a collaborative effort involving colleagues at Uppsala University and is funded by Göran Gustafssons Stiftelse (The Göran Gustafsson Foundation, a Swedish foundation for basic research in the natural sciences). (Hans Hüttel, Josva Kleist; Uwe Nestmann, Björn Victor, Uppsala University)