# Decentralized Identity Authentication with Auditability and Privacy
## 5 Privacy-Preserving Protocol
### Final Protocol
#### 5.2.1 New Token and Its Consistency
In the next rule, as stated, we demonstrate how the blockchain verifies the signature on the public inputs (included in \(p\)) from the client and checks whether the token that it received from the client is not registered with the blockchain using the received action facts:

rule Blockchain_receive:

[!Pk($A, pkA), In(<p, sig>),!Token($A, tkn), !Did($A, did)]  --[Recv_RR($A)],

Eq(verify(sig, p, pkA), true), Unique(token) ]->

[!Did($A, did),!Betadid(did),!Betatkn(tkn)]

Here, \(Eq\) and \(Unique\) are called restrictions such that, to execute the premises, all of the respective variables should satisfy the specified restrictions. \(Eq\) is an equality restriction denoted by \(Eq(x,y)\), which means that \(x=y\), while \(Unique\) is a unique restriction denoted by \(Unique(x)\), which means that \(x\) can only be executed once. If the signature verification is successful and the token is unique, then it outputs the \(did\) that belongs to the client and the corresponding inclusion proofs as facts.

After the registration step, we define rules for the client to authenticate with a specific service, which involves generating a new token and its corresponding computational integrity proof (which is the zkSNARK proof). As premises, we take the previous token, gamma (token proof), betatoken (token inclusion proof), fresh variable \(w\) as the witness, and the setup phase proving key. Then, we check whether both the token and gamma share the same counter and secret key, as well as whether the betatoken corresponds to the token. Finally, we return a new token and gamma with its counter increased by 1 and the computational integrity proof denoted as \(Phi\).

rule Generate_tkn:

[!Token($A, tkn),!Gamma($A, gam),!Betatchn(betatoken), Fr(~w),!Ltk($Z, ltkz) ]

--[ Eq(g1(gam), t1(tkn)),  Eq(g2(gam), t2(tkn)),  Eq(betatoken, tkn) ]->

[!Token($A, pk(~ltkA))]

rule Register_did:

[!Pk($0A, gamma(g1(gam)+'1', g2(gam))),  Phi($A, pk(~ltkA))]

rule Register_did:

[!Pk($1A, ltkA) ] -->

[ Ltk2($A, pk(~ltkA))]

rule Register_did:

[!Pk($2A, sign(pk(~ltkB), ltkA)) ]

The ephemeral key helps to protect the client against a reply attack; hence, it plays an important role. Once we have the ephemeral key, we define the next rule, _Auth_req_, to model the authentication request that is initiated by the client and then sent to the service. rule Auth_req:

let tknreq = <<proof, tkn>, sign(<proof,tkn>, ltkB), pkB>

in [Phi($A, pk(~ltkA))]

rule Register_did:

[!Pk($3A, tkn), Ltk2($A, pk(~ltkA))]

rule Register_did:

[!Pk($4A, pkB),!Did($A, pk(~ltkA))]

rule Register_did:

[!Pk($5A, gam) ] --[ Send_to_service($A, pk(~ltkA))]

rule Register_did:

[!Pk($6A, pkA))]--[ Recv_AR($A, pk(~ltkA))]

rule Register_did:

[!Pk($7Z, pkz)

--[ Recv_TR(),  Eq(vrfy(proof, tkn, pkz), true), Unique(tkn) ]-->

[!Betatkn(tkn) ]

The _betatoken_ is defined with a persistent fact!_Betatkn_. In the final step, we model the _Return_to_service_ rule, which models how the service verifies the inclusion proof received from the blockchain and establishes a session with the client. rule return_to_service:

[!Token($A, pk(~ltkA))]

rule Register_did:

[!Pk($8A) ]

The rule takes a token and betatoken as premises, checks whether the betatoken corresponds to the token, and then initiates the session. ### Security Property

An attacker cannot login to an honest service by using an identity on the blockchain without being detected. The client will be able to detect its credentials being misused at an honest service through active surveillance of the blockchain or its subsequent authentication events. An honest service or blockchain is an entity that is not controlled by the attacker. We formalize it as follows. **Definition 1**.