-
Notifications
You must be signed in to change notification settings - Fork 0
/
safkhani.spdl
109 lines (63 loc) · 1.78 KB
/
safkhani.spdl
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
const XOR: Function;
secret k; // shared
usertype Timestamp;
macro M1 = XOR(Tij,Nt);
macro M2 = {(Tij, Sij, Nt)}k;
macro Tijp1 = {Tij}k;
macro Sijp1 = {Sij}Tijp1;
macro M4 = {Sijp1}XOR(Nt,Nr);
protocol fan(tag, reader, cloud) {
role tag {
fresh Nt: Nonce;
fresh Tij: Timestamp;
secret Sij;
fresh Nr: Nonce;
recv_1(reader, tag, Nr);
send_2(tag, reader, {(Tij)}k, M1, M2);
claim(tag, Secret, {(Tij)}k);
claim(tag, Secret, M1);
claim(tag, Secret, M2);
recv_7(reader,tag, M4);
claim(tag, Secret, M4);
};
role reader {
fresh Nr: Nonce;
send_1(reader, tag, Nr);
var Tij: Timestamp;
var Nt: Nonce;
secret Sij;
recv_2(tag, reader, {(Tij)}k, M1, M2);
claim(reader, Secret, {(Tij)}k);
claim(reader, Secret, M1);
claim(reader, Secret, M2);
send_3(reader, cloud, {Tij}k);
claim(reader, Secret, {Tij}k);
var Nc: Nonce;
recv_4(cloud, reader, {Sij}Tij, Nc);
claim(reader, Secret, {Sij}Tij);
send_5(reader, cloud, {{Tij}k}Nc, {Tijp1}k, {Sijp1}Tijp1);
claim(reader, Secret, {{Tij}k}Nc);
claim(reader, Secret, {Tijp1}k);
claim(reader, Secret, {Sijp1}Tijp1);
recv_6(cloud, reader, cloud);
send_7(reader,tag, M4);
claim(reader, Secret, M4);
};
role cloud {
// lookup
var Tij: Timestamp;
recv_3(reader, cloud, {Tij}k);
claim(cloud, Secret, {Tij}k);
fresh Nc: Nonce;
secret Sij;
send_4(cloud, reader, {Sij}Tij, Nc);
claim(cloud, Secret, {Sij}Tij);
var Tijp1: Timestamp;
secret Sijp1;
recv_5(reader, cloud, {{Tij}k}Nc, {Tijp1}k, {Sijp1}Tijp1);
claim(cloud, Secret, {{Tij}k}Nc);
claim(cloud, Secret, {Tijp1}k);
claim(cloud, Secret, {Sijp1}Tijp1);
send_6(cloud, reader, cloud);
};
};