Proving that a protocol is not attackable

Consider the following protocol:

1. $A\rightarrow B: \{N_A,A\}_{pk(B)}$

2. $B\rightarrow A: \{N_B,N_A\}_{pk(A)}$

3. $A\rightarrow B: hash(N_B, A, B)$

where it is intended that when either $A$ or $B$ has completed their own role in the protocol, they are assured that the other has participated in the protocol with them and that $N_A$ and $N_B$ are random nonces generated by $A$ and $B$. $\{X\}_{Y}$ means that $X$ is encrypted under the key $Y$.

I know for a fact that no attack exists for this protocol but I'm unsure about how to prove it.

Without clearly defined attacker capabilities nor security guarantees of the different components (public-key encryption, hash function, etc). It is not easy to say whether or not this protocol is "attachable".

Given that we are given "carte blanche", I'll show two PITM attacks based on varying security and attacker models.

The general attacker model: I assume an attacker with full control of the network, they can inject, reorder, modify and otherwise delete messages. Furthermore, the attacker is allowed to "register" new users at anytime.

Attack 1: Identity misbinding and the need for more than CPA secure PKE

As written, it seems the protocol should be secure as long as a "secure" PKE scheme is used. However, the basic notion of security as in semantic security is not enough. At a high level, at end of the attack, $A$ thinks that they are talking to $B$, while $B$ thinks they are talking to the the attacker say $E$.

To do so, we will exhibit a CPA secure PKE for which the attack is possible. Let $\mathcal E$ be a "hybrid" PKE scheme (otherwise based) on a trapdoor function. Where encryption of the message $m$ under $pk$, roughly consists of generating a random value $s$ then generate a symmetric encryption key $k = H(s)$. $k$ is then used to encrypt the message with a stream cipher like algorithm, creating a ciphertext $c$. The final ciphertext from the PKE scheme is $$\{m\}_{pk} = (enc_{PKE}(pk, s), c)$$ The attack works as follows.

1. $ A\rightarrow B: c_1 = \{N_A,A\}_{pk(B)} $
2. The attacker intercepts this message, creates a new user $E$, modifies the ciphertext to a value $c_1'$ such that it decrypts to $N_A, E$. This is possible since we are using a stream cipher.(We also assume for instance, that the nonce and the identities are of fixed lengths, etc...)
3. $B$ decrypts the message and seems $E's$ identity therefore the second message is sent to $E$
4. $B \rightarrow E: c_2 = \{N_A. N_B\}_{pk_E}$.
5. $E$ decrypts $c_2$, and gets the nonces.
6. $E \rightarrow A: c_2' = \{N_A, N_B\}_{pk_A}$
7. $A \rightarrow B: c_3 = H(N_B, A, B)$
8. $E$ intercpets dropbs $c_3$ and send $c_3' = H(N_B, E, B)$

From the flow above, the view of $A$ is the same as if it interacted with $B$, while the view of $B$ is as if it interacted with $E$.

Attack 2: Long-Term secret exposure and Key-Compromise Integrity

Here the attacker's capabilities are strengthened and we allow compromise of long-term secret keys. Now obviously, if $sk_A$ is compromised (and $A$ is yet unaware) the attacker can impresonate $A$ at will; however it seems normal to expect that if $A$ runs a session with an honest $B$, $A$ should have assurance about who she talked to. However in this attack, compromise of $sk_A$ implies that the attacker can impresonate anyone towards $A$.

The basic idea as above is that, a PITM attacker will be able to decrypt the second message $\{N_A, N_B\}_{pk_A}$. The attacker can now conclude the interaction with $A$ and "cut the wire" towards B. As a consequence, $A$ thinks they are talking $B$ while in fact talking to B.

I'll assume a lot about the protocol that's not explicit in the question. I state some of that in the second section of this answer. Also I won't make my arguments overly detailed.

The desired insurance is

(participants) are assured that the other has participated in the protocol with them

but I'll remove with them, since that's not clear, and I see no precise definition for it that crypto can meet (it's always possible for a Man-in-the-Midle to relay messages unchanged). I'll replace it with since the protocol started, which is not to be confused with the much stronger in the way the protocol normally goes.

At step 1, $N_A$ was randomly chosen by $A$ and encrypted under $pk(B)$, as part of the plaintext of $\{N_A,A\}_{pk(B)}$. Thus only $A$ or some entity having some degree of capability to decipher $\{N_A,A\}_{pk(B)}$, that is only $B$, can know anything about $N_A$ beside it's length. Thus when at the conclusion of step 2, $A$ receives something that deciphers to $N_A$, and they know they did not use $N_A$ for another purpose than generating the message of step 1, they have assurance that $B$ participated in the protocol. I won't make this assurance quantitative, reserving that for the other direction.

At step 2, $N_B$ was randomly chosen by $B$ and encrypted under $pk(A)$, as part of the plaintext of $\{N_B,N_A\}_{pk(A)}$. Thus only $B$ or an entity having some degree of capability to decipher $\{N_B,N_A\}_{pk(A)}$, that is only $A$, can know anything about $N_B$ beside it's length. Assuming
  (a) the hash is a random oracle with output width $k_H$,
  (b) $N_B$ was chosen uniformly at random and has width $k_N$,
  (c) any adversary has advantage bounded by $\epsilon$ against the encryption,
then said adversary as probability upper-bounded by $2^{-k_H}+2^{-k_N}+\epsilon$ to exactly find the value of the hash of step 3. Thus when at the conclusion of step 3, $B$ finds such value for the hash they recompute, and they know they did not use $N_B$ for another purpose than generating the message of step 2, they have assurance that $A$ participated in the protocol.

If this reasoning is correct, step 3 could be simplified to $A\rightarrow B:\ hash(N_B)$. If not, I want to know why! This is not to be construed as a suggestion to do this simplification: including identities in what's hashed can only help, and I vaguely see it can block some intentional alterations of the protocol, only not of the kind that break the security assurance as I restated it.

Partial list of assumptions not stated in the question

• Late addition: Public keys are known and trusted before the protocol starts.
• Late addition: The cipher is secure to IND-CCA2. Sine I have no certainty about if we can get away with a lesser property, I'd rather err on the safe side.
• As often left unstated in protocol analysis, recipients of messages
  • attempt decryption and abort if that fails (as decryption of many IND-CCA2 ciphers do)
  • parse the deciphered messages as per the convention outlined for their generation and abort if that fails
  • check values received against their expected value if known from a previous step or otherwise computable (as occurs for the hash of step 3 on the $B$ side) and abort on no match. It does not seem necessary that such comparison is made constant-time.
  • or/and reuse said value for variables with the same name in forthcoming steps.
• In plaintext of encrypted messages, the comma sign symbolizes a form of concatenation with provision that from the result it remains possible to split at the point where the concatenation occurred, e.g. because one of the two messages concatenated has a fixed size. That does not seem necessary for the comma sign used in the message hashed at step 3.
• In messages, $A$ and $B$ are identities of the eponymous participants.
• Entities use their private keys only for the purpose of decrypting the messages they receive.
• After step 1, $B$ decides which public key they use for encryption at step 2, and towards what recipient to send at that step, on the basis of the second part $A$ of the deciphered message of step 1, and abort if they do not know the corresponding public key. It's not necessary for the security of the protocol as stated that they check that this second part is not their own identity.
• If participants attempt multiple simultaneous connections, as servers routinely do, it's assumed they keep separate variables for each protocol instance. I see no reason why it would not be OK that the multiple connection attempts an entity engages in are in potentially different directions.
• I disregard side channels not already discussed, faults attacks, and implementation errors.