PROTOCOL:
ZG: Zhou-Gollmann Non-repudiation protocol

PURPOSE:
Fair two-party non-repudiation
 

REFERENCE:

http://citeseer.ist.psu.edu/62704.html  

MODELER:

 

ALICE_BOB:

  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)

 

LIMITATIONS:

We cannot model the (fairness) assumption that the server is eventually available, i.e. communication with the server is not blocked forever. Since we moreover cannot state and check liveness properties, we can only give approximations of non-repudiation and fair exchange.

 

PROBLEMS:
9

 

CLASSIFICATION:
G1, G2, G3, (G18), (G19), (fair exchange)

 

ATTACKS:
None

 

NOTES:

 


HLPSL:


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