### Abstract

In the context of formal cryptographic protocol verification, logging-independent message anonymity is the property for a given message to remain anonymous despite the attacker's capability of mapping messages of that sort to agents based on some intrinsic feature of such messages, rather than by logging the messages exchanged by legitimate agents as with logging-dependent message anonymity. This paper illustrates how logging-independent message anonymity can be formalized according to the relational method for formal protocol verification by considering a real-world protocol, namely the Restricted Identification one by the BSI. This sample model is used to verify that the pseudonymous identifiers output by user identification tokens remain anonymous under the expected conditions.

### License

BSD License

### Topics

- Computer science/Security

### Session Logging_Independent_Anonymity

- Definitions
- Anonymity
- Possibility

## Cite

×

Logging_Independent_Anonymity-AFP

    @article{Logging_Independent_Anonymity-AFP,
      author  = {Pasquale Noce},
      title   = {Logging-independent Message Anonymity in the Relational Method},
      journal = {Archive of Formal Proofs},
      month   = {August},
      year    = {2021},
      note    = {\url{https://isa-afp.org/entries/Logging_Independent_Anonymity.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Sep 5, 2021 : Isabelle2021