# Decentralized Identity Authentication with Auditability and Privacy
## 5 Privacy-Preserving Protocol
### Final Protocol
#### 5.2.1 New Token and Its Consistency
#### 5.2.3 Discussion

This protocol hides token-identity mappings and login frequency from an adversary observing the blockchain (i.e., the adversary sees new tokens, but is unable to link them to their originators or other tokens). However, if a client uses its identity with a service multiple times, the service learns the corresponding counters. Any pair of counters allows the service to deduce how many authentications with other services for which the identity has been used between these two counters. Although we do not believe that this is a major privacy issue, our protocol can be extended with the following modifications to mitigate it:

1. Prior to the registration, the client generates its counter \(cnt\) as a large secret number. 2. For every authentication, a new token and its proof are computed as \(\langle tkn,\gamma\rangle\gets VRF_{sk}(H(cnt))\) (the only difference is that the counter is internally hashed). 3. The service receives \(H(cnt)\)--not \(cnt\), as previously--and verifies the token's authenticity by calling \(\forall rgyVRF_{rk}(H(cnt),tkn,\gamma)\). 4. The circuit verifies two tokens analogically, thus guaranteeing that the hashes are for the two consecutive values. These changes would hide counter values from services, as they would learn only counters' hashes. This would eliminate the mentioned privacy leak; however, it would require a more complicated circuit. ## 6 Security Proofs with Tamarin

We used the Tamarin Prover [42] to prove the security properties that provide both auditability and privacy for the DID authentication protocol. To the best of our knowledge, this is the first formal security modeling of a DID authentication protocol. All of the Tamarin code can be found in [43]. ### The Tamarin Prover

The Tamarin Prover [42] is a powerful automated tool for the modeling and analysis of security protocols. In Tamarin, protocols and adversaries are described by using multiset rewriting rules, and trace properties such as authentication and secrecy are specified in first-order logical statements. These rules are represented by states or facts in which the symbolic representation of the adversary's knowledge, network messages, and freshly generated information are stored. The protocols and adversaries interact by updating and generating network messages based on the rules. The security properties are modeled as trace properties, which specify a sequence of the rules' actions. Tamarin works on the Dolev-Yao (DY) model, which is a symbolic model in which messages are represented as terms. In the DY model, the attacker controls the network, can see all of the messages, and can manipulate, block, or re-order them. However, the attacker is not capable of breaking cryptographic primitives, such as forging the signature. In the Tamarin protocol, execution is represented by a labeled state transition system. A _state_ is a finite multiset of facts that include arguments of the state and their current snapshots of protocol execution. The facts include the local states of all participants, messages sent over the network, and messages that an attacker can construct from these messages. The action performed by the protocol participants and the attacker is specified by _rules_, which rewrite one state to another. The _rules_ are of the form \(a-[b]-->c\), where \(a\) is a set of premises, \(b\) is a set of actions (optional), and \(c\) is a set of conclusions. Executing the rules requires all premises to be currently present in the state, satisfy requirements of all actions, and result in adding conclusions to the state while the premises are deleted. The following are some of the important prefixes used in Tamarin:

1. \(\sim x\) denotes the fresh variable \(x\);
2.