Computational Secrecy by Typing for the Pi Calculus

M. Abadi, R.J. Corin, C. Fournet

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    10 Citations (Scopus)

    Abstract

    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.
    Original languageUndefined
    Title of host publicationThe Fourth ASIAN Symposium on Programming Languages and Systems (APLAS 2006)
    EditorsN. Kobayashi
    Place of PublicationLondon
    PublisherSpringer
    Pages253-269
    Number of pages17
    ISBN (Print)3-540-48937-1
    DOIs
    Publication statusPublished - Nov 2006

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Verlag
    Volume4279

    Keywords

    • EWI-6089
    • IR-63179
    • METIS-237434
    • SCS-Cybersecurity

    Cite this

    Abadi, M., Corin, R. J., & Fournet, C. (2006). Computational Secrecy by Typing for the Pi Calculus. In N. Kobayashi (Ed.), The Fourth ASIAN Symposium on Programming Languages and Systems (APLAS 2006) (pp. 253-269). [10.1007/11924661_16] (Lecture Notes in Computer Science; Vol. 4279). London: Springer. https://doi.org/10.1007/11924661_16