VARIANT:

With TLS method

PURPOSE:

Mutual authentication, key establishment,
replay protection, confidentiality. EAP-TLS [10] is based on TLS as a mechanism designed for providing authentication and encryption scheme over TCP transport. The EAP-TLS method is developed to use the concept of TLS handshake over EAP.

REFERENCE:

http://www.ietf.org/rfc/rfc2716.txt

MODELER:

Jing Zhang for Siemens CT IC 3, 2004
Peter Warkentin, Siemens CT IC 3
Vishal Sankhla, University of Southern California, 2004

ALICE_BOB:

Let S/Ks/Ns denote id/public-key/nonce respectively of the server. Similarly, P/Kp/Np for the Peer. Furthermore, let Kca denote the public key of a certification authority. Then set

Client_hello : Vers.SessionID.Np.CipherSuite Server_hello : Vers.SessionID.Ns.Cipher Client_certificate : {P.Kp}_inv(Kca) Server_certificate : {S.Ks}_inv(Kca) Server_key_exchange : Client_key_exchange : {PMS}_Ks with pre-master-secret PMS (nonce of P) Client_certificate_verify : {H(Np.Ns.S.PMS)}_inv(Kp) Change_cipher_spec : text Server_hello_done : text Finished : encrypted hash of all previous messages with master secret PRF(PMS,Np,Ns)

S -> P: request_id P -> S: respond_id.UserId S -> P: start_tls P -> S: Client_hello S -> P: Server_hello, Server_certificate, Server_key_exchange, Server_certificate_request, % only if authentication of P required Server_hello_done P -> S: Client_certificate, % only if authentication of P required Client_key_exchange, Client_certificate_verify, % only if authentication of P required Change_cipher_spec, Finished S -> P: Change_cipher_spec, Finished

LIMITATIONS:

The server S combines the (logically) different roles of the network access server NAS and the EAP server.
no modelling of session-resumption
only public key encryption in TLS

PROBLEMS:

secrecy of sec_clientK, sec_serverK
strong authentication on nps1
strong authentication on nps2

ATTACKS:

None

NOTES:

This protocol sets up the communication between two agents, in the following called Peer and Server. It is used to authenticate the Server and (optionally) the Peer. Furthermore, a set of keys is established for future encryption and data integrity. Initially, in client_hello and server_hello, the Peer and Server exchange and agree on versions-numbers, cipher-suites, session-ids. Furthermore, they exchange nonces Np, Nc which are used later on for key generation. The Server sends a certificate to the Peer for authentication. The Server may (optionally) ask the Peer to authenticate himself. On receipt of the Server's message, the Peer checks the Server's certificate and (if asked) sends his own certificate together with verify-data to the Server. The Peer generates a new secret PMS and sends it (encrypted) to the Server. Based on Np, Ns, PMS both parties are now able to compute the new session keys. They both close the protocol by sending a final message "Finished" encrypted with the new keys.

HLPSL:


role peer (P, S           : agent,
           H, KeyGen      : hash_func,
           PRF            : hash_func,
           Kp, Kca        : public_key,
           SND_S, RCV_S   : channel (dy))
