Provable anonymity

F.D. Garcia, I. Hasuo, Wolter Pieters, P.J.B. van Rossum

    Research output: Contribution to conferencePaperAcademicpeer-review

    47 Citations (Scopus)

    Abstract

    This paper provides a formal framework for the analysis of information hiding properties of anonymous communication protocols in terms of epistemic logic. The key ingredient is our notion of observational equivalence, which is based on the cryptographic structure of messages and relations between otherwise random looking messages. Two runs are considered observationally equivalent if a spy cannot discover any meaningful distinction between them. We illustrate our approach by proving sender anonymity and unlinkability for two anonymizing protocols, Onion Routing and Crowds. Moreover, we consider a version of Onion Routing in which we inject a subtle error and show how our framework is capable of capturing this flaw.
    Original languageUndefined
    Pages63-72
    Number of pages10
    DOIs
    Publication statusPublished - 2005
    Event2005 ACM workshop on Formal methods in security engineering - Fairfax, VA, USA
    Duration: 1 Jan 20051 Jan 2005

    Workshop

    Workshop2005 ACM workshop on Formal methods in security engineering
    Period1/01/051/01/05

    Keywords

    • SCS-Cybersecurity
    • IR-62534
    • EWI-14065

    Cite this