we will build a NuSMV model to reconstruct the man-inthe-middle attack to the Needham-Schroeder authentication protocol. Consider a simplified public-key Needham-Schroeder protocol:
(1) A → B: {Na,A}Kb
(2) B → A: {Na,Nb}Ka
(3) A → B: {Nb}Kb where Na,Nb are the nonces of A,B, and Ka,Kb are the public keys of A,B respectively. Messages encrypted by a party’s public key can only be decrypted by the party. At Step (1), A initiates the protocol by sending a nonce and its identity (encrypted by B’s public key) to B. Using its private key, B deciphers the message and gets A’s identity. At Step (2), B sends A’s and its nonces (encrypted by A’s public key) back to A. Using its private key, A decodes the message and checks its nonce is returned. At Step (3), A returns B’s nonce (encrypted by B’s public key) back to B.
Here is the man-in-the-middle attack to the simplified protocol:
(1A) A → E: {Na,A}Ke (A wants to talk to E)
(1B) E → B: {Na,A}Kb (E wants to convince B that it is A)
(2B) B → E: {Na,Nb}Ka (B returns nonces encrypted by Ka)
(2A) E → A: {Na,Nb}Ka (E forwards the encrypted message to A)
(3A) A → E: {Nb}Ke (A confirms it is talking to E)
(3B) E → B: {Nb}Kb (E returns B’s nonce back)
The NuSMV source code (http://www.iis.sinica.edu.tw/~bywang/courses/ comp-logic/hw3-1.smv) contains a model for the Needham-Schroeder protocol. When the attack was found, a fix was proposed to prevent the attack:
(1) A → B: {Na,A}Kb
(2) B → A: {Na,Nb,B}Ka
(3) A → B: {Nb}Kb
In Step (2) of the Needham-Schroeder-Lowe protocol, B sends its identity along with the nonces back to A.
1
