[prev in list] [next in list] [prev in thread] [next in thread] 

List:       avispa-users
Subject:    Re: [Avispa-users] Kudo-Mathuria protocol
From:       Laurent Vigneron <laurent.vigneron () loria ! fr>
Date:       2008-11-19 14:08:56
Message-ID: 20081119150856.xvcx3trcsg8s0cww () webmail ! loria ! fr
[Download RAW message or body]


Hello Péter,

There are several errors in your specification.
I am surprised that you could run a tool on it... (the translator  
hlpsl2if should have raised several errors).

Please find bellow the main rules that you should follow for  
correcting your spec.

And looking at the spec and at the cited paper, the attack is  
"trivial": Xa cannot be secret, as it appears in a message signed by A  
(its public key is... public), and encrypted by the public key Tktreq  
(the corresponding private key is given almost in clear in the last  
message of the protocol).

Enjoy your play with AVISPA! :)

Laurent.


- a prime (') added to a variable is efficient for one transition, the  
one where you learn or generate the value of the variable.
(most of your transitions are not correct wrt. this rule)

Example: (role alice)
    1. Allapot = 0 /\ RCV(start) =|> Allapot':=3 /\ Enc':=new()
       /\ Treq':=new() /\ SND(Enc'.Treq')
means that Enc and Treq get a new (random) value, and Allapot changed  
its value from 0 to 3.
Writing
    2. Allapot = 3 /\ RCV({Enc'.Treq'.Tktreq}_inv(Kt)) =|> Allapot':=6  
/\ SND(A)
means that in this other transition, A learns the values of Enc and  
Treq from the received message.
Instead, writing
    2. Allapot = 3 /\ RCV({Enc.Treq.Tktreq}_inv(Kt)) =|> Allapot':=6 /\ SND(A)
means that A checks the received values with the one he has generated  
in the previous transition.

- each transition should contain at most one input (RCV) and one output (SND).
(transition 2 of role bob has two outputs; you should decompose it  
into two transitions)

- what you write as received message has to correspond to what the  
agent is able to learn by decomposition of the received message.
(this is correct in your spec)

- what you write as sent message has to correspond to what the agent  
is able to compose from his knowledge.
(in your spec, you sometimes re-use par of a received message that  
cannot be compose by the agent)

Example: (role alice)
   2. Allapot = 3 /\ RCV({Enc.Treq.Tktreq}_inv(Kt)) =|> ...
   3. ... /\
      SND({{Xa'.Ra'.A}_Tktreq.A.B.Treq.Nb'.Tktreq}_inv(Ka)
          .{Enc.Treq.Tktreq}_inv(Kt))
You re-use {Enc.Treq.Tktreq}_inv(Kt), but this message is signed by S,  
to A cannot compose it.
For a correct semantics, you should have stored this message in a  
local variable (of type message, for example), and re-use this variable:
   2. Allapot = 3 /\ RCV(Msg3') /\ Msg3'={Enc.Treq.Tktreq}_inv(Kt) =|> ...
   3. ... /\
      SND({{Xa'.Ra'.A}_Tktreq.A.B.Treq.Nb'.Tktreq}_inv(Ka).Msg3)

Finally, you have forgotten
- to generate the value of Dec in transition 2 of role bob
- to sign the last message, send by S to B:
   SND({Dec'.Treq.inv(Tktreq)}_inv(Kt))


_______________________________________________
Avispa-users mailing list
Avispa-users@avispa-project.org
http://mail63.csoft.net/mailman/listinfo/avispa-users

[prev in list] [next in list] [prev in thread] [next in thread]