S: Trusted Third Party (TTP)
C: Commitment = {M}_K
L: Label = hash(M.K)
A -> B: fNRO.B.L.C.NRO NRO = {fNRO.B.L.C}_inv(Ka)
A <- B: fNRR.A.L.NRR NRR = {fNRR.A.L.C}_inv(Kb)
A -> S: fSUB.B.L.K.SubK SubK = {fSUB.B.L.K}_inv(ka)
A <-> S: fCON.A.B.L.K.ConK ConK = {fCON.A.B.L.K}_inv(ks)
B <-> S: fCON.A.B.L.K.ConK ConK = {fCON.A.B.L.K}_inv(ks)
role alice(A, B, S : agent,
Ka, Kb, Ks : public_key,
Snd, Rcv : channel(dy)) played_by A def=
local State : nat,
M : text,
K : symmetric_key,
C : {text}_symmetric_key,
L : hash(text.symmetric_key),
NRO , NRR,
SubK, ConK: message
const h: hash_func
init State := 0
transition
0. State = 0 /\ Rcv(start)
=|>
State':= 1
/\ M':=new()
/\ K':=new()
/\ C':={M'}_K'
/\ L':=h(M'.K')
/\ NRO':={fNRO.B.L'.C'}_inv(Ka)
/\ Snd (fNRO.B.L'.C'.NRO')
/\ witness(A,B,bob_alice_nro,NRO')
10. State = 1
/\ B=i /\ iknows(M)
--|>
wrequest(A,A,dishonest_bob_prematurely_learns_M,M)
1. State = 1
/\ Rcv (fNRR.A.L.NRR')
/\ NRR'= {fNRR.A.L.C}_inv(Kb)
=|>
State':= 2
/\ SubK':={fSUB.B.L.K}_inv(Ka)
/\ Snd (fSUB.B.L.K.SubK')
/\ request(A,B,alice_bob_nrr,NRR')
/\ witness(A,S,server_alice_sub,SubK')
/\ witness(A,B,bob_learns_M_only_after_alice_got_NRR,K)
2. State = 2
--|>
State':= 3
/\ Snd(fREQ.A.B.L)
3. State = 3
/\ Rcv (fCON.A.B.L.K.ConK')
/\ ConK'={fCON.A.B.L.K}_inv(Ks)
=|>
State':= 4
/\ request(A,S,alice_server_con,ConK')
% Non-repudiation of Receipt: Alice has checked both NRR and ConK
% /\ B=i --> iknows(ConK')
% 4. State = 4
% /\ B=i /\ not(iknows(ConK))
% --|>
% wrequest(A,A,despite_evidence_dishonest_bob_does_not_have_ConK,ConK)
end role
role bob(B, A, S : agent,
Kb, Ka, Ks : public_key,
Snd, Rcv : channel (dy)) played_by B def=
local State : nat,
M : text,
K : symmetric_key,
C : {text}_symmetric_key,
L : hash(text.symmetric_key),
NRO, NRR,
ConK: message
init State := 0
transition
0. State = 0
/\ Rcv (fNRO.B.L'.C'.NRO')
/\ NRO'={fNRO.B.L'.C'}_inv(Ka)
=|>
State':= 1
/\ NRR':={fNRR.A.L'.C'}_inv(Kb)
/\ Snd (fNRR.A.L'.NRR')
/\ wrequest(B,A,bob_alice_nro,NRO')
/\ witness(B,A,alice_bob_nrr,NRR')
1. State = 1
--|>
State':= 2
/\ Snd(fREQ.A.B.L)
2. State = 2
/\ Rcv (fCON.A.B.L.K'.ConK')
/\ ConK'={fCON.A.B.L.K'}_inv(Ks)
/\ C = {M'}_K' % M is extracted here!
=|>
State':= 3
/\ request(B,S,bob_server_con,ConK')
/\ wrequest(B,A,bob_learns_M_only_after_alice_got_NRR,K')
% Non-repudiation of Origin: Bob has checked both NRO and ConK
% /\ A=i --> iknows(ConK')
% 3. State = 3
% /\ A=i /\ not(iknows(ConK))
% --|>
% wrequest(B,B,despite_evidence_dishonest_alice_does_not_have_ConK,ConK)
end role
role server (S, A : agent,
Ks, Ka : public_key,
Snd, Rcv : channel (dy)) played_by S def=
local State: nat,
K : symmetric_key,
B : agent,
L : hash(text.symmetric_key),
SubK,
ConK: message
init State := 0
transition
0. State = 0
/\ Rcv (fSUB.B'.L'.K'.SubK')
/\ SubK'={fSUB.B'.L'.K'}_inv(Ka)
=|>
State':= 1
/\ wrequest(S,A,server_alice_sub,SubK')
1. State = 1
/\ Rcv(fREQ.A.B.L) % request can originate from A or B
=|>
State':= 1 % loop!
/\ ConK':={fCON.A.B.L.K}_inv(Ks)
/\ Snd (fCON.A.B.L.K.ConK') % actually made available to both A and B
/\ witness(S,A,alice_server_con,ConK')
/\ witness(S,B, bob_server_con,ConK')
end role
role session(A,B,S: agent,
Ka,Kb,Ks: public_key,
Snd,Rcv: channel (dy)) def=
composition
alice (A,B,S,Ka,Kb,Ks,Snd,Rcv) /\
bob (B,A,S,Kb,Ka,Ks,Snd,Rcv) /\
server(S,A, Ks,Ka,Snd,Rcv)
end role
role environment() def=
local Snd, Rcv: channel (dy)
const a,b,s,i: agent,
ka,kb,ks,ki: public_key,
alice_bob_nrr, bob_alice_nro,
alice_server_con, bob_server_con,
server_alice_sub,
bob_learns_M_only_after_alice_got_NRR,
dishonest_bob_prematurely_learns_M,
despite_evidence_dishonest_alice_does_not_have_ConK,
despite_evidence_dishonest_bob_does_not_have_ConK: protocol_id,
fREQ,fNRO,fNRR,fSUB,fCON: text
intruder_knowledge = {a,b,s,ka,kb,ks,ki,inv(ki),
fREQ,fNRO,fNRR,fSUB,fCON}
composition
% Only for checking the less important standard authentication goals:
session(a,b,s,ka,kb,ks,Snd,Rcv)
/\ session(a,b,s,ka,kb,ks,Snd,Rcv) % for checking replays
/\ session(a,i,s,ka,ki,ks,Snd,Rcv)
/\ session(i,b,s,ki,kb,ks,Snd,Rcv)
% /\ session(a,b,i,ka,kb,ki,Snd,Rcv) % the server is trusted!
end role
goal
% all authentication goals check for entity authentication (G1) and/or
% message authentication (G2), the strong ones also for replay protection (G3)
weak_authentication_on server_alice_sub % addresses G1 and G2
% signals showing failure of evidence for non-repudiation of...
%... origin (G18):
weak_authentication_on despite_evidence_dishonest_alice_does_not_have_ConK
%... delivery (G19):
weak_authentication_on despite_evidence_dishonest_bob_does_not_have_ConK
authentication_on alice_bob_nrr % addresses part of G19 (proof of delivery)
weak_authentication_on bob_alice_nro % address part of G18 (proof of origin)
% but only when both parties are honest (i.e. not played by the intruder)
authentication_on alice_server_con % addresses G19 and fairness for Bob
authentication_on bob_server_con % addresses G18 and fairness for Alice
% together with the following meta-level liveness argument:
% after the server has sent conK to one of the parties,
% due to the assumption that communication with it is not blocked forever,
% if this party has reached its final (successful) state,
% the other party will eventually also reach its final (successful) state.
% Note that these authentiation goals are not fulfilled trivially
% because the intruder is not allowed to play the role of the server.
% necessary conditions for fairness for Alice:
weak_authentication_on bob_learns_M_only_after_alice_got_NRR
weak_authentication_on dishonest_bob_prematurely_learns_M
end goal
environment()