VARIANT:
with two self-signatures

REFERENCE:

 

PURPOSE:

A Location Recipient obtains Location Information, restricted by a Privacy Rule (policy), about a Target from a Location Server. Using pseudonyms and self-signatures 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)
 LS : Location Server (subsumes Rule Holder)
 LR : Location Recipient
 LI : Location Information
 GR : Granularity
 % initially, T and LR exchange their pseudonyms:
 1. T <------------------------ {LR}_K_T.{{T.N1}_K_T .h(P_LR)}_inv(K_LR) -- LR
 2. T ------------------------------------ {{N1}_K_LR.h(P_T )}_inv(K_T ) -> LR
 % then, T informs LS about its policy, and later also about its location:
 3. T --- {GR.h(P_LR).h(P_T)}_inv(P_T).P_T -> LS
 4. T - {TS.{LI.h(P_T)}_K_LS}_inv(P_T).P_T -> LS
 % some time later, LR requests the location information of T from LS:
 5.                              LS <- {h(P_LR).h(P_T).N2}_inv(P_LR).P_LR - LR
 6.                              LS --- {{GR(LI)}_P_LR.N2}_inv(K_LS) -----> LR
 

PROBLEMS:
7
 

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.

 

CLASSIFICATION:
G1, G2, G3, G12, G20
 

ATTACKS:

There is a useless "attack" where the intruder acts like both the T and LR to confuse the LS (violating both weak_authentication_on_ls_LR_P_LR and weak_authentication_on_ls_T_GR), but he does not gain anything interesting. Yet a DoS attack could be based on this.
 ATTACK TRACE
 i -> (ls,3): {g67.h(j69).h(i64)}_inv(i64).i64
 i -> (ls,3): {t66.{l65.h(i64)}_k_LS}_inv(i64).i64
 i -> (ls,3): {h(j69).h(i64).n68}_inv(j69).j69
 (ls,3) -> i: {{g67(l65)}_j69.n68}_inv(k_LS)
 
 

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 public-key cryptography between T and LR.

Both T and LR use public/private keys created on-the-fly. The private keys are used to sign the traffic to LS. The public key is sent along with the messages to LS such that LS can check the consistency of the public key with the pseudonym in the signed part (self-signature) since the pseudonym is nothing but the hashed version of the public key. Neither the pseudonyms nor the related public keys need to be kept secret.

The Location Server just knows the pseudonyms (and the related public keys) but not the identities of the Location Recipient and of the Target. Still, LS can authenticate T and LR, in the sense that LS checks the consistency of the messages received from these two parties.

In the fourth message, we use {LI.h(P_T)}_K_LS rather than {LI}_K_LS.h(P_T) in order to prevent re-use of {LI}_K_LS in a kind of MITM attack:

 GOAL
   secrecy_of_filtered_LI
 ATTACK TRACE
 i -> (lr,3): start
 (lr,3) -> i: {lr}_k_T.{{t.N1}_k_T .h(P_LR)}_inv(k_LR)
 i -> (t ,3): {lr}_k_T.{{t.N1}_k_T .h(P_LR)}_inv(k_LR)
 (t ,3) -> i:          {{  N1}_k_LR.h(P_T)}_inv(k_T)
 (t ,3) -> i:     {GR.h(P_R).h(P_T)}_inv(P_T).P_T
 (t ,3) -> i:  {TS.{LI}_k_LS.h(P_T)}_inv(P_T).P_T
 i -> (ls,3):    {g94.h(j96).h(i91)}_inv(i91).i91
 i -> (ls,3): {t93.{LI}_k_LS.h(i91)}_inv(i91).i91
 i -> (ls,3):    {h(j96).h(i91).n95}_inv(j96).j96
 (ls,3) -> i:    {{g94(LI)}_j96.n95}_inv(k_LS)
 i -> (i,17): GR(LI)
 

In the last message, LS re-uses the publicly known key P_LR to encrypt the location information for LR. Therefore, LS has to sign the message in order to authenticate itself to LR.  



HLPSL:

role target(
        T, LS, LR       : agent,
        K_T, K_LS, K_LR : public_key,
        H               : hash_func,
        Snd_LR, Snd_LS, Rcv: channel(dy)) played_by T def=

local
        State   : nat,
        N1      : text, 
        P_T     : public_key,
        Psi_LR  : hash(public_key),
        LI, TS  : text,
        GR      : hash_func

init State := 1

