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)
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.
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()