# Decentralized Identity Authentication with Auditability and Privacy
## 5 Privacy-Preserving Protocol
### Final Protocol
#### 5.2.1 New Token and Its Consistency
\(\$x\) denotes the public variable \(x\);
3. \(\#i\) denotes the timestamp \(i\);
4. \(!Fact\) denotes a persistent \(Fact\).

Here, the only difference between persistent facts (with the! prefix) and linear facts is that persistent facts are never removed from the state, while linear facts can be removed after executing some rules. Specifically, if there is a linear fact as a premise, but it does not appear as a conclusion, then it will be removed (consumed by the corresponding rule). To handle this, persistent facts are sometimes utilized.

Builtins, Functions, and Equations

In Tamarin, a function is an expression involving variables that maps some arguments to other arguments. We can define our functions or use builtin functions. However, an equation is a statement used to model the properties of a function. Equations can also be user-defined or extracted from builtin message theories.

In our Tamarin model for DID authentication, we use various builtins, such as, :

* Signing: This theory models the signature scheme. The function's symbols are \(sign/2\), \(verify/3\), \(pk/1\), and \(true\), which satisfy the equation \(verify(sign(m,sk),m,pk(sk))=true\).
* Hashing: This theory models a hash function. The function's symbol is \(h/1\), and there are no equations.
* Multiset: This theory introduces the associative-commutative operator \"+\", which is usually used to model multisets.

The custom functions with their respective equations are as follows:

* \(prove/3\) and \(vrfy/3\) with \(vrfy(prove(inp,w,sk),inp,pk(sk))=true\) helps to obtain the zero-knowledge proof and verify the proof.
* \(token/2\), \(gamma/2\), and \(vrfyVRF/4\) with \(vrfyVRF(x,token(x,sk),gamma(x,sk),pk(sk))=true\) help to obtain and verify the VRF output with the token and token proof (gamma).
* \(t1/1[private]\) and \(t2/1[private]\) with \(t1(token(a,b))=a,t2(token(a,b))=b\).
* \(g1/1[private]\) with \(g2/1[private]\) with \(g1(gamma(a,b))=a\), \(g2(gamma(a,b))=b\). Both t1 and g1 are getter functions. For example, given a pair of tokens, t1 takes the first element of the token.

### Privacy-Preserving DID Authentication Model in Tamarin

We modeled DID authentication in a standard way and explain the set of rules that we defined to verify the security properties.

We start with rules that help the clients to initialize their new identifiers and the authentication tokens corresponding to them:

rule Register_pk:

[ Fr(~ltkA) ] --> [!Ltk($A, ~ltkA),!Pk($A, pk(~ltkA))]

rule Register_did:

[!Pk($A, pkA)] --> [!Did($A, h(pkA))]

rule Register_tkn:

[!Ltk($A, ltkA)] -->

[!Token($A, token('0', ltkA)),!Gamma($A, gamma('0', ltkA))]

The _Register_tkn_ rule consists of the _Token_ fact, which ensures that token \(tkn\) and the token VRF proof _gamma_ belong to a specific client. Next, we have a registration request rule that is created by the client that uses it; it can register the initialized values to the blockchain:

rule Registration_request:

let p = <pkA, ~info, token('0', ltkA)>

in

[ Fr(~info),!Token($A, token('0', ltkA)),!Ltk($A, ltkA),!Pk($A, pkA) ] --[ Send_RR($A) ]->

[ Out(<p, sign(p, ltkA)>)]

Here, we take freshly generated information, a token fact, and both the secret key and public key as premises and output a public statement with its respective signature. This action will be called Send_RR, as stated in the rule.