- Passwd : password only known to client - Seed : a nonce supplied by server - MD4 : one-way hash function - Secret : secret generated by client (=MD4(Passwd.Seed)) - Nmax : maximal number of one-time passwords (here Nmax=6) - OTP(N) : N-th one-time password (N=1,2,..Nmax) obtained by applying MD4 (Nmax-N)-times to Secret, i.e. OTP(N) = MD4^(Nmax-N)(Secret). Initially, S knows OTP(1) = MD4^5(Secret) (here: Nmax = 6).C -> S : C S -> C : N.Seed % challenge of S to C for authentication: % C is asked to send N-th OTP (wrt Seed) % here: C is asked for next OTP C -> S : OTP(N) % S knows previous one-time password OTP(N-1) % and checks validity, i.e MD4(OTP(N)) = OTP(N-1) S -> C : Success
The server may ask for a the N-th OTP by supplying N in his challenge.
This cannot be easily modelled within the current framework.
role client( C,S : agent, MD4 : hash_func, Secret : message, SEED : text, SUCCESS : text, SND, RCV : channel(dy)) played_by C def= local State : nat, M : message const m : protocol_id init State := 0 transition 0. State = 0 /\ RCV(start) =|> State':= 1 /\ SND(C) 1. State = 1 /\ RCV(SEED) =|> State':= 2 /\ M' := MD4(MD4(MD4(MD4(Secret)))) /\ SND(M') /\ witness(C,S,m,M') 2. State = 2 /\ RCV(SUCCESS) =|> State':= 3 /\ SND(C) 3. State = 3 /\ RCV(SEED) =|> State':= 4 /\ M' := MD4(MD4(MD4(Secret))) /\ SND(M') /\ witness(C,S,m,M') 4. State = 4 /\ RCV(SUCCESS) =|> State':= 5 /\ SND(C) 5. State = 5 /\ RCV(SEED) =|> State':= 6 /\ M' := MD4(MD4(Secret)) /\ SND(M') /\ witness(C,S,m,M') 6. State = 6 /\ RCV(SUCCESS) =|> State':= 7 end role
role server( C,S : agent, MD4 : hash_func, OTP : message, SEED : text, SUCCESS : text, SND,RCV : channel(dy)) played_by S def= local State : nat, M : message const m : protocol_id init State := 10 transition 1. State = 10 /\ RCV(C) =|> State':= 11 /\ SND(SEED) 2. State = 11 /\ RCV(M') /\ OTP = MD4(M') =|> State':= 10 /\ OTP' := M' /\ SND(SUCCESS) /\ request(S,C,m,M') end role
role session ( C,S : agent, MD4 : hash_func, Passwd : text, SUCCESS : text, SEED : text) def= local OTP : message, Secret : message, S1, S2 : channel (dy), R1, R2 : channel (dy) init OTP := MD4(MD4(MD4(MD4(MD4(MD4(Passwd.SEED)))))) /\ Secret := MD4(Passwd.SEED) composition client(C,S,MD4,Secret,SEED,SUCCESS,S1,R1) /\ server(C,S,MD4,OTP, SEED,SUCCESS,S2,R2) end role
role environment() def= const c1,s1 : agent, c2,s2 : agent, md4 : hash_func, passwd1 : text, passwd2 : text, success : text, seed1 : text, seed2 : text intruder_knowledge = {c1,s1,c2,s2,md4,success, passwd2,seed2 } composition session(c1,s1,md4,passwd1,success,seed1) /\ session(i, s1,md4,passwd2,success,seed2) end role
goal %Server authenticates Client on m authentication_on m end goal
environment()