-
Notifications
You must be signed in to change notification settings - Fork 3
/
unlinkability.pv
95 lines (65 loc) · 2.4 KB
/
unlinkability.pv
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
free c:channel.
type AttestationPublicKey.
type AttestationPrivatekey.
type nonce.
type pkey.
type skey.
type host.
type key.
type RP_id.
(*For Digital Signatures *)
fun spk(skey):pkey.
fun sign(bitstring, skey):bitstring.
reduc forall x:bitstring, y:skey; getmess(sign(x, y)) = x.
reduc forall x:bitstring, y:skey; checksign(sign(x, y), spk(y)) = x.
(*For nonces*)
fun nonce_to_bitstring ( nonce ) : bitstring [ data , typeConverter ] .
table nonceTable(nonce) .
(*For Digital signature over Attestation Credentials*)
fun spkAtt(AttestationPrivatekey):AttestationPublicKey.
fun signAtt(bitstring, AttestationPrivatekey):bitstring.
reduc forall x:bitstring, y:AttestationPrivatekey; getmessAtt(signAtt(x, y)) = x.
reduc forall x:bitstring, y:AttestationPrivatekey; checksignAtt(signAtt(x, y), spkAtt(y)) = x.
(*Symetric encryption*)
fun senc(bitstring, key): bitstring.
reduc forall x: bitstring, k: key; sdec(senc(x,k),k) = x.
(*User's ID and Server's ID*)
const cert:bitstring [private].
const a:RP_id [private].
const credentialID2:bitstring [private].
(*Table*)
table tableAtt(AttestationPublicKey).
(*Events and Queries*)
event reachSameKey(AttestationPublicKey).
query N1:AttestationPublicKey; event(reachSameKey(N1)).
free attskU: AttestationPrivatekey[private].
query attacker(attskU).
free attpkU: AttestationPublicKey[private].
query attacker(attpkU).
const k:key.
let processUser ( k: key,cert:bitstring, attskA: AttestationPrivatekey, attpkA:AttestationPublicKey) =
(*Registration*)
in(c,s:bitstring);
let(challengeU:nonce, aU:RP_id)= sdec(s,k) in
new skU:skey;
let pkU = spk(skU) in
out(c,senc(signAtt((pkU, attpkU, cert,challengeU), attskU),k))
.
let processServer (k: key, a:RP_id) =
(*Registration*)
new challenge:nonce;
new attpkU3: AttestationPublicKey;
let ver1=(challenge,a) in
out(c, senc((challenge,a),k));
in(c, s:bitstring);
let m= sdec(s,k) in
let (pkY1: pkey, attpkU1:AttestationPublicKey, cert: bitstring, Nt:nonce) = getmessAtt(m) in
let ver = checksignAtt(m, attpkU1) in
get tableAtt(= attpkU1) in event reachSameKey(attpkU1)
else insert tableAtt(attpkU1).
process
new attskU:AttestationPrivatekey;
let attpkU = spkAtt(attskU) in
(
!processUser( k, cert, attskU,attpkU) | !processServer(k, a)
)