played_by P def=

  local  Np, Csus, PMS                  : text,
         SeID                           : text,
         Ns, TNo, Csu, Sh, Rcert        : text,
         Sc, Ske, Cke, Cv, Shd, Ccs     : text,
         State                          : nat,
         Finished : hash(hash(text.text.text).agent.agent.text.text.text),
         ClientK, ServerK : hash(agent.text.text.hash(text.text.text)),
         Ks                             : public_key,
         Nps                            : text.text

  const sec_clientK,
        sec_serverK,
        nps1, nps2 : protocol_id,
        sid0       : text,  % session id = 0
        request_id : text,
        respond_id : text,
        start_tls  : text

  init State := 0

  transition

  0. State  = 0 /\ RCV_S(request_id) =|>
     State':= 2 /\ SND_S(respond_id.P)
        
  2. State  = 2 /\ RCV_S(start_tls) =|>
     State':= 4 /\ Np'   := new()
                /\ Csus' := new()
                /\ TNo'  := new()
                /\ SND_S( TNo'.sid0.Np'.Csus' )    % client hello (SeID=0)

  % with client authentication
  41. State = 4 /\ RCV_S(
                TNo.SeID'.Ns'.Csu'.         % server hello
                {S.Ks'}_inv(Kca).           % server certificate
                Ske'.                       % server key exchange
                Rcert'.                     % server certificate request
                Shd')                       % server hello done
     =|>
      State':= 6
       /\ PMS'      := new()
       /\ Ccs'      := new()
       /\ Finished' := H(PRF(PMS'.Np.Ns').P.S.Np.Csu'.SeID')
       /\ ClientK'  := KeyGen(P.Np.Ns'.PRF(PMS'.Np.Ns'))
       /\ ServerK'  := KeyGen(S.Np.Ns'.PRF(PMS'.Np.Ns'))
       /\ SND_S({P.Kp}_inv(Kca).            % client certificate
                {PMS'}_Ks'.                 % client key exchange
                {H(Np.Ns'.S.PMS')}_inv(Kp). % client certificate verify
                Ccs'.                       % change cipher spec
                {Finished'}_ClientK')       % finished
       /\ witness(P,S,nps2,Np.Ns')

  % without client authentication
  42. State = 4 /\ RCV_S(
                TNo.SeID'.Ns'.Csu'.         % server hello
                {S.Ks'}_inv(Kca).           % server certificate
                Ske'.                       % server key exchange
                Shd')                       % server hello done
     =|>
      State':= 6
       /\ PMS'      := new()
       /\ Ccs'      := new()
       /\ Finished' := H(PRF(PMS'.Np.Ns').P.S.Np.Csu'.SeID')
       /\ ClientK'  := KeyGen(P.Np.Ns'.PRF(PMS'.Np.Ns'))
       /\ ServerK'  := KeyGen(S.Np.Ns'.PRF(PMS'.Np.Ns'))
       /\ SND_S({PMS'}_Ks'.                 % client key exchange
               %{H(Ns'.S.PMS')}_inv(Kp).    % client certificate verify
                Ccs'.                       % change cipher spec
                {Finished'}_ClientK')       % finished
       /\ witness(P,S,nps2,Np.Ns')

  6. State  = 6 /\ RCV_S(Ccs.{Finished}_ServerK) =|>
     State':= 8 /\ secret(ClientK,sec_clientK,{P,S})
                /\ secret(ServerK,sec_serverK,{P,S})
                /\ request(P,S,nps1,Np.Ns)

end role



role server (P, S           : agent,
             H, KeyGen      : hash_func,
             PRF            : hash_func,
             Ks, Kca        : public_key,
             SND_P, RCV_P   : channel (dy))
played_by S def=

  local  Ns, SeID                        : text,
         PMS                             : text,
         Np, Csus, TNo, Csu, Sh, Sc, Ske : text,
         Cke, Cv, Ccs, Rcert,Shd         : text,
         State                           : nat,
         Finished : hash(hash(text.text.text).agent.agent.text.text.text),
         ClientK, ServerK : hash(agent.text.text.hash(text.text.text)),
         Kp                              : public_key

  const nps1, nps2 : protocol_id,
        sid0       : text,  % session id = 0
        request_id : text,
        respond_id : text,
        start_tls  : text

  init State := 1

  transition

  1. State  = 1 /\ RCV_P(start) =|>
     State':= 3 /\ SND_P(request_id)


  3. State  = 3 /\ RCV_P(respond_id.P) =|>
     State':= 5 /\ SND_P(start_tls)

  % with client authentication
  51. State  = 5 /\ RCV_P(TNo'.sid0.Np'.Csus')     % client hello
     =|>
      State':= 7
       /\ Ns'   := new()
       /\ SeID' := new()
       /\ Shd'  := new()
       /\ Rcert'  := new()
       /\ Ske'  := new()
       /\ Csu'  := new()
       /\ SND_P(TNo'.SeID'.Ns'.Csu'.         % server hello  
                {S.Ks}_inv(Kca).             % server certificate
                Ske'.                        % server key exchange
                Rcert'.                      % server certificate request
                Shd')                        % server hello done
       /\ witness(S,P,nps1,Np'.Ns')  

  % without client authentication
  52. State  = 5
       /\ RCV_P(TNo'.sid0.Np'.Csus')         % client hello
     =|>
      State':= 9
       /\ SeID'  := new()
       /\ Ns'  := new()
       /\ Ske'  := new()
       /\ Shd'  := new()
       /\ Csu'  := new()
       /\ SND_P(TNo'.SeID'.Ns'.Csu'.         % server hello
                {S.Ks}_inv(Kca).             % server certificate       
                Ske'.                        % server key exchange
                Shd')                        % server hello done
       /\ witness(S,P,nps1,Np'.Ns') 


  % with client authentication
  7. State  = 7
       /\ RCV_P({P.Kp'}_inv(Kca).            % client certificate
                {PMS'}_Ks.                   % client key exchange
                {H(Np.Ns.S.PMS')}_inv(Kp').  % client certificate verify
                Ccs'.                        % change cipher spec
                {Finished'}_ClientK'         % finished
               ) 
       /\ Finished' = H(PRF(PMS'.Np.Ns).P.S.Np.Csu.SeID) 
       /\ ClientK'  = KeyGen(P.Np.Ns.PRF(PMS'.Np.Ns)) 
     =|>
     State' := 11
       /\ ServerK'  := KeyGen(S.Np.Ns.PRF(PMS'.Np.Ns)) 
       /\ SND_P(Ccs'.{Finished'}_ServerK')
       /\ request(S,P,nps2,Np.Ns) 

  % without client authentication
  9. State  = 9
       /\ RCV_P({PMS'}_Ks.                   % client key exchange 
                %{H(Ns.S.PMS')}_inv(Kp).     % client certificate verify
                Ccs'.                        % change cipher spec
                {Finished'}_ClientK'         % finished
               ) 
       /\ Finished' = H(PRF(PMS'.Np.Ns).P.S.Np.Csu.SeID) 
       /\ ClientK'  = KeyGen(P.Np.Ns.PRF(PMS'.Np.Ns)) 
     =|>
     State' := 11
       /\ ServerK'  := KeyGen(S.Np.Ns.PRF(PMS'.Np.Ns)) 
       /\ SND_P(Ccs'.{Finished'}_ServerK')
      %/\ request(S,P,nps2,Np.Ns) 








end role



role session(P, S           : agent,
             Kp, Ks, Kca    : public_key,
             H, KeyGen      : hash_func,
             PRF            : hash_func)
def=

  local SP, SS, RP, RS : channel (dy)

  composition
           peer(  P,S,H,KeyGen,PRF,Kp,Kca,SP,RP)
        /\ server(P,S,H,KeyGen,PRF,Ks,Kca,SS,RS)

end role




role environment()
def=

   const p,s             : agent,
         kp, ks, ki, kca : public_key,
         h, keygen       : hash_func,
         prf             : hash_func

   intruder_knowledge = {p,s, h,keygen,prf, kp,ks,kca,ki,inv(ki),

                         {i.ki}_inv(kca)     
                        }

   composition
        session(p,s,kp,ks,kca,h,keygen,prf)
%   /\  session(p,i,kp,ki,kca,h,keygen,prf)
    /\  session(i,s,ki,ks,kca,h,keygen,prf)

end role



goal

        %secrecy_of ClientK, ServerK
        secrecy_of sec_clientK, sec_serverK

        %Peer authenticates Server on nps1
        authentication_on nps1
        %Server authenticates Peer on nps2
        authentication_on nps2

end goal



environment()