We define and study a distributed cryptographic implementation for an asynchronous pi calculus. At the source level, we adapt simple type systems designed for establishing formal secrecy properties. We show that those secrecy properties have counterparts in the implementation, not formally but at the level of bitstrings, and with respect to probabilistic polynomial-time active adversaries. We rely on compilation to a typed intermediate language with a fixed scheduling strategy. While we exploit interesting, previous theorems for that intermediate language, our result appears to be the first computational soundness theorem for a standard process calculus with mobile channels. © Springer-Verlag Berlin Heidelberg 2006.
CITATION STYLE
Abadi, M., Corin, R., & Fournet, C. (2006). Computational secrecy by typing for the Pi calculus. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4279 LNCS, pp. 253–269). Springer Verlag. https://doi.org/10.1007/11924661_16
Mendeley helps you to discover research relevant for your work.