%UAC -> SS: register (the info is called Nu)
%SS -> UAC: ok (the content is called Ns)

%After TLS established, 
%using the symmetric key scheme for a security protocol Kus

%UAC -> P: INVITE (kus)
%P -> UAS: INVITE (ksu)
%UAS -> P: OK (ksu)
%P -> UAC: OK (kus)
%UAC -> UAS: ACK (kuu)
%UAC -> UAS: BYE (kuu)
%UAS -> UAC: OK  (kuu)



%HLPSL:

    role uac (UAC, SS, UAS: agent,             
              Kus,Kuu: symmetric_key,      
              UAC_SS, SS_UAC, UAC_UAS, UAS_UAC: channel (dy)) 
    
    played_by UAC def=

      local State : nat, 
            Ni, No, Na: text
	%Ni: invite content
	%No: ok content : need contain the message said what media it willing to establish connection
	%Na: ack content

      init State := 0

      transition  
        %Send invite and its invite content
	%This content must be secure, and can be used for authenticated
        1.  State  = 0 /\ SS_UAC(start) =|> 
            State':= 1 /\ Ni' := new() /\ UAC_SS({sipinvite.UAC.UAS.Ni'}_Kus)
                       /\ secret(Ni',ni,{UAC,UAS}) 
                       /\ witness(UAC,UAS,uas_uac_ni,Ni')	
	
	%Receive okay with SDP content for negotiation
	%This content must be secure and can be used for authenticated
	%To simply, we assume it finishes in this step and send ack
        2.  State  = 1 /\ SS_UAC({sipok.UAS.UAC.No'}_Kus) =|> 
            State':= 2 /\  Na' := new() /\ UAC_UAS({UAC.UAS.Na'}_Kuu) 
                       /\ request(UAC,UAS,uac_uas_no,No')
	
	%Receive bye (no content) from Bob and send ok (no content)
	3.  State  = 2 /\ UAS_UAC({sipbye.UAS.UAC}_Kuu) =|> 
            State':= 3 /\ UAC_UAS({sipok.UAC.UAS}_Kuu) 

    end role

    role ss(UAC, SS, UAS: agent,      
             Kus,Ksu: symmetric_key,      
             SS_UAC, UAC_SS, SS_UAS, UAS_SS: channel (dy)) 
    
    played_by SS def=

      local State : nat, 
            Ni, No: text

      init State := 1

      transition 

	%Recv from Alice and forward to Bob, attach its address
        4.  State  = 1 /\ UAC_SS({sipinvite.UAC.UAS.Ni'}_Kus) =|> 
            State':= 2 /\ SS_UAS({sipinvite.UAC.UAS.SS.Ni'}_Ksu)

        5.  State  = 2 /\ UAS_SS({sipok.UAS.UAC.SS.No'}_Ksu) =|> 
            State':= 3 /\ SS_UAC({sipok.UAS.UAC.No'}_Kus)

    end role


    role uas (UAC, SS, UAS: agent,             
              Ksu,Kuu: symmetric_key,      
              UAS_SS, SS_UAS, UAC_UAS, UAS_UAC: channel (dy)) 
    
    played_by UAS def=

      local State : nat, 
            Ni, No, Na: text

      init State := 0

      transition  
        %Recv invite and send okay
	%This content must be secure, and can be used for authenticated
        6.  State  = 0 /\ SS_UAS({sipinvite.UAC.UAS.SS.Ni'}_Ksu) =|> 
            State':= 1 /\ No' := new() /\ UAS_SS({sipok.UAS.UAC.SS.No'}_Ksu)
                       /\ secret(No',no,{UAC,UAS}) 
                       /\ witness(UAC,UAS,uac_uas_no,No')	
		       /\ request(UAS,UAC,uas_uac_ni,Ni')
	%We could remove the authenticate above
	
        7.  State  = 1 /\  UAC_UAS({UAC.UAS.Na'}_Kuu) =|> 
            State':= 2 /\  UAS_UAC({sipbye.UAS.UAC}_Kuu) 
	
	%We might not need to do Rec ok but right now just doing junk
	8.  State  = 2 /\ UAC_UAS({sipok.UAC.UAS}_Kuu) =|> 
            State':= 3 /\ secret(No',no,{UAC,UAS})

    end role

    role session(A, S, B: agent, Kus, Ksu, Kuu: symmetric_key) def=

      local SAS, RAS, SAB, RAB,
	    SSA, RSA, SSB, RSB,
	    SBS, RBS, SBA, RBA : channel (dy)

      composition 

            uac(A,S,B,Kus,Kuu,SAS,RAS,SAB,RAB)
         /\ ss (A,S,B,Kus,Ksu,SSA,RSA,SSB,RSB)
	 /\ uas(A,S,B,Ksu,Kuu,SBS,RBS,SBA,RBA)

    end role



    role environment() def=

        const uac, ss,uas    : agent,
              kus, ksu, kuu, kis, ksi,kiu,kui : symmetric_key,
              sipinvite, sipok, sipack, sipbye,
	      ni, no,
              uac_uas_no, uas_uac_ni : protocol_id

        intruder_knowledge = {uac, ss, uas, kis, ksi,kiu,kui, sipinvite, sipok, sipack, sipbye}

        composition

            session(uac,ss,uas,kus,ksu,kuu)
	   /\ session(i,ss,uas,kis,ksu,kiu)
	   /\ session(uac,ss,i,kus,kis,kui)
	   /\ session(uac,i,uas,kui,kiu,kuu)
	
	%If we remove this an intruder session(uac,i,uas,kui,kiu,kuu)
	%Then it would be safe

    end role



    goal

      %We need to see if the ni, no secrecy is violated or not
      secrecy_of ni, no
	
    end goal



    environment()