Related Work

At the beginning of Background, we mentioned the past tradition in the use of universal languages in program analyses/optimisation. Recent surveys and textbooks [56,8,57] compile diverse existing PAs, developed using specific languages/formalisms. Bodei and others [15,16] presents a basic control flow analysis of the untyped $\pi$-calculus, though their analysis does not reach the precision of the standard PA of real programming languages, due to the lack of types. Our secrecy typing in [45,41] unifies representative approaches to type-based secure information flow in [,,,,,] using the linear/affine type structure.

Typed $\lambda$-calculi are often used a general meta-language for type-based program analyses (cf. [56,8,57]). Two aspects make the $\pi$-calculus a much better candidate than the $\lambda$-calculus in the context of the present project: (1) The (typed and untyped) $\lambda$-calculi in general do not offer fully abstract embedding of different formalisms and programming languages [60]; and (2) they are not amenable to the representation of ``impure'' features such as side effects and concurrency. It is notable that the linear/affine $\pi$-calculus (via its close connection with game-based semantics) allows a fully abstract embedding of typed $\lambda$-calculi: this allows a smooth integration of related studies based on the $\lambda$-calculus into the present work, while extending them non-trivially using the powerful representation power of name passing processes.

There are a growing number of proposals on analyses of security and cryptography using the $\pi$-calculus (cf. [2,3,5,36,33,74]). Software which uses various security features is most likely written with traditional concepts such as procedures, objects, sequencing, assignments and loop, combined with constructs enabling, for example, communication between different agents. The uniform platform of PA resulting from the present project, which encompasses diverse primitives and behaviours, would open the possibility to apply these techniques directly to source code of existing software.

Quantitative secrecy is a young field, with two leading research groups located in London [18,25,26]. Clark and others [18] focus more on information theoretic aspects, while our work [25,26] focus on probabilistic aspect. Our recent work [26] recast the quantitative secrecy in the setting of probabilistic transition systems, offering an essential basis for its extension to the $\pi$-calculus.