[Avispa-users] May Avispa find an attack after a second one?

[Juan Carlos López Pimentel]

Hi Laurent,
thanks for your soon answer...

In the protocol:

1 A --> B: A, {B, Nxa, {Nya}_Kb}_inv(Ka)


Laurent Vigneron wrote:

>About the first attack that you are looking for, I am not convinced
>this is one.  Could you explain what is the property that is not
>satisfied?
>In the trace
>
> > Attack 1:
> > i -> (a,3): start
> > (a,3) -> i: a.{b.Nxa(1).{Nya(1)}_kb}_inv(ka)
> > i -> (b,10): i.{b.x38.{Nya(1)}_kb}_inv(ki)
>
>b knows that i has sent him this message, and as i is the intruder,
>there is no authentication done between b and i.
>  
>

Maybe I have an erroneous idea about the role that "i" (the intruder) is 
playing with respect to "b". In the above attack I have the idea that 
"b", naively, thinks that "i" is a honest agent and "b" could 
authenticate to "i" on Nya  (same variable where "a" does a witness).  
This attack is shown in http://www.lsv.ens-cachan.fr/spore/ccittx509_1.html

If you think that I have an erroneous idea, please I will be grateful 
you tell me why...

best regards,

Juan Carlos

>  
>