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
For simplicity, we let the target sign its certificate. This should actually be done by CA.
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
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()