[messaging] Can a pre-shared public key prevent MITM-attacks?

[U.Mutlu]

Martin Dehnel-Wild wrote on 12/04/2015 09:58 PM:
> Yes. Having a pre-shared public key definitely allows you to prevent MITM
> attacks. (Where by 'attack' I assume  you mean 'the adversary learns the
> agreed key')

Yes, indeed that's what I'm meaning by attacks.
But I have a hard time to see how the use of a public key can help here,
because the public key is by definition known to everybody, so also to
the MITM, but then he can easily replace the encrypted message by his
own message encrypted with the same public key --> bingo!

Or, where is my lack of understanding here?

Thanks for the info and links below, I'm going to study them.

> See e.g. MQV (https://en.wikipedia.org/wiki/MQV), HMQV, NAXOS for examples
> of modern(-ish) protocols that are not vulnerable to MITM attacks.
> Even Needham-Schroeder-Lowe protocol (
> https://en.wikipedia.org/wiki/Needham%E2%80%93Schroeder_protocol#Fixing_the_man-in-the-middle_attack,
> http://www.cs.cornell.edu/~shmat/courses/cs6431/lowe.pdf, 1996, not
> DH-based) is not vulnerable to MITM when you have pre-shared public keys.
>
> If you'd like machine-based proofs of the fact that they're not vulnerable
> to MITM attacks, run them through the Tamarin-prover (a security protocol
> verification tool that supports both falsification and unbounded
> verification of security protocols): download
> https://github.com/tamarin-prover/tamarin-prover/ and then look in
> examples/ake/dh/ and examples/classic/ for each of the above mentioned
> protocols.
>
> This is just one way of demonstrating their invulnerability (in this case
> in the symbolic world), but you can also find proofs for (I believe) most
> of the above in the computational setting as well, which are generally
> stronger 'proofs', but mostly human constructed and verified.
>
> Martin
>
>> Date: Fri, 4 Dec 2015 03:03:27 +0100
>> From: "U.Mutlu" <for-gmane at mutluit.com>
>> To: messaging at moderncrypto.org
>> Subject: [messaging] Can a pre-shared public key prevent MITM-attacks?
>> Message-ID: <n3qs9g$9p4$1 at ger.gmane.org>
>> Content-Type: text/plain; charset=UTF-8; format=flowed
>>
>> On the following wiki page it's boldly claimed that "A pre-shared public
>> key
>> also prevents man-in-the-middle attacks"
>> https://en.wikipedia.org/wiki/Diffie?Hellman_key_exchange#Public_key :
>>     "It is also possible to use Diffie?Hellman as part of a public key
>> infrastructure, allowing Bob to encrypt a message so that only Alice will
>> be
>> able to decrypt it, with no prior communication between them other than Bob
>> having trusted knowledge of Alice's public key. Alice's public key is
>> (g^a mod p, g, p). To send her a message, Bob chooses a random b and then
>> sends Alice g^b mod p (un-encrypted) together with the message encrypted
>> with symmetric key (g^a)^b mod p. Only Alice can determine the symmetric
>> key
>> and hence decrypt the message because only she has a (the private key).
>> A pre-shared public key also prevents man-in-the-middle attacks."
>>
>> I have my doubts.
>> What do others think of 'MITM prevention by using public key encryption'?