VARIANT:
with password and certificate

REFERENCE:

 

PURPOSE:

A Location Recipient obtains Location Information, restricted by a Privacy Rule (policy), about a Target from a Location Server. Authorization of the Location Recipient via a simple password which may be shared with other Location Recipients assumed to trust each other. Uses a pseudonym for the Target related to its public key via a certificate.  

MODELER:

 

ALICE_BOB:

 T  : Target (subsumes Location Generator, Mobile User and Rule Maker)
 LS : Location Server (subsumes Rule Holder)
 LR : Location Recipient
 LI : Location Information
 GR : Granularity
 % initially, T sends to LR its pseudonym and password, requested by LR:
 1. T <----------------------------------------------- LR.{T.N1}_K_T_LR -- LR
 2. T ------------------------------------------ {PW_T.Psi_T.N1}_K_T_LR -> LR
 % then, T informs LS about its policy, and later also about its location:
 3. T ---------- {Psi_T.K_T}_inv(K_CA).
      {GR.{PW_T}_K_LS.Psi_T}_inv(K_T) -> LS
 4. T - {TS.{LI}_K_LS.Psi_T}_inv(K_T) -> LS
 % some time later, LR requests the location information of T from LS:
 5.                                      LS <- {K_LR.PW_T.Psi_T.N2}_K_LS -- LR
 6.                                      LS ----------- {GR(LI).N2}_K_LR -> LR
 

PROBLEMS:
6
 

LIMITATIONS:

Our model does not allow location updates by re-sending the fourth message with new data. If such updates are possible, one must prevent replay attacks, which can be done with a timestamp. Since HLPSL does not support time, we include an unused pseudo-timestamp TS just as a reminder.

For simplicity, we let the target sign its certificate. This should actually be done by CA.

 

CLASSIFICATION:
G1, G2, G3, G12, G20
 

ATTACKS:
None
 

NOTES:

