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