Programme

Track A, Typed $\pi$-Calculus:

A consistent extension of the linear/affine $\pi$-calculus in [12,72] so that it covers all major language constructs in high-level programming languages. A concrete testbed is the fully abstract embeddability of the major part of generic, multi-threaded Java, establishing its faithfulness by reflecting it to the original language. This track is carried out by RA, Yoshida, Wiklicky, Hankin and Di Pierro; with collaboration with other co-authors.

Track B, Qualitative/Quantitative Secrecy Analysis:

This has two subtracks: (a) an extension of the quantitative secrecy analysis developed in [25,26] to the linear/affine $\pi$-calculus; and (b) an extension of the qualitative secrecy analysis in [45,41,75,68] to the enriched typed $\pi$-calculus from Track A. As a testbed, we establish non-interference results (including quantitative non-interference [25] in (b), which means high-level information never flows down to low-level channels under certain probability). (a) is carried out by RA, Yoshida, Wiklicky, Hankin and Di Pierro; while (b) is carried out by PhD, Honda, Yoshida and Berger.

Track C, Experimentation:

This track uses the theories obtained in other tracks for the development of prototypical software tools, and experiment with the developed tools using non-trivial programs with security concerns written in high-level languages such as Java. Along the way we shall also consider incorporation of other security analyses for the $\pi$-calculus as found in [2,3,5,36,33,74] . This track is carried out by PhD, Honda, Berger and Yoshida.

For flexibility tracks overlap with each other. Two subtracks in Track B will be carried out in parallel (with the subtrack (b) incrementally using the results from Track A), while Track C again would use results incrementally produced from Track B.