[Verifpal] Missed trivial attack

[Nadim Kobeissi]

Not at all surprising, this is what I was talking about when I said that I was sure 0.6.8 would miss attacks. I’m working on resolving similar scenarios.

Verifpal should be considered under heavy refactoring until 0.7.

Nadim Kobeissi
Symbolic Software • https://symbolic.software

> On Sep 18, 2019, at 9:30 PM, Loup Vaillant David <loup at loup-vaillant.fr> wrote:
> 
> (Originally sent to Nadim only, sorry for the duplicate.)
> 
> Hi,
> 
> I have a little problem with this Model:
> 
>    attacker [active]
>    principal Alice [ generates e ]
>    principal Bob   [             ]
>    Alice -> Bob: e
>    principal Bob   [ H = HASH(e) ]
> 
>    queries [
>        authentication? Alice -> Bob : e
>    ]
> 
> The latest commit from the master branch (b3dd726), finds no result.
> Yet `e` here is successfully used in HASH(e), right?
> 
> ---
> 
> I found this trying to build a minimum failing test case for Monokex. I
> figured the recipient could not authenticate anything, because the
> initiator never sent them any public key (not static, not ephemeral)
> over a secure channel. Then there's the little problem of sending the
> same thing twice, but making sure the second time is right:
> 
>    // before the protocol
>    Alice -> Bob [public_key]
> 
>    // during the protocol
>    Alice -> Bob public_key
> 
> In real world protocols, Bob compares the insecurely sent public key,
> with the one he trusts. I'm not sure how we would model that in
> Verifpal?
> 
> But first, there's this little issue.
> 
> Loup.
> 
> 
> _______________________________________________
> Verifpal mailing list
> Verifpal at lists.symbolic.software
> https://lists.symbolic.software/mailman/listinfo/verifpal