-
Notifications
You must be signed in to change notification settings - Fork 3
/
Authentication and key agreement phase
160 lines (153 loc) · 4.91 KB
/
Authentication and key agreement phase
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
%Role specification for the User
role role_U (U, GW, SN: agent,H:hash,SND, RCV: channel(dy))
played_by U
def=
local
State: nat,
% Here Q is denote the secret biometric key
PIDs,PSW,Kgu,Kgunew,TIDu,TIDunew,Q,IDu,IDs,IDg,Ts1,Ts4,SK,W:text
const sec_1,sec_2,sec_4,sec_5,sec_6,sec_7,sec_8,sec_9,auth_1,auth_4,auth_5,auth_6,auth_7:protocol_id
init
State := 0
Transition
%Login phase
1. State=0 /\RCV(start) =|> State':=1
/\Ts1':=new()/\IDs':=new()/\Q':=new()/\PSW':=new() /\IDu':=new()/\witness(U,GW,auth_1,Ts1')
/\witness(U,GW,auth_5,Kgu')
/\secret(Q',sec_1,{U})
/\secret(IDu',sec_4,{U})
/\secret(Kgu',sec_7,{U,GW})
/\secret(PSW', sec_8,{U})
/\Kgu':= H(IDu.IDg.H(Q.PSW.IDu).W)/\ TIDu':= H(IDu'.IDg.Kgu'.W)/\PIDs':=xor(IDs',H(Kgu'))
/\SND(TIDu'.PIDs'.H(IDu'.IDs'.Kgu'.H(Q'.PSW'.IDu').Ts1') .Ts1')
%Authentication and key agreement phase
4. State=1 /\RCV(Ts4'.xor(SK',Kgunew').H(SK'.H(TIDu.TIDunew'.Kgunew'.Ts4')))=|>State':=4
/\request(U,GW,auth_4,Ts4')
/\request(U,GW,auth_5,Kgu)
/\request(U,GW,auth_7,SK')
/\secret(IDu,sec_4,{U})
/\secret(Q',sec_1,{U})
/\secret(SK,sec_2,{GW,U,SN})
/\secret(Kgu,sec_7,{U,GW})
/\secret(Kgunew',sec_9,{U,GW})
end role
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Role specification for the Gateway
role role_GW (GW,U,SN:agent,H:hash,SND,RCV:channel(dy))
played_by GW
def=
local
State: nat,
PIDs,PSW,Kgu,Kgunew,TIDu,TIDunew,Kgs,IDg,W,Ts1,Ts2,Ts3,IDs,Ts4,SK,IDu, Q:text
const sec_1,sec_2,sec_3,sec_4,sec_5,sec_6,sec_7,sec_8,sec_9,auth_1,auth_2,auth_3,auth_7:protocol_id
init
State := 0
Transition
%Login phase
1. State=0/\RCV(TIDu'.PIDs'.H(IDu'.IDs'.Kgu'.H(Q'.PSW'.IDu).Ts1').Ts1') =|>State':=1
/\request(GW,U,auth_1,Ts1')
/\request(GW,U,auth_5,Kgu')
/\secret(Q',sec_1,{U})
/\secret(W',sec_6,{GW})
/\secret(IDg',sec_5,{GW})
/\secret(IDu',sec_4,{U})
/\secret(Kgu',sec_7,{U,GW})
/\secret(PSW',sec_8,{U})
/\Ts2':=new()/\ SK':=new()
/\witness(GW,SN,auth_2,Ts2')
/\witness(GW,SN,auth_6,Kgs)
/\witness(GW,SN,auth_7,SK')
/\secret(SK',sec_2,{GW,U,SN})
/\secret(Kgs,sec_3,{GW,SN})
/\SND(H(IDs'.Kgs).xor(SK',H(Kgs)).H(IDs'.Kgs.SK'.Ts2').Ts2')
%Receive the message from sensor node Sn
3. State=1 /\RCV(H(IDs.Kgs).Ts3'.H(SK'.IDs. H(Kgs.IDs.Ts3').Ts3')) =|> State':=3
/\request(GW,SN,auth_3,Ts3')
/\request(GW,SN,auth_6,Kgs)
/\secret(Kgs,sec_3,{GW,SN})
/\ secret(SK',sec_2,{GW,U,SN})
/\Ts4':=new()
/\witness(GW,U,auth_4,Ts4')
/\witness(GW,U,auth_5,Kgu)
/\witness(GW,U,auth_7,SK')
/\secret(IDu,sec_4,{U})
/\secret(Q',sec_1,{U})
/\secret(W,sec_6,{GW})
/\secret(IDg,sec_5,{GW})
/\secret(Kgu,sec_7,{U,GW})
/\secret(Kgunew',sec_9,{U,GW})
/\Kgunew':=(Kgu.H(Q'.PSW'.IDu).IDu.Ts4')
/\TIDunew':=H(TIDu.H(Kgu.H(Q'.PSW'.IDu).IDu.Ts4').Ts4')
/\SND(Ts4'.xor(SK',H(Kgunew')).H(SK'.H(TIDu.TIDunew'.Kgunew'.Ts4')))
end role
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Role specification for the Sensor node
role role_SN(SN,U,GW:agent,H:hash,SND,RCV:channel(dy))
played_by SN
def=
local
State: nat,
Kgs,IDs,Ts2,Ts3,SK:text
const sec_2,sec_3,auth_2,auth_3,auth_7:protocol_id
init
State := 1
Transition
% Authentication and key agreement phase
2. State=1
/\RCV(H(IDs'.Kgs).xor(SK',H(Kgs)).H(I Ds'.Kgs.SK'.Ts2').Ts2') =|>State':=2
/\ request(SN,GW,auth_2,Ts2')
/\request(SN,GW,auth_6,Kgs)
/\request(SN,GW,auth_7,SK')
/\secret(SK',sec_2,{GW,U,SN})
/\secret(Kgs,sec_3,{GW,SN})
/\Ts3':=new()
/\witness(SN,GW,auth_3,Ts3')
/\witness(SN,GW,auth_3,Kgs)
/\SND(H(IDs.Kgs).Ts3'.H(SK'.IDs.H(Kgs.IDs.Ts3').Ts3'))
end role
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Role specification for the Session
role session (SN,U,GW:agent,H:hash)
def=
local
SND3,RCV3,SND2,RCV2,SND1,RCV1:channel(dy)
composition
role_SN(SN,U,GW,H,SND3,RCV3)
/\role_GW(GW,U,SN,H,SND2,RCV2)
/\role_U(U,GW,SN,H,SND1,RCV1)
end role
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Role specification for the Goal and Environment
role environment()
def=
const
users,node,gateway:agent,sec_1,sec_2,sec_3,sec_4,sec_5,sec_6,auth_1,auth_2,auth_3,auth_4:protocol_id,
h:hash
intruder_knowledge = {users,gateway,node,h}
composition
session(node,users,gateway,h)
/\session(node,users,gateway,h)
/\session(node,users,gateway,h)
/\session(i,users,gateway,h)
/\ session(node,i,gateway,h)
/\session(node,users,i,h)
end role
goal
secrecy_of sec_1
secrecy_of sec_2
secrecy_of sec_3
secrecy_of sec_4
secrecy_of sec_5
secrecy_of sec_6
secrecy_of sec_7
secrecy_of sec_8
secrecy_of sec_9
authentication_on auth_1
authentication_on auth_2
authentication_on auth_3
authentication_on auth_4
authentication_on auth_5
authentication_on auth_6
authentication_on auth_7
end goal
environment()