[isabelle] New AFP entry: Logging-independent Message Anonymity in the Relational Method
- To: isabelle-users <isabelle-users at cl.cam.ac.uk>, pasquale.noce.lavoro at gmail.com
- Subject: [isabelle] New AFP entry: Logging-independent Message Anonymity in the Relational Method
- From: Andreas Lochbihler <mail at andreas-lochbihler.de>
- Date: Sun, 5 Sep 2021 09:45:12 +0200
- Authentication-results: cam.ac.uk; iprev=pass (mta0.cl.cam.ac.uk) smtp.remote-ip=126.96.36.199; spf=fail smtp.mailfrom=andreas-lochbihler.de; arc=none
- Authentication-results: cam.ac.uk; iprev=pass (wp589.webpack.hosteurope.de) smtp.remote-ip=188.8.131.52; spf=pass smtp.mailfrom=andreas-lochbihler.de; arc=none
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:78.0) Gecko/20100101 Thunderbird/78.13.0
I'm happy to announce a new entry, Logging-independent Message Anonymity in the Relational
Method, by Pasquale Noce:
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.
You'll find it at https://www.isa-afp.org/entries/Logging_Independent_Anonymity.html
The modelling of the security protocol is exceptionally well-documented!
This archive was generated by a fusion of
Pipermail (Mailman edition) and