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:

 

MODELER:

 

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:

 

PROBLEMS:
3
 

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