VARIANT:
pseudonyms for Location Recicpient and Target

REFERENCE:

 

PURPOSE:

Obtain geographical location information restricted by a privacy policy.
Using pseudonyms for both the location recipient and the target,
to protect their anonymity against the location server.  

MODELER:

 

ALICE_BOB:

 T  : Target (subsumes Location Generator, Mobile User and Rule Maker)
 LR : Location Recipient
 LS : Location Server (subsumes Rule Holder)
 LI : Location Information
 PR : Privacy Rule
 1. LR ---- LR.{LR.K_LR.N_LR}_K_T_LR ---------------------------------> T
 2. LR <- {Psi_LR.Psi_T.N_LR}_K_T_LR ---------------------------------- T
 3.                              LS <- {Psi_LR.Psi_T.PR.LI.K_LR}_K_LS - T
 % some time later, LR requests the location information of T:
 4. LR -- {Psi_LR.Psi_T}_K_LS -> LS
 5. LR <- {PR(LI).Psi_T}_K_LR -- LS
 

PROBLEMS:
4
 

CLASSIFICATION:
G1, G2, G3, G12, G20
 

ATTACKS:
None
 

NOTES:

This version of Geopriv is different from the normal one in the sense that the real identity of the Target should not be known by the Location Server. The Location Server just knows the pseudonyms of the Location Recipient and of the Target. Unfortunately, this implies that LS cannot authenticate the Target. To compensate this, K_LR is sent by LR already in its first message to the Target and forwarded to LS in the third message. Still, LS cannot check the authenticity and integrity of the Privacy Rule.

A further (minor) difference is that we model the Location Generator as part of the Target and transmit in the third message both the pseudonyms and the location of the Target because the Location Server cannot associate these values since he is not allowed to know the identity of the Target.

 



HLPSL:

role locationRecipient(
        T, LR, LS       : agent,            
        K_T_LR          : symmetric_key,
        K_LS            : public_key,
        Snd, Rcv        : channel(dy)) played_by LR def=

local
        State           : nat, 
        N_LR            : text,
        Psi_LR          : text,
        Psi_T           : text,
        K_LR            : symmetric_key, % could also be: public_key 
        Filtered_LI     : message 

init State := 0

transition

        0. State  = 0 /\ Rcv(start) 
       =|> State':= 2 /\ N_LR' := new() 
                      /\ K_LR' := new()
                      /\ secret(K_LR' , k_LR, {T, LR, LS})
                      /\ Snd(LR.{LR.K_LR'.N_LR'}_K_T_LR)
                      /\ witness(LR, T, t_LR_LR, LR)    
        
        2. State  = 2 /\ Rcv({Psi_LR'.Psi_T'.N_LR}_K_T_LR)      
       =|> State':= 8 /\ Snd({Psi_LR'.Psi_T'}_K_LS) 
                      /\ witness(LR, LS, ls_LR_K_LR, K_LR)
                      /\ request(LR, T , lr_T_N_LR, N_LR)
        
        8. State  = 8 /\ Rcv({Filtered_LI'.Psi_T}_K_LR) 
       =|> State':= 10/\ request(LR, T, lr_T_filtered_LI, Filtered_LI') 

end role 


role target( T, LS : agent, K_T_LR : symmetric_key, % should be determined by a lookup K_LS : public_key, Snd_LR, Snd_LS, Rcv: channel(dy)) played_by T def= local State : nat, LR : agent, N_LR : text, K_LR : symmetric_key, % could also be: public_key Psi_LR : text, Psi_T : text, LI : text, PR : hash_func init State := 1 transition 1. State = 1 /\ Rcv(LR'.{LR'.K_LR'.N_LR'}_K_T_LR) =|> State':= 3 /\ Psi_LR' := new() /\ Psi_T' := new() /\ Snd_LR({Psi_LR'.Psi_T'.N_LR'}_K_T_LR) /\ witness (T, LR', lr_T_N_LR, N_LR') /\ wrequest(T, LR', t_LR_LR, LR') /\ PR' := new() % chooses some privacy (accuracy) rule /\ LI' := new() /\ secret(LI', li, {T, LS}) /\ secret((PR'.LI'), filtered_LI, {T, LR', LS}) /\ Snd_LS({Psi_LR'.Psi_T'.PR'.LI'.K_LR'}_K_LS) /\ witness (T, LR', lr_T_filtered_LI, (PR'.LI')) end role
role locationServer( T, LR, % but LS does not actually use identity of T and LR LS : agent, K_LS : public_key, Psi_Table: (text.text.hash_func.text.symmetric_key) set, Snd, Rcv : channel(dy)) played_by LS def= local State : nat, Psi_LR : text, Psi_T : text, K_LR : symmetric_key, LI : text, PR : hash_func init State := 5 transition 5. State = 5 /\ Rcv({Psi_LR'.Psi_T'.PR'.LI'.K_LR'}_K_LS) =|> State':= 7 /\ Psi_Table':= cons(Psi_LR'.Psi_T'.PR'.LI'.K_LR', Psi_Table) 7. State = 7 /\ Rcv({Psi_LR'.Psi_T'}_K_LS) /\ in(Psi_LR'.Psi_T'.PR'.LI'.K_LR', Psi_Table) % uses the information Psi_LR and Psi_T to look up PR, LI and K_LR in the table. =|> State':= 9 /\ Snd({(PR'.LI').Psi_T'}_K_LR') /\ wrequest(LS, LR, ls_LR_K_LR, K_LR') end role
role session(T, LR, LS : agent, K_T_LR : symmetric_key, K_LS : public_key, Psi_Table : (text.text.hash_func.text.symmetric_key) set) def= local SLR, RLR, STLR, STLS, RT, SLS, RLS: channel(dy) composition locationRecipient(T, LR, LS, K_T_LR, K_LS, SLR, RLR) /\ target (T, LS, K_T_LR, K_LS, STLR, STLS, RT) /\ locationServer (T, LR, LS, K_LS, Psi_Table, SLS, RLS) end role
role environment() def= local Psi_Table: (text.text.hash_func.text.symmetric_key) set % shared between all instances of LS const psi_LR, li, filtered_LI, lr_T_N_LR, k_LR, t_LR_LR, lr_LS_filtered_LI : protocol_id, t, lr, ls : agent, k_LS : public_key, k_T_LR, k_T_i, k_i_LR : symmetric_key init Psi_Table := {} intruder_knowledge = {t, lr, ls, k_LS, k_T_i, k_i_LR} composition session(t, lr, ls, k_T_LR, k_LS, Psi_Table) /\ session(t, lr, ls, k_T_LR, k_LS, Psi_Table) % repeat session to check for replay attacks % /\ session(i, lr, ls, k_i_LR, k_LS, Psi_Table) % It does not make much sense to let the intruder play the role of T % since then the intruder would know its location information anyway. % /\ session(t, i, ls, k_T_i, k_LS, Psi_Table) % It does not make sense to let the intruder play the role of LR % since then the intruder is allowed to know the (secret) location of T. end role
goal secrecy_of li, filtered_LI, k_LR % addresses G12 % strong authentication and integrity of the Location Information, % (including replay protection): authentication_on lr_T_filtered_LI % addresses G2 and G3 % the Location Server (weakly) authenticates the Location Recipient: % weak_authentication_on ls_LR_K_LR % addresses G2 and G3 % additional authentication goals, not in RFC3693: authentication_on lr_T_N_LR % addresses G1 and G3 weak_authentication_on t_LR_LR % addresses G1 % and G20: T authorizes LR to receive the location via LS end goal
environment()