PROTOCOL:

HIP: Host Identity Protocol

PURPOSE:

4-way hand-shake protocol that provides mobility enhanced with security, in particular authentication and authorisation.

REFERENCE:

MODELER:

Murugaraj Shanmugam for Siemens CT IC 3, January 2005
David von Oheimb, Siemens CT IC 3, January 2005

ALICE_BOB:

S chooses HIP_Trans and PUZZLE

 0. C -> S: Hash(HI_S).Hash(HI_C)
 1. S -> C: {PUZZLE.HI_S.DH_S.HIP_Trans.ESP_Trans}_Sig(S)
 2. C -> S: {Soln.LSI_C.SPI_C.HIP_Trans.ESP_Trans.DH_C.{HI_C}_key}_Sig(C)
 3. S -> C: {LSI_S.SPI_S.HMAC}_Sig(S)

where
HI -- Host Identity/Public key
DH -- Diffie-Hellman
HIP_Trans -- Algorithms for HIP key Generation
ESP_Trans -- Algorithms for ESP key Generation
Soln -- function to solve puzzle
key -- generated using the HIP_Trans and DH
SPI -- Security Parameter Index Value
LSI -- Local Index Value
HMAC -- one of the hash chains derived from DH

LIMITATIONS:

We assume that there is a Certificate Authority for verifying the certificates.
Generation of hash chains to protect the further Base Exchange is not shown in the model.
The key for hashing cannot be specified directly; we gave it as an extra field to Hash.
Since HLPSL does not support arithmetic, we are unable to use the counter mechanism on puzzles, which prevents the replay attack. We incorporated the puzzle and the counter mechanism into a single fresh PUZZLE variable.

PROBLEMS:

secrecy of hash_dh
strong authentication on initiator_responder_hash_dh

CLASSIFICATION:

G1, G3, G9, G10

ATTACKS:

None

NOTES:

This protocol does not guarantee client authentication for the server, because there is no DNS lookup for the responder to verify the identity of the claimer.

Since the Certificate packet follows the I2 Packet, we just combined I2 and Certificate into a single packet. This does not pose a new attack, except for potential Denial of Service attacks, which we do not consider (yet).

HLPSL:


role initiator (
        J,R     : agent,        % Initiator and Responder
        SND,RCV : channel(dy),  % Send, Receive Channel
        Hash    : hash_func,    % Hash Function
        Soln    : hash_func,    % Solution 
        HI_I,HI_R:public_key,   % Public key of the Initiator and Responder
        G:nat)                  % Diffie Hellman's public G value
        played_by J def=

        local 
        State   : nat,
        X       : text,         % Initiator's Diffie Hellman Value
        SPI_I   : text,         % Initiator's Security Parameter Index Value
        LSI_I   : text,         % Initiator's Local Scope Index Value
        SPI_R   : text,         % Responder's Security Parameter Index Value
        LSI_R   : text,         % Responder's Local Scope Index Value
        PUZZLE  : text,         % Puzzle
        HIP_Trans:text,         % HIP Transform sent by the Responder
        ESP_Trans:text,         % ESP Transform of the Responder
        EGY     : message,      % Responder's Diffie Hellman Value
        R2      : hash(message) % R2 Packet
                                
        const
        hit_r     : text,       % HIT of the Responder (Hash of HI_R)
        cert      : text,       % Certificate Packet
        choose    : hash_func
                                   
        init State := 0
                
