diff --git a/web/entries/Logging_Independent_Anonymity.html b/web/entries/Logging_Independent_Anonymity.html --- a/web/entries/Logging_Independent_Anonymity.html +++ b/web/entries/Logging_Independent_Anonymity.html @@ -1,208 +1,209 @@ Logging-independent Message Anonymity in the Relational Method - Archive of Formal Proofs







Logging-independent Message Anonymity in the Relational Method


Title: Logging-independent Message Anonymity in the Relational Method
Author: Pasquale Noce (pasquale /dot/ noce /dot/ lavoro /at/ gmail /dot/ com)
Submission date: 2021-08-26
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.
   author  = {Pasquale Noce},
   title   = {Logging-independent Message Anonymity in the Relational Method},
   journal = {Archive of Formal Proofs},
   month   = aug,
   year    = 2021,
   note    = {\url{https://isa-afp.org/entries/Logging_Independent_Anonymity.html},
             Formal proof development},
   ISSN    = {2150-914x},
License: BSD License

\ No newline at end of file diff --git a/web/statistics.html b/web/statistics.html --- a/web/statistics.html +++ b/web/statistics.html @@ -1,302 +1,302 @@ Archive of Formal Proofs










Number of Articles:672
Number of Authors:424
Number of lemmas:~196,100
Lines of Code:~3,391,200

Most used AFP articles:

NameUsed by ? articles
1. List-Index 20
2. Collections 14
Show 14
3. Coinductive 12
Jordan_Normal_Form 12
Regular-Sets 12
4. Landau_Symbols 11
Polynomial_Factorization 11
5. Abstract-Rewriting 10
Automatic_Refinement 10
Deriving 10

Growth in number of articles:

Growth in lines of code:

Growth in number of authors:

Size of articles:

\ No newline at end of file