-
Notifications
You must be signed in to change notification settings - Fork 0
/
dp-3t-bak5.pv
143 lines (121 loc) · 5.23 KB
/
dp-3t-bak5.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
(*
Protocol: DP-3T
Modeler: Bachir Bendrissou
Sources:
[S] https://blog.symbolic.software/2020/04/05/dp-3t-verifpal/
[OS] https://github.com/DP-3T/documents
[OS-l] ...
Footnote:
[1] We model each day as a phase, ex: phase 0 for day 0.
[2] We model the extreme case where everyone exchange EphIDs with everyone every day.
If the protocol is secure in this special case, than it must be secure in all other cases.
*)
free c:channel.
free c_ab:channel [private]. (* private channel for Alice and Bob *)
free c_ac:channel [private]. (* private channel for Alice and Charlie *)
free c_bc:channel [private]. (* private channel for Bob and Charlie *)
free c_bs:channel [private]. (* Backend Server and the Healthcare Authority share a secure connection *)
free c_a:channel.
free c_b:channel.
free c_c:channel.
free BroadcastKey: bitstring.
type skey.
(* We declare 1 tables to store exchanged ephemeral values. *)
table eph_values(bitstring, bitstring).
fun hmac(skey,bitstring, bitstring):bitstring. (* hmac/2 a function to derive ephemeral value from the secret key of the sender and the identity of the receiver *)
fun h(skey):skey. (* h/1, a hash function to derive a new secret key from yesterday's secret key *)
(* symmetric crypto *)
fun senc(skey,bitstring):bitstring. (* enc/2 *)
reduc forall k:skey, m:bitstring; sdec(k,senc(k,m)) = m.
(* AEAD: Authenticated Encryption with Associated Data *)
(* Encryption scheme *)
fun encrypt(skey, skey, bitstring): bitstring.
reduc forall x:skey, k:skey, r:bitstring; decrypt(encrypt(x,k,r),k,r) = x.
(* Function for generating Ephs from private keys*)
fun eph_key(bitstring):skey [private]. (* eph/1 *)
(* Function for generating Ephs from private keys*)
fun get_id(skey):bitstring. (* id/1 *)
reduc forall k:skey; get_key(get_id(k)) = k [private].
(* pairs *)
(* c) Model pairs with constructor pair/2 and destructors fst and snd. *)
fun pair(bitstring,bitstring):bitstring. (* pair/2 *)
reduc forall m1:bitstring,m2:bitstring; fst(pair(m1,m2))=m1.
reduc forall m1:bitstring,m2:bitstring; snd(pair(m1,m2))=m2.
fun RequestToken():bitstring. (* A constant *)
(* events *)
event Here().
event Ok().
event ProFinished(). (* Event when the protocol has finished all phases *)
event ProStep(). (* Some event at some point *)
event InfectionSent().
event Notification().
(* queries query attacker(C). query event(Infected(C)).
*)
query event(Here()).
query event(InfectionSent()).
query event(Notification()).
(* Process for Ephs-exchange initializer *)
let ini_exch(sender: bitstring, receiver: bitstring, senderkey: skey, pc:channel) =
let ephv = hmac(senderkey, receiver, BroadcastKey) in
out(pc, pair(sender, ephv));
in(pc, xeph:bitstring);
let senderx = fst(xeph) in
let eph = snd(xeph) in
insert eph_values(eph, senderx).
(* Process for Ephs-exchange responder*)
let resp_exch(c:channel, receiver: bitstring, receiverkey: skey) =
in(c, xeph:bitstring);
let sender = fst(xeph) in
let eph = snd(xeph) in
let x = hmac(receiverkey, sender, BroadcastKey) in
out(c, pair(sender, x));
insert eph_values(eph, receiver).
(* Report infection *)
let report_inf(sender: bitstring, senderKey: skey) =
out(c, RequestToken());
in(c_bc, encToken:bitstring);
let token = sdec(eph_key(sender), encToken) in
let msg = encrypt(senderKey, eph_key(sender), token) in
out(c, msg); event InfectionSent().
let healthCareAuthority(person: bitstring) =
in(c, xr:bitstring);
if xr = RequestToken() then
new token:bitstring;
out(c_bs, senc(eph_key(person), token));
out(c_bc, senc(eph_key(person), token)).
let backendServer(person: bitstring) =
in(c_bs, encToken:bitstring); (* Receive encrypted token from healthCareAuthority via private channel *)
in(c, y:bitstring);
let x = sdec(eph_key(person), encToken) in
let ym = decrypt(y, eph_key(person), x) in
out(c_a, ym); out(c_b, ym); out(c_c, ym); event Here(). (* Send out infectedPatients1 *)
let getNotified(k: skey, c:channel) =
in(c, y:skey);
if h(k) <> y then (* If the person infected is not me. *)
get eph_values(=hmac(y, get_id(k), BroadcastKey), =get_id(k)) in event Notification().
process
! new skA : skey ; new skB : skey ; new skC : skey ; (* Private keys for Alice, Bob, and Charlie *)
let A = get_id(skA) in
let B = get_id(skB) in
let C = get_id(skC) in
out(c, A) | out(c, B) | out(c, C) |
( ini_exch(A, B, skA, c_ab) | resp_exch(c_ab, B, skB) |
ini_exch(A, C, skA, c_ac) | resp_exch(c_ac, C, skC) |
ini_exch(B, C, skB, c_bc) | resp_exch(c_bc, C, skC) |
phase 1; let skA1 = h(skA) in
let skB1 = h(skB) in
let skC1 = h(skC) in
ini_exch(A, B, skA1, c_ab) | resp_exch(c_ab, B, skB1) |
ini_exch(A, C, skA1, c_ac) | resp_exch(c_ac, C, skC1) |
ini_exch(B, C, skB1, c_bc) | resp_exch(c_bc, C, skC1) |
phase 2; let skA2 = h(skA1) in
let skB2 = h(skB1) in
let skC2 = h(skC1) in
ini_exch(A, B, skA2, c_ab) | resp_exch(c_ab, B, skB2) |
ini_exch(A, C, skA2, c_ac) | resp_exch(c_ac, C, skC2) |
ini_exch(B, C, skB2, c_bc) | resp_exch(c_bc, C, skC2) |
phase 3; in(c, person:bitstring);
(if person = B || person = C || person = A then report_inf(person, h(get_key(person))) | healthCareAuthority(person) | backendServer(person)) |
getNotified(skA, c_a) | getNotified(skB, c_b) | getNotified(skC, c_c) | phase 4
)
(* etc. *)