# Decentralized Identity Authentication with Auditability and Privacy
## 5 Privacy-Preserving Protocol
### Final Protocol
#### 5.2.1 New Token and Its Consistency
: _A DID authentication protocol can achieve auditability and privacy with honest client \(C\), honest service \(S\), and blockchain \(B\) if \(C\) can register an identity on \(B\), use it to authenticate with \(S\), and successfully and anonymously log the event onto \(B\); then, \(C\) holds a valid identity on \(B\), and an adversary has not used it to authenticate to an honest \(S\)._

For the DID authentication protocol, we use the following formalization. lemma executable: exists-trace  \"Ex #i. Finish() @i  & (All x y #i #j. (Send_RR(x)@i & Send_RR(y)@j)  ==> x = y & #i = #j)  & (All x y #i #j. (Recv_RR(x)@i & Recv_RR(y)@j)  ==> x = y & #i = #j)  & (All x y #i #j. (Send_to_service(x)@i & Send_to_service(y)@j) ==> x = y)  & (All x y #i #j. (Recv_AR(x)@i & Recv_AR(y)@j)  ==> x = y & #i = #j)  & (All #i #j. (Recv_TR()@i & Recv_TR()@j)  ==> #i = #j)\"

The above lemma checks whether there is a trace from the client registration to the start session passing all rules associated with the following:

1. The client sends a registration request to the blockchain. 2. The blockchain receives the registration request, verifies the signature, ensures that the token received is unique, and returns the _did_ and token inclusion proof. 3. The client generates an authentication request to be sent to the service after deriving a new token and proving its computation. 4. The service receives the authentication request, verifies that the token is created with the respective counter and secret key, verifies whether the _did_ corresponds to its did inclusion proof, and sends a token request to the blockchain. 5. The blockchain receives the token request and verifies it, after which the service establishes a session with the client. We provide a Tamarin model that has 128 lines of code. The model was computed automatically on a desktop machine with 8 CPUs of the type Intel(R) Core (TM) i7-8550U at1.80 GHz, with 16 GB for RAM, running Ubuntu 20.04.2 LTS. The runtime for our model was 3.716 s, and the code is available at [43]. In Appendix A, we also provide a UC modeling of our DID authentication protocol. ### Privacy with Token Unlinkability

Our protocol achieves auditability while providing the privacy property defined as _token unlinkability_ between (_did_, _token_) and (_service provider_, _token_). To formulate token unlinkability, we should depend on a typical indistinguishability game that an adversary plays with a challenger. However, to facilitate our token unlinkability analysis, we analyze it through the following three informal anonymity sets. _Anonymity client set \(\mathbb{S}_{\mathbb{C}}\)._ A client \(C_{0}\) with a registered _did\({}_{0}\)_ is anonymous with respect to logging a token \(tkn_{0}\) onto the blockchain if and only if \(C_{0}\) is anonymous within a set of clients \(\{C_{1},C_{2},\cdots,C_{n}\}\) defined as the \(\mathbb{S}_{\mathbb{C}}\) anonymity set. _Anonymity service set \(\mathbb{S}_{\mathbb{S}}\)._ A service provider \(S_{0}\) is anonymous with respect to logging tokens to the blockchain on behalf of the clients in the set \(\mathbb{S}_{\mathbb{C}}\) if and only if \(S_{0}\) is anonymous within a set of service providers \(\{S_{1},S_{2},\cdots,S_{n}\}\) defined as the \(\mathbb{S}_{\mathbb{S}}\) service anonymity set. _Anonymity token set \(\mathbb{S}_{\mathbb{BC}}\)._ A token \(tkn_{0}\) on the blockchain is anonymous if and only if \(tkn_{0}\) is indistinguishable from other tokens \(\{tkn_{1},tkn_{2},\cdots,tkn_{n}\}\) within a set defined as the \(\mathbb{S}_{\mathbb{BC}}\) token anonymity set. The privacy guarantee of our protocol depends on the size of the anonymity set. If there is only a single client \(C_{0}\in\mathbb{S}_{\mathbb{C}}\) and one token \(tkn_{0}\in\mathbb{S}_{\mathbb{BC}}\), then a union set \(\mathbb{S}_{\mathbb{C}}\cup\mathbb{S}_{\mathbb{BC}}\) with a set size of, at most, \(n^{2}\) compromises privacy with the probability \(1/n^{2}+negl(\lambda)\). This is similar in the case of service providers.