transition
                
 0.     State = 0 /\ RCV (start)=|>
                  State':= 1 /\ SND (Hash(HI_R).Hash(HI_I))
        
 1.     State = 1 /\ RCV((PUZZLE'.HI_R.EGY'.HIP_Trans'.ESP_Trans').
                    {Hash(PUZZLE'.HI_R.EGY'.HIP_Trans'.ESP_Trans')
                    }_inv(HI_R)) =|>
        State':= 3 /\ X':=new() /\ SPI_I':=new()
                  /\ R2':=Hash(exp(EGY',X'))
                  /\ SND(Soln(PUZZLE').SPI_I'.LSI_I.choose(HIP_Trans').
                              choose(ESP_Trans').exp(G,X').{HI_I}_R2'.
                        {Hash(Soln(PUZZLE').SPI_I'.LSI_I.choose(HIP_Trans').
                              choose(ESP_Trans').exp(G,X').{HI_I}_R2')
                        }_inv(HI_I).
                         cert.{Hash(cert)}_inv(HI_I))
                  
3.      State = 3 /\ RCV(Hash(SPI_R'.LSI_R'.Hash(R2))
                            .{SPI_R'.LSI_R'.Hash(R2)}_inv(HI_R)) =|>
        State':=5 /\ request(J,R,initiator_responder_hash_dh,R2) 
                  /\ secret(Hash(exp(EGY,X)),hash_dh,{J,R})
            
end role     
            

            
role responder (
                J,R     :agent,         % Initiator and Responder
                SND,RCV :channel(dy),   % Send, Receive Channel
                Hash    :hash_func,     % Hash Function
                Soln    :hash_func,     % Solution 
                HI_R    :public_key,    % Public key of the Responder
                G:nat)                  % Diffie Hellman's public G value
        played_by R def=

        local 
        State:nat,
        Y       :text,          % Responder's Diffie Hellman parameter
        SPI_R   :text,          % Responder's Security Parameter Index Value
        LSI_R   :text,          % Responder's Local Scope Index Value
        SPI_I   :text,          % Initiator's Security Parameter Index Value
        LSI_I   :text,          % Initiator's Local Scope Index Value
        Puzzle  :text,          % Responder's Puzzle
        HI_I    :public_key,    % Public key of the Initiator
        Hj_I    :hash(public_key),      % Hash (Public key)  of the Initiator
        Chosen_HIP_Trans :hash(text),   % chosen HIP Transform
        Chosen_ESP_Trans :hash(text),   % chosen HIP Transform
        I1      :text,          % I1 Packet
        CERT    :text,          % Certificate Packet
        EGX     :message,       % Initiator's Diffie-Hellman value
        R2      :hash(message)  % R2 Packet
                        
        const
        hIP_Trans : text,  % HIP Transform of the Responder
        eSP_Trans : text   % HIP Transform of the Responder
                  
        init State := 2
                
        transition

2.       State = 2 /\ RCV (Hash(HI_R).Hj_I') =|>
         State':=4 /\ Y':=new() /\ Puzzle':=new() /\
                      SND ((Puzzle'.HI_R.exp(G,Y').hIP_Trans.eSP_Trans).
                     {Hash((Puzzle'.HI_R.exp(G,Y').hIP_Trans.eSP_Trans))
                     }_inv(HI_R))
        
4.       State = 4 /\ RCV((Soln(Puzzle).SPI_I'.LSI_I'.Chosen_HIP_Trans'.
                            Chosen_ESP_Trans'.EGX'.{HI_I'}_Hash(exp(EGX',Y))).
                     {Hash(Soln(Puzzle).SPI_I'.LSI_I'.Chosen_HIP_Trans'.
                            Chosen_ESP_Trans'.EGX'.{HI_I'}_Hash(exp(EGX',Y)))
                     }_inv(HI_I').
                        CERT'.{Hash(CERT')}_inv(HI_I'))
                   /\ (Hash(HI_I')= Hj_I) =|>
         State':=6 /\ R2':=Hash(exp(EGX',Y)) /\ SPI_R':=new()
                   /\ SND(Hash(SPI_R'.LSI_R.Hash(R2')).
                              {SPI_R'.LSI_R.Hash(R2')}_inv(HI_R))
                   /\ witness(R,J,initiator_responder_hash_dh,R2') 
            
end role                                   
            

           
role session (
        J,R      : agent,       % Initiator and Responder
        IR,RI    : channel(dy), % Send, Receive Channel
        Hash     : hash_func,   % Hash Function
        Soln     : hash_func,   % Solution 
        HI_I,HI_R: public_key,  % Public key of the Initiator,Responder
        G        :nat)          % Diffie Hellman's public G value
def=

       composition
                initiator(J,R,IR,RI,Hash,Soln,HI_I,HI_R,G)
             /\ responder(J,R,RI,IR,Hash,Soln,HI_R,G)

end role



role environment() def=
            
        local SND,RCV :channel(dy)

        const
          j,r     : agent,      % Initiator and Responder
          hash_   : hash_func,  % Hash Function
          soln_   : hash_func,  % Solution
          hi_j,hi_r:public_key, % Public key of the Initiator,Responder
          hi_i    :public_key,  % Public key of the intruder
          g       : nat,        % Diffie Hellman's public G value
          hash_dh, initiator_responder_hash_dh : protocol_id    % Protocol ID

        intruder_knowledge = {j,r,hash_,soln_,hi_j,hi_r,g,hi_i,inv(hi_i)}
        % in the first session, intruder should not solve puzzles.
              
        composition

        session(j,r,SND,RCV,hash_,soln_,hi_j,hi_r,g)
% /\    session(i,r,SND,RCV,hash_,soln_,hi_i,hi_r,g)
%       Adding this session yields a spurious authentication failure because
%       the client of the first session talks to the server of the second,
%       but in exactly the same way as he would do within the first session.
  /\    session(j,i,SND,RCV,hash_,soln_,hi_j,hi_i,g)     
              
end role 



goal
            
        secrecy_of hash_dh                            % addresses G9 and G10
        authentication_on initiator_responder_hash_dh % addresses G1 and G3
        
end goal



environment()