PROTOCOL:
S/Key One-Time Password System

PURPOSE:

Mechanism for providing replay protection, authentication and secrecy by generating a sequence of one-time passwords.

 

REFERENCE:

 

MODELER:

 

ALICE_BOB:

Given:
 - 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

 

LIMITATIONS:

 

PROBLEMS:
1
 

ATTACKS:
None

 

NOTES:

The protocol consists of two agents: a client and a server. The client computes a secret based on a seed (supplied by the server) and his own password, i.e. Secret = MD4(Passwd.Seed). For a given Nmax, the client further computes a sequence of Nmax one-time passwords OTP(1),..., OTP(Nmax) by repeatedly applying the hash function to this secret (see above). Initially, the server is given the first one-time password OTP(1) and stores it as the current OTP. In following protocol steps, whenever the client is asked to authenticate himself to the server, he sends the next unused OTP. The server checks the validity of the received OTP by applying MD4 and comparing the result with the previously sent OTP - these must coincide! Thereafter, the server stores the obtained OTP as the current one.

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.  



HLPSL:


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()