Dataflow analysis of the [pi]-calculus

Static analysis [NNH99] is technique used to compute information about the run-time behaviour of a program prior to execution. Traditionally, it has been used in the context of optimizing compilers, but it has recently been applied to more formalized languages in order to develop provable policies that can be used to verify the security of networks. Best results are naturally achieved with the most precise information flow techniques, though complex systems impose feasibility constraints. Accuracy of results, particularly with respect to relative cost of computation is thus an important quality.This thesis presents a series of dataflow analyses of the pi-calculus, an extensively studied concurrent language that has been used to model and verify security protocols. Some of the presented analyses are equivalent to previous work done in the field, but the framework in which the analysis is done is new in that it immediately suggests an iterative implementation.There are also analyses presented that improve on existing approaches in two ways. First, by fully treating the sequentiality of potential actions in a protocol, thereby improving the accuracy of previous approaches. Second, by considering the potential environment that a process could be running in, the computed results are correct independent of any context that the analyzed process may be in parallel composition with