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