[Verifpal] Missed trivial attack
nadim at symbolic.software
Wed Sep 18 21:34:12 CEST 2019
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.
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.)
> 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
> But first, there's this little issue.
> Verifpal mailing list
> Verifpal at lists.symbolic.software
More information about the Verifpal