[Verifpal] Missed trivial attack

[Loup Vaillant David]

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