transition

        1. State  = 1 /\ Rcv({LR}_K_T.{{T.N1'}_K_T.Psi_LR'}_inv(K_LR)) 
       =|> State':= 3 /\ P_T'  := new()
                      /\ Snd_LR({{N1'}_K_LR.H(P_T')}_inv(K_T))
                      /\ witness (T, LR, lr_T_N1, N1')
                      /\ wrequest(T, LR, t_LR_Psi_LR, Psi_LR')
% could be new transition here, but not done for efficiency
                      /\ GR' := new()  % chooses some granularity (accuracy)
                      /\ Snd_LS({GR'.Psi_LR'.H(P_T')}_inv(P_T').P_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'.H(P_T')}_K_LS}_inv(P_T').P_T')

                      /\ witness (T, LR, lr_T_filtered_LI, (GR'(LI')))
                      /\ witness(LS, LR, ls_LR_P_LR, LS) 






end role


role locationServer( T, LS, LR: agent, % but LS does not actually use identity of T and LR Psi_Table: (hash(public_key).hash(public_key).hash_func) set, K_LS : public_key, H : hash_func, Snd, Rcv : channel(dy)) played_by LS def= local State : nat, P_T,P_LR : public_key, N2 : text, Psi_LR : hash(public_key), LI, TS : text, GR : hash_func init State := 5 transition 5. State = 5 /\ Rcv({GR'.Psi_LR'.H(P_T')}_inv(P_T').P_T') =|> State':= 7 /\ Psi_Table':= cons(Psi_LR'.H(P_T').GR', Psi_Table) 7. State = 7 /\ Rcv({TS'.{LI'.H(P_T)}_K_LS}_inv(P_T).P_T) =|> State':= 9 9. State = 9 /\ Rcv({H(P_LR').H(P_T).N2'}_inv(P_LR').P_LR') /\ in(H(P_LR').H(P_T).GR', Psi_Table) % uses Psi_LR and Psi_T to look up GR in the table =|> State':=11 /\ Snd({{(GR'(LI))}_P_LR'.N2'}_inv(K_LS)) /\ wrequest(LS, T , ls_T_GR, GR') % delayed /\ wrequest(LS, LR, ls_LR_P_LR, P_LR') /\ witness (LS, LS, lr_LS_N2, N2') % to any LR! end role
role locationRecipient( T, LS, LR : agent, K_T, K_LS, K_LR : public_key, H : hash_func, Snd, Rcv : channel(dy)) played_by LR def= local State : nat, N1, N2 : text, Psi_T : hash(public_key), P_LR : public_key, Filtered_LI : hash(text) init State := 0 transition 0. State = 0 /\ Rcv(start) =|> State':= 2 /\ N1' := new() /\ P_LR' := new() /\ Snd({LR}_K_T.{{T.N1'}_K_T.H(P_LR')}_inv(K_LR)) /\ witness(LR, T, t_LR_Psi_LR, H(P_LR')) 2. State = 2 /\ Rcv({{N1}_K_LR.Psi_T'}_inv(K_T)) =|> State':= 8 /\ N2' := new() /\ Snd({H(P_LR).Psi_T'.N2'}_inv(P_LR).P_LR) /\ witness(LR, LS, ls_LR_P_LR, P_LR) /\ request(LR, T , lr_T_N1, N1) /\ witness(LS, T , ls_T_GR, LS) 8. State = 8 /\ Rcv({{Filtered_LI'}_P_LR.N2}_inv(K_LS)) =|> 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, K_LS, K_LR : public_key, H : hash_func, Psi_Table : (hash(public_key).hash(public_key).hash_func) set) def= local STLR, STLS, RT, SLR, RLR, SLS, RLS: channel(dy) composition target (T, LS, LR, K_T, K_LS, K_LR, H, STLR, STLS, RT) /\ locationServer (T, LS, LR, Psi_Table, K_LS, H, SLS, RLS) /\ locationRecipient(T, LS, LR, K_T, K_LS, K_LR, H, SLR, RLR) end role
role environment() def= local Psi_Table: (hash(public_key).hash(public_key).hash_func) set % shared between all instances of LS const li, filtered_LI, ls_T_GR, lr_T_N1, t_LR_Psi_LR, ls_LR_P_LR, lr_LS_N2, lr_T_filtered_LI : protocol_id, t, ls, lr : agent, k_T, k_LS, k_LR, k_i : public_key, h : hash_func init Psi_Table := {} intruder_knowledge = {t, ls, lr, k_T, k_LS, k_LR, k_i, inv(k_i), h} composition session(t, ls, lr, k_T, k_LS, k_LR, h, Psi_Table) % /\ session(t, ls, lr, k_T, k_LS, k_LR, h, Psi_Table) % repeat session to check for replay attacks /\ session(i, ls, lr, k_i, k_LS, k_LR, h, 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, k_LS, k_i , h, 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. end role
goal secrecy_of li, filtered_LI % 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 Location authenticates the Location Server: authentication_on lr_LS_N2 % addresses G2 and G3 % the Location Server (weakly) authenticates the Location Recipient: weak_authentication_on ls_LR_P_LR % 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_Psi_LR % addresses G1 % and G20: T authorizes LR to receive the location via LS end goal
environment()