VARIANT:
Pervasive access

REFERENCE:

Geographic Location Privacy Requirements: Pervasive Scenarios.
Talk by Jorge Cuellar at Pervasive 2002 in Zurich, http://www.pervasive2002.org/  

PURPOSE:
authorization for anonymous access (using a pseudonym of the target)

to location services in a spontaneous place through the Location Beacon Server  

MODELER:
Lan Liu for Siemens CT IC 3, May 2005
 

ALICE_BOB:

 T	: Target
 LoSi	: Location Sighter
 LBS	: Pervasive-Location Beacon Server (or P-LBS)
 1. T    --------------  {P1_T.Loc}_K_LoSi ----------------------> LoSi
 2. LoSi --------------- {P1_T.Loc}_K_LL ------------------------> LBS
 3. T    <---------- {LBS.N_LBS.Loc}_P1_T ------------------------ LBS
 4. T    ------- P1_T.Psi_T.K_T.Cert_Psi_T.N_LBS.
                {P1_T.Psi_T.K_T.Cert_Psi_T.N_LBS}_inv(K_T) ------> LBS
 %5. T   <----------------  {LBS}_K_T  ----------------------------LBS
 Cert_Psi_T = {Psi_T.Dom_T.K_T}_inv(K_CA)
 

PROBLEMS:
2
 

CLASSIFICATION:
G1, G3, G12
 

ATTACKS:
None
 

NOTES:

% We chose to use weak authentication for LoSi by T % because with strong authentication, there would be a replay attack. % An alternative fix for this attack could be that the % target sends its identity T to the LoSi and the % LBS, so the target can authenticate the LoSi on % Loc and T. Yet the target does not want to use its % real identity T for privacy reasons.

We model the authorization of the target by the LBS indirectly by checking the certificate of the target which binds the pseudonym of the target with its domain and its public key. If correct, the LBS can communicate further with the target using the public key.  



HLPSL:

role locationSighter(LoSi, T, LBS       : agent,
                     K_LL               : symmetric_key,
                     K_LoSi, K_LBS      : public_key,                     
                     Snd, Rcv           : channel(dy)) 
played_by LoSi def=

local   State           : nat,  
        P1_T            : public_key, 
        Loc             : text
           
init State := 1

transition

        1.  State  = 1 /\ Rcv({P1_T'.Loc'}_K_LoSi) 
        =|> State':= 3 /\ Snd({P1_T'.Loc'}_K_LL)
                     % /\ witness(LoSi, T, t_losi_loc, Loc')

end role


role target(LoSi, T, LBS : agent, K_T, K_LBS, K_LoSi : public_key, Psi_T : text, Cert_Psi_T : {text.text.public_key}_inv(public_key), Snd, Rcv : channel(dy)) played_by T def= local State : nat, N_LBS : text, Loc : text, P1_T : public_key const loc : protocol_id init State := 0 transition 0. State = 0 /\ Rcv(start) =|> State':= 2 /\ P1_T' := new() /\ Loc' := new() /\ Snd({P1_T'.Loc'}_K_LoSi) /\ secret(Loc, loc, {T, LoSi, LBS}) 2. State = 2 /\ Rcv({LBS.N_LBS'.Loc}_P1_T) =|> State':= 7 /\ Snd(P1_T.Psi_T.K_T.Cert_Psi_T.N_LBS'. {P1_T.Psi_T.K_T.Cert_Psi_T.N_LBS'}_inv(K_T)) /\ witness(T, LBS, lbs_t_n_lbs, N_LBS') % /\ wrequest(T, LoSi, t_losi_loc, Loc') %7. State = 7 /\ Rcv({LBS}_K_T) %=|>State':= 9 end role
role locationBeaconServer(LoSi, T, LBS : agent, K_LL : symmetric_key, K_LBS, K_CA : public_key, Domain : text, Snd, Rcv : channel(dy)) played_by LBS def= local State : nat, Loc, Psi_T, N_T : text, P1_T, K_T : public_key, N_LBS : text init State := 4 transition 4. State = 4 /\ Rcv({P1_T'.Loc'}_K_LL) =|> State':= 6 /\ N_LBS' := new() /\ Snd({LBS.N_LBS'.Loc'}_P1_T') 6. State = 6 /\ Rcv(P1_T.Psi_T'.K_T'.{Psi_T'.Domain.K_T'}_inv(K_CA).N_LBS. {P1_T.Psi_T'.K_T'.{Psi_T'.Domain.K_T'}_inv(K_CA).N_LBS}_inv(K_T')) =|> State':= 8 /\ request(LBS, T, lbs_t_n_lbs, N_LBS) % /\ Snd({LBS}_K_T') end role
role session (LoSi, T, LBS : agent, Psi_T : text, K_T, K_LBS, K_CA, K_LoSi : public_key, K_LL : symmetric_key, Domain : text, Cert_Psi_T : {text.text.public_key}_inv(public_key)) def= local SLBS, ST, SLoSi, RLBS, RT, RLoSi: channel(dy) composition locationSighter(LoSi, T, LBS, K_LL, K_LoSi, K_LBS, SLoSi, RLoSi) /\ target(LoSi, T, LBS, K_T, K_LBS, K_LoSi, Psi_T, Cert_Psi_T, ST, RT) /\ locationBeaconServer(LoSi, T, LBS, K_LL, K_LBS,K_CA,Domain,SLBS,RLBS) end role
role environment() def= const lbs_t_n_lbs, t_losi_loc : protocol_id, t, lbs, losi : agent, k_t, k_i, k_lbs, k_ca, k_losi : public_key, psi_t, psi_i : text, dom, dom_i : text, k_ll : symmetric_key intruder_knowledge = {losi, t, lbs, k_t, k_lbs, k_ca, k_losi, k_i, inv(k_i), psi_i, {psi_i.dom_i.k_i}_inv(k_ca)} composition session(losi, t, lbs, psi_t, k_t, k_lbs, k_ca, k_losi, k_ll, dom, {psi_t.dom.k_t}_inv(k_ca)) % repeat session to check for replay attacks /\ session(losi, t, lbs, psi_t, k_t, k_lbs, k_ca, k_losi, k_ll, dom, {psi_t.dom.k_t}_inv(k_ca)) /\ session(losi, i, lbs, psi_i, k_i, k_lbs, k_ca, k_losi, k_ll, dom, {psi_i.dom_i.k_i}_inv(k_ca)) % Since the intruder has no certificate of the domain that the LBS knows, the % LBS does not authorise the intruder and the third sesssion is not executable, % which is not a failure here. end role
goal secrecy_of loc % addresses G12 authentication_on lbs_t_n_lbs % addresses G1 and G3 % weak_authentication_on t_losi_loc % it is not important in this protocol to authenticate the LS % That's also the reason why we have no session here % where the intruder impersonates the location sighter. end goal
environment()