-
Notifications
You must be signed in to change notification settings - Fork 3
/
Password and biometric change phase
93 lines (88 loc) · 2.65 KB
/
Password and biometric change 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
%Role specification for the User
role role_U (U,GW:agent,H:hash,SND,RCV:channel(dy))
played_by U
def=
local State: nat,
% Here Q is denote the secret biometric key
Q,Qnew,PSW,PSWnew,IDu,Kgu,Ts5,Ts6,TIDu,TIDunew,Rpswnew:text
const sec_1,sec_2,sec_3,sec_4,sec_5,sec_6,sec_7,auth_1,auth_2,auth_3:protocol_id
init
State := 0
transition
1. State=0/\RCV(start)=|>State':=1
/\Ts5':=new()
/\PSW':=new()
/\PSWnew':=new()
/\Q':=new()
/\Qnew':=new()
/\secret(IDu,sec_2,{U,GW})
/\secret(Kgu,sec_3,{U,GW})
/\secret(PSW',sec_4,{U,GW})
/\secret(PSWnew',sec_5,{U,GW})
/\secret(Q',sec_1,{U,GW})
/\secret(Qnew',sec_6,{U,GW})
/\secret(Rpswnew',sec_7,{U,GW})
/\Rpswnew':=H(Qnew'.PSWnew'.IDu)
/\witness(U,GW,auth_1,Ts5')
/\SND(TIDu'.xor(Rpswnew',H(Kgu)).Ts5'.H(IDu.Kgu.H(Q'.PSW'.IDu).Rpswnew'.Ts5'))
2. State=1
/\ RCV(Ts6'.H(TIDunew'.Rpswnew'.Ts6'))=|>State':=2
/\request(U,GW,auth_2,Ts6')
/\request(U,GW,auth_3,TIDunew')
end role
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Role specification for the Gateway
role role_GW(GW,U:agent,H:hash,SND,RCV:channel(dy))
played_by GW
def=
local State:nat,
Q,Qnew,IDu,Kgu,Kgunew,Ts5,PSW,PSWnew,TIDu,Ts6,TIDunew,Rpswnew:text
const auth_1,auth_2,auth_3:protocol_id
init
State := 0
transition
1. State=0/\RCV(TIDu'.xor(Rpswnew',H(Kgu)).Ts5'.H(IDu.Kgu.H(Q.PSW'.IDu).Rpswnew'.Ts5'))=|>State':=1
/\Ts6':=new()
/\request(GW,U,auth_1,Ts5')
/\witness(GW,U,auth_2,Ts6')
/\witness(GW,U,auth_3,TIDunew')
/\Kgunew':=H(Kgu.Rpswnew'.IDu.Ts6')
/\TIDunew':=H(TIDu.Kgunew'.Ts6')
/\SND(Ts6'.H(TIDunew'.Rpswnew'.Ts6'))
end role
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Role specification for the Session
role session(GW,U:agent,H:hash)
def=
local
SND2,RCV2,SND1,RCV1:channel(dy)
composition
role_GW(GW,U,H,SND2,RCV2)/\role_U(U,GW,H,SND1,RCV1)
end role
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Role specification for the Goal and Environment
role environment()
def=
const sec_1,sec_2,sec_3,sec_4,sec_5,sec_6,sec_7,auth_1,auth_2,auth_3:protocol_id,gateway,users:agent,
h:hash
intruder_knowledge ={users,gateway,h}
composition
session (gateway,users,h)
/\session (gateway,users,h)
/\session(gateway,users,h)
/\session(i,users,h)
/\session(gateway,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
authentication_on auth_1
authentication_on auth_2
authentication_on auth_3
end goal
environment()