We model the Location Generator as part of the Target and let the Target transmit the location information in a secured way to the Location Server. An alternative is that the Location Server senses the presence of the Target directly (still without knowing T's identity).

In this variant we use a pre-shared symmetric key between T and LR. Therefore in the first message the identity of LR needs to be sent in the clear because otherwise T does not know why shared key to use for decryption.

The Location Server can authenticate the Target (and thus also check the integrity of the privacy rule provided by T) using a certificate, signed by a trusted third party called CA, that states the relation between the pseudonym and the public key.

In the last message, LS uses a secret temporary key K_LR received from LR in the previous message, to encrypt the location information for LR. Therefore LS only needs to echo N2 in order to authenticate itself.

The Location Server can authenticate the LR only modulo the group of agents that know the password. Therefore we resort to checking the secrecy of the password instead of weak_authentication_on_ls_LR_PW_T. If the intruder plays the role of LR and we require weak_authentication_on_ls_LR_PW_T then we get a failure of (too strong) authentication:

 GOAL
   weak_authentication_on_ls_LR_PW_T
 ATTACK TRACE
 i -> (t,11): i.{t.n240}_k_T_i
 (t,11) -> i: {PW_T.Psi_T.n240}_k_T_i
 (t,11) -> i: {Psi_T.K_T}_inv(k_CA).
              {GR.{PW_T}_k_LS.Psi_T}_inv(K_T)
 (t,11) -> i: {TS.{LI}_k_LS.Psi_T}_inv(K_T)
 i -> (ls,3): {Psi_T.K_T}_inv(k_CA).
              {GR.{PW_T}_k_LS.Psi_T}_inv(K_T)
 i -> (ls,3): {TS.{LI}_k_LS.Psi_T}_inv(K_T)
 i -> (ls,3): {k292.PW_T.Psi_T.n294}_k_LS
 (ls,3) -> i: {GR(LI).n294}_k292
 


HLPSL:

role target(
        T, LS, LR       : agent,
        K_T_LR          : symmetric_key, % should be determined by a lookup
        K_LS, K_CA      : public_key,
        Snd_LR, Snd_LS, Rcv: channel(dy)) played_by T def=

local
        State   : nat,
        N1      : text, 
        Psi_T   : text,
        K_T     : public_key,
        PW_T    : text,
        Cert_T  : {text.public_key}_inv(public_key),
        LI, TS  : text,
        GR      : hash_func

init State := 1

transition

        1. State  = 1 /\ Rcv(LR.{T.N1'}_K_T_LR) 
       =|> State':= 3 /\ Psi_T' := new()
                      /\ PW_T'  := new()
                      /\ secret(PW_T', pw_T, {T, LS, LR})
                      /\ Snd_LR({PW_T'.Psi_T'.N1'}_K_T_LR)
                      /\ witness (T, LR, lr_T_N1, N1')
                      /\ wrequest(T, LR, t_LR_LR, LR)
% could be new transition here, but not done for efficiency
                      /\ GR' := new()  % chooses some granularity (accuracy)
                      /\ K_T':= new()
                      /\ Snd_LS({Psi_T'.K_T'}_inv(K_CA). % should be signed by CA
                                {GR'.{PW_T'}_K_LS.Psi_T'}_inv(K_T'))
                      /\ witness(T, LS, ls_T_GR, GR')
% could be new transition here, but not done for efficiency
                      /\ LI' := new()
                      /\ secret(LI', li, {T, LS, LR}) 
                      /\ secret((GR'(LI')), filtered_LI, {T, LS, LR})
                      /\ TS' := new()
                      /\ Snd_LS({TS'.{LI'}_K_LS.Psi_T'}_inv(K_T'))
                      /\ witness (T, LR, lr_T_filtered_LI, (GR'(LI')))

end role


role locationServer( T, LS, LR: agent, % but LS does not actually use identity of T and LR Psi_Table: (text.text.hash_func) set, K_LS,K_CA: public_key, Snd, Rcv : channel(dy)) played_by LS def= local State : nat, Psi_T, PW_T : text, K_T : public_key, N2 : text, K_LR : symmetric_key, LI, TS : text, GR : hash_func init State := 5 transition 5. State = 5 /\ Rcv({Psi_T'.K_T'}_inv(K_CA). {GR'.{PW_T'}_K_LS.Psi_T'}_inv(K_T')) =|> State':= 7 /\ Psi_Table' := cons(PW_T'.Psi_T'.GR', Psi_Table) 7. State = 7 /\ Rcv({TS'.{LI'}_K_LS.Psi_T}_inv(K_T)) =|> State':= 9 9. State = 9 /\ Rcv({K_LR'.PW_T'.Psi_T.N2'}_K_LS) /\ in(PW_T'.Psi_T.GR', Psi_Table) % uses PW_T and Psi_T to look up GR in the table =|> State':= 11/\ Snd({(GR'(LI)).N2'}_K_LR') /\ wrequest(LS, T , ls_T_GR, GR') % delayed % /\ wrequest(LS, LR, ls_LR_PW_T, PW_T') /\ witness (LS, LS, lr_LS_N2, N2') % to any LR! end role
role locationRecipient( T, LS, LR : agent, K_T_LR : symmetric_key, K_LS : public_key, Snd, Rcv : channel(dy)) played_by LR def= local State : nat, N1, N2 : text, Psi_T, PW_T : text, K_LR : symmetric_key, % could also be: public_key Filtered_LI : hash(text) init State := 0 transition 0. State = 0 /\ Rcv(start) =|> State':= 2 /\ N1' := new() /\ Snd(LR.{T.N1'}_K_T_LR) /\ witness(LR, T, t_LR_LR, LR) 2. State = 2 /\ Rcv({PW_T'.Psi_T'.N1}_K_T_LR) =|> State':= 8 /\ N2' := new() /\ K_LR' := new() /\ secret(K_LR' , k_LR, {LR, LS}) /\ Snd({K_LR'.PW_T'.Psi_T'.N2'}_K_LS) /\ request(LR, T , lr_T_N1, N1) % /\ witness(LR, LS, ls_LR_PW_T, PW_T') 8. State = 8 /\ Rcv({Filtered_LI'.N2}_K_LR) =|> State':= 10/\ request(LR, T , lr_T_filtered_LI, Filtered_LI') /\ request(LS, LS, lr_LS_N2, N2) end role
role session(T, LS, LR : agent, K_T_LR : symmetric_key, K_LS, K_CA : public_key, Psi_Table : (text.text.hash_func) set) def= local STLR, STLS, RT, SLR, RLR, SLS, RLS: channel(dy) composition target (T, LS, LR, K_T_LR, K_LS, K_CA, STLR, STLS, RT) /\ locationServer (T, LS, LR, Psi_Table, K_LS, K_CA, SLS, RLS) /\ locationRecipient(T, LS, LR, K_T_LR, K_LS, SLR, RLR) end role
role environment() def= local Psi_Table: (text.text.hash_func) set % shared between all instances of LS const li, filtered_LI, pw_T, k_LR, ls_T_GR, lr_T_N1, t_LR_LR, ls_LR_PW_T, lr_LS_N2, lr_T_filtered_LI : protocol_id, t, ls, lr : agent, k_LS, k_CA, k_i : public_key, k_T_LR, k_T_i, k_i_LR : symmetric_key init Psi_Table := {} intruder_knowledge = {t, ls, lr, k_T_i, k_LS, k_i_LR, k_i, inv(k_i), k_CA} composition session(t, ls, lr, k_T_LR, k_LS, k_CA, Psi_Table) % /\ session(t, ls, lr, k_T_LR, k_LS, k_CA, Psi_Table) % repeat session to check for replay attacks /\ session(i, ls, lr, k_i_LR, k_LS, k_CA, Psi_Table) % It does not make much sense to let the intruder play the role of T % since then the intruder knows its location information anyway. /\ session(t, ls, i , k_T_i, k_LS, k_CA, Psi_Table) % It does not make much sense to let the intruder play the role of LR % since then the intruder is allowed to know the (secret) location of T as % well as the password, which contradicts the trust assumption between LRs. end role
goal secrecy_of li, filtered_LI, pw_T, 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 Recipient authenticates the Location Server: authentication_on lr_LS_N2 % addresses G2 and G3 % the Location Server cannot fully authenticate the Location Recipient % because there may be many of them, all legitimately knowing the password % weak_authentication_on ls_LR_PW_T % addresses G2 % weak authentication and integrity of Granularity weak_authentication_on ls_T_GR % addresses G1 % additional authentication goals, not in RFC3693: authentication_on lr_T_N1 % 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()