-
Notifications
You must be signed in to change notification settings - Fork 3
/
LiKe_test_1.pv
159 lines (125 loc) · 5.29 KB
/
LiKe_test_1.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
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
(*Pietro Tedeschi - Hamad Bin Khalifa University - LiKe protocol (pietrotedeschi dot me at gmail dot com)*)
(*Dolev-Yao model Open Channels*)
free cak:channel. (*Channel between DeviceA and DomAuth*)
free cbk:channel. (*Channel between DeviceB and DomAuth*)
free cab:channel. (*Channel between DeviceA and DeviceB*)
(*Constants and Variables*)
const IDA:bitstring. (*ID of DeviceA*)
const IDB:bitstring. (*ID of DeviceB*)
const TsA:bitstring. (*Timestamp of DeviceA*)
const TsB:bitstring. (*Timestamp of DeviceB*)
type nonce. (*Random nonce generated by the user*)
type sharedKey. (*Shared Secret*)
type plk. (*PreLink Key*)
type lk. (*Link Key*)
free G:bitstring. (*Generator point of the Elliptic Curve*)
free xA:bitstring[private]. (*First partial private Key---generated from the DeviceA*)
free rA:bitstring[private]. (*Second partial private Key---generated from the DomAuth for the DeviceA*)
free xB:bitstring[private]. (*First partial private Key---generated from the DeviceB*)
free rB:bitstring[private]. (*Second partial private Key---generated from the DomAuth for the DeviceB*)
free pA:bitstring[private].
free pB:bitstring[private].
(*Auxiliary Functions*)
fun hash(bitstring):bitstring.
fun append(bitstring,bitstring):bitstring.
fun add(bitstring,bitstring):bitstring.
fun mul(bitstring,bitstring):bitstring.
fun kdf(sharedKey):plk.
fun hmac(plk,bitstring):bitstring.
fun get_shared_key(bitstring,bitstring):sharedKey.
fun get_link_key(bitstring,nonce,nonce):lk.
(*Events*)
event endADomAuth(bitstring,bitstring).
event endBDomAuth(bitstring,bitstring).
event beginDomAuthA(bitstring,bitstring).
event beginDomAuthB(bitstring,bitstring).
event begin_LiKe_B(bitstring,bitstring,bitstring,bitstring,nonce).
event begin_LiKe_A(bitstring,bitstring,bitstring,bitstring,nonce).
event end_LiKe_A(lk). (*A ends the protocol with B*)
event end_LiKe_B(lk). (*B ends the protocol with A*)
(*Attack Model*)
query attacker(xA).
query attacker(xB).
query attacker(pA).
query attacker(pB).
(*Test the Authenticity Phase with the KGC
query u:bitstring,v:bitstring; event(endADomAuth(u,v)) ==> event(beginDomAuthA(u,v)).
query u:bitstring,v:bitstring; event(endBDomAuth(u,v)) ==> event(beginDomAuthB(u,v)).*)
(*A authenticates B*)
query x:lk, u:bitstring, v:bitstring, y:bitstring, w:bitstring, n:nonce; inj-event(end_LiKe_B(x))==>inj-event(begin_LiKe_A(u,v,y,w,n)).
(*B authenticates A*)
query x:lk, u:bitstring, v:bitstring, y:bitstring, w:bitstring, n:nonce; inj-event(end_LiKe_A(x))==>inj-event(begin_LiKe_B(u,v,y,w,n)).
(*Process userA*)
let DeviceA(Cpub:bitstring) =
let PvA = mul(xA,G) in
out(cak,(IDA,TsA,PvA));
in(cak,(XPA:bitstring,XpA:bitstring));
let ZA = add(XPA,mul(hash(append(IDA,append(TsA,append(PvA,XPA)))),Cpub)) in
let ZAP = mul(XpA,G) in
if ZA = ZAP then
event endADomAuth(XpA,PvA);
(*Key Generation Phase of DeviceA*)
new nA:nonce;
out(cab,(IDA,TsA,PvA,XPA,nA));
in(cab,(IDXB:bitstring,TsXB:bitstring, XPvB:bitstring, XXPB:bitstring, nXB:nonce));
(*A believes it started the protocol with B*)
event begin_LiKe_B(IDXB,TsXB,XPvB,XXPB,nXB);
if IDXB = IDB then
let KAB1 = mul(XpA,add(XXPB,mul(hash(append(IDXB,append(TsXB,append(XPvB,XXPB)))),Cpub))) in
let KAB2 = mul(xA,XPvB) in
let skAB = kdf(get_shared_key(KAB1,KAB2)) in
let sigmA = hmac(skAB,(IDA,TsA,PvA,XPA,IDXB,TsXB,XPvB,XXPB,nA,nXB)) in
out(cab,sigmA);
in(cab,sigmBX:bitstring);
let sigmBV = hmac(skAB,(IDXB,TsXB,XPvB,XXPB,IDA,TsA,PvA,XPA,nXB,nA)) in
if sigmBX = sigmBV then
let lkAB = get_link_key(append(KAB1,KAB2),nA,nXB) in
(*Compute Link Key*)
event end_LiKe_A(lkAB).
(*Process userB*)
let DeviceB(Cpub:bitstring) =
let PvB = mul(xB,G) in
out(cbk,(IDB,TsB,PvB));
in(cbk,(XPB:bitstring,XpB:bitstring));
let ZB = add(XPB,mul(hash(append(IDB,append(TsB,append(PvB,XPB)))),Cpub)) in
let ZBP = mul(XpB,G) in
if ZB = ZBP then
event endBDomAuth(XpB,PvB);
(*Key Generation Phase of DeviceB*)
in(cab,(IDXA:bitstring,TsXA:bitstring, XPvA:bitstring, XXPA:bitstring, nXA:nonce));
(*B believes it started the protocol with A*)
event begin_LiKe_A(IDXA,TsXA,XPvA,XXPA,nXA);
if IDXA = IDA then
let KBA1 = mul(XpB,add(XXPA,mul(hash(append(IDXA,append(TsXA,append(XPvA,XXPA)))),Cpub))) in
let KBA2 = mul(xB,XPvA) in
let skBA = kdf(get_shared_key(KBA1,KBA2)) in
new nB:nonce;
out(cab,(IDB,TsB,PvB,XPB,nB));
in(cab,sigmAX:bitstring);
let sigmAV = hmac(skBA,(IDXA,TsXA,XPvA,XXPA,IDB,TsB,PvB,XPB,nXA,nB)) in
if sigmAX = sigmAV then
let sigmB = hmac(skBA,(IDB,TsB,PvB,XPB,IDXA,TsXA,XPvA,XXPA,nB,nXA)) in
out(cab,sigmB);
let lkBA = get_link_key(append(KBA1,KBA2),nXA,nB) in
(*Compute Link Key*)
event end_LiKe_B(lkBA).
(*Process DomAuth*)
let DomAuth(c:bitstring, Cpub:bitstring) =
in(cak,(IDX:bitstring,TsX:bitstring,PvXA:bitstring));
if IDX = IDA then
let PA = mul(rA,G) in
let pA = add(rA,mul(hash(append(IDX,append(TsX,append(PvXA,PA)))),c)) in
event beginDomAuthA(pA,PvXA);
out(cak,(PA,pA));
in(cbk,(IDXB:bitstring,tXB:bitstring,PvXB:bitstring));
if IDXB = IDB then
let PB = mul(rB,G) in
let pB = add(rB,mul(hash(append(IDXB,append(tXB,append(PvXB,PB)))),c)) in
event beginDomAuthB(pB,PvXB);
out(cbk,(PB,pB)).
process
new c:bitstring;
let Cpub = mul(c,G) in (*Domain Authority Public Key*)
out(cak,Cpub);
out(cbk,Cpub);
(!DeviceA(Cpub))|(DomAuth(c,Cpub))|(!DeviceB(Cpub))