PROTOCOL:
SIMPLE

 

PURPOSE:

The Session Initiation Protocol (SIP) for Instant Messaging and Presence (MP)

 

REFERENCE:

 

MODELER:

Judson Santiago, LORIA Nancy, June 2005

 

ALICE_BOB: 

  WR --> PS: SUBSCRIBE
  PS --> WR: Challenge.realm (a nonce and id of the user domain)
  WR --> PS: Hash(Username.Challenge.Password)
  PS --> WR: PresenceInfo


  WR = Watcher
  PS = Presence Server

 

LIMITATIONS:

The protocol has two more agents, besides WR and PS, that do not appear in the specification, namely PT (Presentity) and RM (Rule Maker). The Presentity is the agent about whom the watcher wants to obtain informations. The Rule Maker is the agent that will provide a policy document to the Presence Server, stating the watchers that can obtain the presence information and under what conditions. Both agents were abstracted, the policy document is considered to be already known by the Presence Server because the document is transported using security mechanisms that prevents eavesdropping and interception of the message. We also assume that all watchers want to gather informations about the same Presentity and that they have the rights to do so.

The presence server has two ways to obtain the identity of the watcher, either the watcher authenticates himself in a local proxy, that can assert the watcher identity, and the proxy forwards the subscribe message to the presence server, or the watcher authenticates directly with the presence server. In the former case the local proxy will add a P-Asserted-identity field to the message that is forwarded to the presence server. This field can then be used to get the watcher identity and decide if the presence information should or not be granted to the watcher. The latter case, the one that is specified here, is a simpler view of the protocol that consider the presence server can authenticate the watcher identity.

The current specification uses common digest authentication and that implies no replay attack protection.

 

PROBLEMS:
3

 

CLASSIFICATION:
G1 G2 G12

 

ATTACKS:
None

 

NOTES:

The main concern with the PresenceInfo is its confidentialidy and that its receiver, the Watcher, is authenticated. Here we also analyse the agreement on (and even the freshness of) the PresenceInfo. wr_ps_info checks these properties, and the authentication of PS happens as a by-product.

The use of transport or network layer hop-by-hop security mechanisms, such as TLS or IPSec with apropriate cipher suites, should be used to prevent eavesdropping and interception of the final message containing the presence info. Here the message is encrypted with a symmetric key scheme.

A further simplification made to the protocol was the use of the Watcher name as the user name. In the SIP protocol a user can choose a username, via the P-prefered-identity field, under which he wants to be authenticated, but that feature do not add any extra security concerns.

 


HLPSL: 


role watcher (WR, PS   : agent,
              Password : text, 
              K        : symmetric_key,
              Hash     : hash_func,
              Realm    : text,
              Snd, Rcv : channel(dy)) played_by WR def=

  local State        : nat,
        Challenge,
        PresenceInfo : text

  init State := 0

  transition

   0.    State  = 0 /\ Rcv(start) =|>
         State':= 2 /\ Snd(subscribe)


   2.    State  = 2 /\ Rcv(Challenge'.Realm) =|>   
         State':= 4 /\ Snd(Hash(WR.Challenge'.Password))
                    /\ witness(WR,PS,ps_wr_user,WR.Password)

   4.    State  = 4 /\ Rcv({WR.PresenceInfo'}_K) =|>
         State':= 6 /\ wrequest(WR,PS,wr_ps_presenceinfo,PresenceInfo') 

end role




role pserver (PS       : agent,
              UserMap  : (agent.text.symmetric_key) set,
              Hash     : hash_func,
              Realm    : text,
              Snd, Rcv : channel(dy)) played_by PS def=


  local WR           : agent,
        State        : nat,
        Challenge,
        Password,
        PresenceInfo : text,
        K            : symmetric_key

  init State := 1

  transition


   1.    State  = 1 /\ Rcv(subscribe) =|> 
         State':= 3 /\ Challenge' := new()  
                    /\ Snd(Challenge'.Realm) 

   3.    State  = 3 /\ Rcv(Hash(WR'.Challenge.Password'))
                    /\ in(WR'.Password'.K', UserMap) =|>
         State':= 5 /\ PresenceInfo' := new() 
                    /\ Snd({WR'.PresenceInfo'}_K')
                    /\ secret(PresenceInfo',presenceinfo,{WR',PS})
                    /\ witness(PS,WR',wr_ps_presenceinfo,PresenceInfo')
                    /\ wrequest(PS,WR',ps_wr_user,WR'.Password')
      
end role




role session (PS       : agent,
              WR       : agent,
              K        : symmetric_key,
              Password : text,
              Realm    : text,
              H        : hash_func,
              UserMap  : (agent.text.symmetric_key) set,
              Snd,Rcv  : channel (dy)) def=

  composition
    watcher(WR,PS,Password,K,H,Realm,Snd,Rcv) /\
    pserver(PS,UserMap,H,Realm,Snd,Rcv)


end role




role environment () def=

 local UserMap: (agent.text.symmetric_key) set,
       Snd, Rcv : channel (dy)

 const wr1,wr2,ps   : agent,
       k1,k2,ki     : symmetric_key,
       h            : hash_func,
       subscribe    : text,
       pass1,pass2,
       passi,domain : text,
       presenceinfo,
       wr_ps_presenceinfo,
       ps_wr_user   : protocol_id
 
 init
       UserMap := {(wr1.pass1.k1),(wr2.pass2.k2),(i.passi.ki)} 

 intruder_knowledge = {wr1,wr2,ps,ki,passi,h,subscribe}

 composition

          session(ps,wr1,k1,pass1,domain,h,UserMap,Snd,Rcv)
       /\ session(ps,wr1,k1,pass1,domain,h,UserMap,Snd,Rcv)
       /\ session(ps,wr2,k2,pass2,domain,h,UserMap,Snd,Rcv)
       /\ session(ps,i  ,ki,passi,domain,h,UserMap,Snd,Rcv)

end role




goal

   % Confidentiality (G12)
   secrecy_of presenceinfo

   % Message authentication (G2)
   weak_authentication_on wr_ps_presenceinfo 
    
   % Entity authentication (G1)
   weak_authentication_on ps_wr_user  

end goal




environment()