PROTOCOL:
APOP: Authenticated Post Office Protocol

PURPOSE:

Secure mechanism for origin authentication and replay protection.

 

REFERENCE:

 

MODELER:

 

ALICE_BOB: 

 S -> C : Hello.Timestamp
 C -> S : C.MD5(Timestamp.K_CS)
 S -> C : Success

 

PROBLEMS:
1
 

ATTACKS:
None

 

NOTES:

The following protocol models part of the POP3 Post Office Protocol. POP3 is used to allow a workstation (client) to retrieve mail that a server is holding for it. After the POP3 server has sent a greeting, the session enters the AUTHORISATION state in which the client has to identify itself to the server. After successful identification the session enters the TRANSACTION state and the client may request actions from the server, e.g. for delivering mail. When the client issues the QUIT command, the session enters the UPDATE state, i.e. the server releases acquired resources and says goodbye. The modelled part of the POP3 protocol covers the greeting and the AUTHORISATION phase. There are several ways for server identification one of which is the APOP method which provides origin authentication and replay protection: The APOP method assumes server and client to share a common secret K_CS. The POP3 server includes a fresh timestamp in its greeting message. The client answers with his identity and a digest calculated by applying the MD5 algorithm to the timestamp followed by the shared secret. On successful verification of the digest, the server issues a positive response and the session enters the TRANSACTION state.  

HLPSL: 


role client(
    C,S            : agent,
    K_CS           : symmetric_key,
    MD5            : hash_func,
    Hello, Success : text,
    SND,RCV        : channel(dy))
played_by C def=

  local
    State     : nat,
    Timestamp : text

  const
    timestamp : protocol_id
                   
  init 
    State := 0
            
  transition
            
 1. State   = 0 /\ RCV(Hello.Timestamp') =|>
    State' := 1 /\ SND(C.MD5(Timestamp'.K_CS))
                /\ witness(C,S,timestamp,Timestamp')

 2. State   = 1 /\ RCV(Success) =|>
    State' := 2 
                              
end role




role server (
    C,S            : agent,
    K_CS           : symmetric_key,
    MD5            : hash_func,
    Hello, Success : text,
    SND,RCV        : channel(dy))
played_by S def=
            
  local
    State     : nat,
    Timestamp : text

  const
    timestamp : protocol_id
                   
  init 
    State := 10
            
  transition
            
 1. State   = 10 /\ RCV(start) =|>
    State' := 11 /\ Timestamp' := new()
                 /\ SND(Hello.Timestamp')
                   
 2. State   = 11 /\ RCV(C.MD5(Timestamp.K_CS)) =|>
    State' := 12 /\ SND(Success)
                 /\ request(S,C,timestamp,Timestamp)
end role




role session (
    C,S            : agent,
    K_CS           : symmetric_key,
    MD5            : hash_func,
    Hello, Success : text)
def=

  local
    S1, S2: channel (dy),
    R1, R2: channel (dy)
              
  composition
              
    client(C,S,K_CS,MD5,Hello,Success,S1,R1)
 /\ server(C,S,K_CS,MD5,Hello,Success,S2,R2)

end role




role environment() def=

  const 
    c,s           : agent,
    md5           : hash_func,
    k_cs,k_is     : symmetric_key,
    hello,success : text

  intruder_knowledge = {c,s,i,k_is,md5,hello,success}

  composition

    session(c,s,k_cs,md5,hello,success)
 /\ session(c,s,k_cs,md5,hello,success)
 /\ session(i,s,k_is,md5,hello,success)
 /\ session(i,s,k_is,md5,hello,success)
           
end role
                  



goal
  %Server authenticates Client on timestamp
  authentication_on timestamp
end goal




environment()