How to use NuSMV to witness the man-in-the-middle attack (Needham-Schroeder protocol)?

Question

I have the following 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 main-in-the-middle attack to the above 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)

I hope that when the attack was found, a fix was proposed to prevent the attack (B sends its identity along with the nonces back to A):

1. A → B: {Na, A} Kb
2. B → A: {Na, Nb, B} Ka (B sends its identity along with the nonces back to A)
3. A → B: {Nb} Kb

The questions are:

1. How can I write an LTL formula and a NuSMV module eve to model the attacker and witness the man-in-the middle attack?
2. How to prevents the attack?

The process of alice(A):

MODULE alice (in0, in1, inkey, out0, out1, outkey)
VAR
    st : { request, wait, attack, finish };
    nonce : { NONE, Na, Nb, Ne };
ASSIGN
    init (st) := request;
    next (st) := case
        st = request                        : wait;
        st = wait & in0 = Na & inkey = Ka   : attack;
        st = attack                         : finish;
        TRUE                                : st;
    esac;

    init (nonce) := NONE;
    next (nonce) := case
        st = wait & in0 = Na & inkey = Ka : in1;
        TRUE                              : nonce;
    esac;

    init (out0) := NONE;
    next (out0) := case
        st = request : Na;
        st = attack  : nonce;
        TRUE         : out0;
    esac;

    init (out1) := NOONE;
    next (out1) := case
        st = request : Ia;
        st = attack  : NOONE;
        TRUE         : out1;
    esac;

    init (outkey) := NOKEY;
    next (outkey) := case
        st = request : { Kb };
        TRUE         : outkey;
    esac;
FAIRNESS running;

The process of bob(B):

MODULE bob (in0, in1, inkey, out0, out1, outkey)
VAR
    st : { wait, receive, confirm, done };
    nonce : { NONE, Na, Nb, Ne };
    other : { NOONE, Ia, Ib, Ie };
ASSIGN
    init (st) := wait;
    next (st) := case
        st = wait & in0 = Na & in1 = Ia & inkey = Kb       : receive;
        st = wait & in0 = Ne & in1 = Ie & inkey = Kb       : receive;
        st = receive                                       : confirm;
        st = confirm & in0 = Nb & in1 = NOONE & inkey = Kb : done;
        TRUE                                               : st;
    esac;

    init (nonce) := NONE;
    next (nonce) := case
        st = wait & in0 = Na & in1 = Ia & inkey = Kb : in0;
        st = wait & in0 = Ne & in1 = Ie & inkey = Kb : in0;
        TRUE                                         : nonce;
    esac;

    init (other) := NOONE;
    next (other) := case
        st = wait & in0 = Na & in1 = Ia & inkey = Kb : in1;
        st = wait & in0 = Ne & in1 = Ie & inkey = Kb : in1;
        TRUE                                         : other;
    esac;

    init (out0) := NONE;
    next (out0) := case
        st = confirm : nonce;
        TRUE         : out0;
    esac;

    init (out1) := NONE;
    next (out1) := case
        st = confirm : Nb;
        TRUE         : out1;
    esac;

    init (outkey) := NOKEY;
    next (outkey) := case
        st = confirm & other = Ia : Ka;
        st = confirm & other = Ie : Ke;
        TRUE                      : outkey;
    esac;
FAIRNESS running;

The process of main:

MODULE main 
VAR
    a_in0 : { NONE, Na, Nb, Ne };
    a_in1 : { NONE, Na, Nb, Ne };
    a_out0 : { NONE, Na, Nb, Ne };
    a_out1 : { NOONE, Ia, Ib, Ie };
    a_inkey : { NOKEY, Ka, Kb, Ke };
    a_outkey : { NOKEY, Ka, Kb, Ke };
    a : process alice (a_in0, a_in1, a_inkey, a_out0, a_out1, a_outkey);
    b : process bob (a_out0, a_out1, a_outkey, a_in0, a_in1, a_inkey);
FAIRNESS running;

LTLSPEC F (a.st = finish & b.st = done)

Thanks a lot!

Answer 1

(note: modeling and verifying the system you have in mind with some other tool (e.g. Spin or the STIATE Toolkit) would be much more simple.)

---

Alice and Bob.

Here we model the type of user that behaves in a honest, transparent manner and that in your use-case can be instantiated as either Alice or Bob.

As a simplification, i hard-coded the fact that if the user is Alice then it will initiate the protocol by trying to contact the other entity.

The inputs my_nonce, my_id and my_key define a user's identity, whereas other_key and other_id represent the publicly available information about the other user we want to get in touch with. Inputs in_1, in_2 and in_k are just like in your code example, whereas in_3 is reserved for exchanging the third value used in the patched version of the protocol.

A user can be in one of five states:

• IDLE: initial state, Alice will initiate the protocol whereas Bob waits for some request.
• WAIT_RESPONSE: when Alice waits to a response to her request
• WAIT_CONFIRMATION: when Bob waits to a confirmation to his response
• OK: when Alice and Bob handshake has been successful
• ERROR: when something goes wrong in the handshake (e.g. unexpected inputs)

A user can perform one of the following actions:

• SEND_REQUEST: {Na, IA} Kb
• SEND_RESPONSE: {Na, Nb} Ka
• SEND_CONFIRMATION: {Nb} Kb

As a simplification, similarly to your own model, I made output values persistent along several transitions instead of putting them back immediately to NONE. In this way, I don't have to add extra variables to keep track of input values before they are resetted.

MODULE user(patched, my_nonce, my_id, my_key, other_key, other_id, in_1, in_2, in_3, in_k)
VAR
    state  : { IDLE, WAIT_RESPONSE, WAIT_CONFIRMATION, OK, ERROR };
    action : { NONE, SEND_REQUEST, SEND_RESPONSE, SEND_CONFIRMATION };
    out_1  : { NONE, NA, NB, NE, IA, IB, IE };
    out_2  : { NONE, NA, NB, NE, IA, IB, IE };
    out_3  : { NONE, NA, NB, NE, IA, IB, IE };
    out_k  : { NONE, KA, KB, KE };

INIT
    state = IDLE & action = NONE & out_1 = NONE
    & out_2 = NONE & out_3 = NONE & out_k = NONE;

-- protocol actions defining outputs
TRANS
    next(action) = SEND_REQUEST -> (
        next(out_1) = my_nonce & next(out_2) = my_id &
        next(out_3) = NONE     & next(out_k) = other_key
    );

TRANS
    ((next(action) = SEND_RESPONSE) & patched) -> (
        next(out_1) = in_1     & next(out_2) = my_nonce &
        next(out_3) = my_id    & next(out_k) = other_key
    );

TRANS
    ((next(action) = SEND_RESPONSE) & !patched) -> (
        next(out_1) = in_1     & next(out_2) = my_nonce &
        next(out_3) = NONE     & next(out_k) = other_key
    );

TRANS
    next(action) = SEND_CONFIRMATION -> (
        next(out_1) = in_2     & next(out_2) = NONE &
        next(out_3) = NONE     & next(out_k) = other_key
    );

-- outputs stabilization: easier modeling
TRANS
    next(action) = NONE -> (
        next(out_1) = out_1    & next(out_2) = out_2 &
        next(out_3) = out_3    & next(out_k) = out_k
    );

-- protocol life-cycle
TRANS
case
    -- protocol: end-positions
    (action = NONE &
     state = ERROR)
                        : next(action) = NONE &
                          next(state) = ERROR;
    (action = NONE &
     state = OK)
                        : next(action) = NONE &
                          next(state) = OK;

    -- protocol: send request
    (action = NONE &
     state = IDLE &
     my_id = IA)
                        : next(action) = SEND_REQUEST &
                          next(state) = WAIT_RESPONSE;

    -- protocol: handle request
    (action = NONE &
     state = IDLE &
     in_k = my_key)
                        : next(action) = SEND_RESPONSE &
                          next(state) = WAIT_CONFIRMATION;

    -- protocol: handle response
    -- without patch
    (action = NONE &
     state = WAIT_RESPONSE &
     in_k = my_key &
     in_1 = my_nonce &
     !patched)
                        : next(action) = SEND_CONFIRMATION &
                          next(state) = OK;
    -- with patch
    (action = NONE &
     state = WAIT_RESPONSE &
     in_k = my_key &
     in_1 = my_nonce &
     in_3 = other_id &
     patched)
                        : next(action) = SEND_CONFIRMATION &
                          next(state) = OK;

    -- protocol: handle confirmation
    (action = NONE &
     state = WAIT_CONFIRMATION &
     in_k = my_key &
     in_1 = my_nonce)
                        : next(action) = NONE &
                          next(state) = OK;

    -- protocol: no change state while performing action
    (action != NONE)
                        : next(action) = NONE &
                          next(state) = state;

    -- protocol: no state change if no valid input
    (action = NONE &
     in_k != my_key)
                        : next(action) = NONE &
                          next(state) = state;

    -- sink error condition for malformed inputs
    TRUE
                        : next(action) = NONE &
                          next(state) = ERROR;
esac;

We add a very simple main module and a simple CTL property to check that Alice and Bob behave in the expected way and are able to complete the handshake in normal circumstances:

MODULE main
VAR
    a1 : process user(FALSE, NA, IA, KA, KB, IB, b1.out_1, b1.out_2, b1.out_3, b1.out_k);
    b1 : process user(FALSE, NB, IB, KB, KA, IA, a1.out_1, a1.out_2, a1.out_3, a1.out_k);

FAIRNESS running;


CTLSPEC ! EF (a1.state = OK & b1.state = OK);

The output is the following one:

NuSMV > reset; read_model -i ns01.smv ; go ; check_property             
...
-- specification !(EF (a1.state = OK & b1.state = OK))  is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample 
Trace Type: Counterexample 
  -> State: 1.1 <-
    a1.state = IDLE
    a1.action = NONE
    a1.out_1 = NONE
    a1.out_2 = NONE
    a1.out_3 = NONE
    a1.out_k = NONE
    b1.state = IDLE
    b1.action = NONE
    b1.out_1 = NONE
    b1.out_2 = NONE
    b1.out_3 = NONE
    b1.out_k = NONE
  -> Input: 1.2 <-
    _process_selector_ = main
    running = TRUE
    b1.running = FALSE
    a1.running = FALSE
  -> State: 1.2 <-
    a1.state = WAIT_RESPONSE
    a1.action = SEND_REQUEST
    a1.out_1 = NA
    a1.out_2 = IA
    a1.out_k = KB
  -> Input: 1.3 <-
  -> State: 1.3 <-
    a1.action = NONE
    b1.state = WAIT_CONFIRMATION
    b1.action = SEND_RESPONSE
    b1.out_1 = NA
    b1.out_2 = NB
    b1.out_k = KA
  -> Input: 1.4 <-
  -> State: 1.4 <-
    a1.state = OK
    a1.action = SEND_CONFIRMATION
    a1.out_1 = NB
    a1.out_2 = NONE
    b1.action = NONE
  -> Input: 1.5 <-
  -> State: 1.5 <-
    a1.action = NONE
    b1.state = OK

---

Alice, Bob and Eve.

In order to model our attack scenario, we first need to model the attacker. This is very similar to Alice and Bob, only that it has double inputs and outputs so that it can communicate with both Alice and Bob at the same time.

Its design is very similar to that of Alice and Bob, so I won't spend many words on it. As a simplification, i removed any error checking on the attacker, since it does not actually have any meaningful reason to fail in the use-case scenario being considered. Not doing so would complicate the code for no good reason.

MODULE attacker(my_nonce, my_id, my_key, a_key, b_key,
    ain_1, ain_2, ain_3, ain_k,
    bin_1, bin_2, bin_3, bin_k)
VAR
    state  : { IDLE, WAIT_RESPONSE, WAIT_CONFIRMATION, OK, ERROR };
    action : { NONE, SEND_REQUEST, SEND_RESPONSE, SEND_CONFIRMATION };
    aout_1  : { NONE, NA, NB, NE, IA, IB, IE };
    aout_2  : { NONE, NA, NB, NE, IA, IB, IE };
    aout_3  : { NONE, NA, NB, NE, IA, IB, IE };
    aout_k  : { NONE, KA, KB, KE };
    bout_1  : { NONE, NA, NB, NE, IA, IB, IE };
    bout_2  : { NONE, NA, NB, NE, IA, IB, IE };
    bout_3  : { NONE, NA, NB, NE, IA, IB, IE };
    bout_k  : { NONE, KA, KB, KE };

INIT
    state = IDLE & action = NONE &
        aout_1 = NONE & aout_2 = NONE & aout_3 = NONE & aout_k = NONE &
        bout_1 = NONE & bout_2 = NONE & bout_3 = NONE & bout_k = NONE;

-- protocol actions defining outputs
TRANS
    -- attacker: forward A secrets to B
    next(action) = SEND_REQUEST -> (
        next(aout_1) = NONE    & next(aout_2) = NONE  &
        next(aout_3) = NONE    & next(aout_k) = NONE  &
        next(bout_1) = ain_1   & next(bout_2) = ain_2 &
        next(bout_3) = ain_3   & next(bout_k) = b_key
    );

TRANS
    -- attacker: forward B response to A (cannot be unencripted)
    next(action) = SEND_RESPONSE -> (
        next(aout_1) = bin_1   & next(aout_2) = bin_2 &
        next(aout_3) = bin_3   & next(aout_k) = bin_k &
        next(bout_1) = NONE    & next(bout_2) = NONE  &
        next(bout_3) = NONE    & next(bout_k) = NONE
    );

TRANS
    -- attacker: send confirmation to B
    next(action) = SEND_CONFIRMATION -> (
        next(aout_1) = NONE    & next(aout_2) = NONE &
        next(aout_3) = NONE    & next(aout_k) = NONE &
        next(bout_1) = ain_1   & next(bout_2) = NONE &
        next(bout_3) = NONE    & next(bout_k) = b_key
    );

-- outputs stabilization: easier modeling
TRANS
    next(action) = NONE -> (
        next(aout_1) = aout_1  & next(aout_2) = aout_2 &
        next(aout_3) = aout_3  & next(aout_k) = aout_k &
        next(bout_1) = bout_1  & next(bout_2) = bout_2 &
        next(bout_3) = bout_3  & next(bout_k) = bout_k
    );

-- attack life-cycle
TRANS
case
    -- attack: end-positions
    (action = NONE &
     state = ERROR)
                        : next(action) = NONE &
                          next(state) = ERROR;
    (action = NONE &
     state = OK)
                        : next(action) = NONE &
                          next(state) = OK;

    -- attack: handle request, send forged request
    (action = NONE &
     state = IDLE &
     ain_k = my_key)
                        : next(action) = SEND_REQUEST &
                          next(state) = WAIT_RESPONSE;

    -- attack: handle response, forward undecryptable response
    (action = NONE &
     state = WAIT_RESPONSE &
     bin_k = a_key)
                        : next(action) = SEND_RESPONSE &
                          next(state) = WAIT_CONFIRMATION;

    -- attack: handle confirmation, send confirmation
    (action = NONE &
     state = WAIT_CONFIRMATION &
     ain_k = my_key)
                        : next(action) = SEND_CONFIRMATION &
                          next(state) = OK;

    -- attack: simple catch-all control no error checking
    TRUE
                        : next(action) = NONE &
                          next(state) = state;
esac;

Again, we add a very simple main module and a simple CTL property to check that Eve is able to successfully attack Alice and Bob.. at the end of it, Alice thinks to be talking to Eve (as it is) and Bob thinks to be talking with Alice when it's truly talking with Eve.

MODULE main
VAR
    a2 : process user(FALSE, NA, IA, KA, KE, IE, e2.aout_1, e2.aout_2, e2.aout_3, e2.aout_k);
    b2 : process user(FALSE, NB, IB, KB, KA, IA, e2.bout_1, e2.bout_2, e2.bout_3, e2.bout_k);
    e2 : process attacker(NE, IE, KE, KA, KB,
                          a2.out_1, a2.out_2, a2.out_3, a2.out_k,
                          b2.out_1, b2.out_2, b2.out_3, b2.out_k);

FAIRNESS running;


CTLSPEC ! EF (a2.state = OK & b2.state = OK & e2.state = OK);

The output follows:

NuSMV > reset; read_model -i ns02.smv ; go ; check_property
...
-- specification !(EF ((a2.state = OK & b2.state = OK) & e2.state = OK))  is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample 
Trace Type: Counterexample 
  -> State: 1.1 <-
    a2.state = IDLE
    a2.action = NONE
    a2.out_1 = NONE
    a2.out_2 = NONE
    a2.out_3 = NONE
    a2.out_k = NONE
    b2.state = IDLE
    b2.action = NONE
    b2.out_1 = NONE
    b2.out_2 = NONE
    b2.out_3 = NONE
    b2.out_k = NONE
    e2.state = IDLE
    e2.action = NONE
    e2.aout_1 = NONE
    e2.aout_2 = NONE
    e2.aout_3 = NONE
    e2.aout_k = NONE
    e2.bout_1 = NONE
    e2.bout_2 = NONE
    e2.bout_3 = NONE
    e2.bout_k = NONE
  -> Input: 1.2 <-
    _process_selector_ = main
    running = TRUE
    e2.running = FALSE
    b2.running = FALSE
    a2.running = FALSE
  -> State: 1.2 <-
    a2.state = WAIT_RESPONSE
    a2.action = SEND_REQUEST
    a2.out_1 = NA
    a2.out_2 = IA
    a2.out_k = KE
  -> Input: 1.3 <-
  -> State: 1.3 <-
    a2.action = NONE
    e2.state = WAIT_RESPONSE
    e2.action = SEND_REQUEST
    e2.bout_1 = NA
    e2.bout_2 = IA
    e2.bout_k = KB
  -> Input: 1.4 <-
  -> State: 1.4 <-
    b2.state = WAIT_CONFIRMATION
    b2.action = SEND_RESPONSE
    b2.out_1 = NA
    b2.out_2 = NB
    b2.out_k = KA
    e2.action = NONE
  -> Input: 1.5 <-
  -> State: 1.5 <-
    b2.action = NONE
    e2.state = WAIT_CONFIRMATION
    e2.action = SEND_RESPONSE
    e2.aout_1 = NA
    e2.aout_2 = NB
    e2.aout_k = KA
    e2.bout_1 = NONE
    e2.bout_2 = NONE
    e2.bout_k = NONE
  -> Input: 1.6 <-
  -> State: 1.6 <-
    a2.state = OK
    a2.action = SEND_CONFIRMATION
    a2.out_1 = NB
    a2.out_2 = NONE
    e2.action = NONE
  -> Input: 1.7 <-
  -> State: 1.7 <-
    a2.action = NONE
    e2.state = OK
    e2.action = SEND_CONFIRMATION
    e2.aout_1 = NONE
    e2.aout_2 = NONE
    e2.aout_k = NONE
    e2.bout_1 = NB
    e2.bout_k = KB
  -> Input: 1.8 <-
  -> State: 1.8 <-
    b2.state = OK
    e2.action = NONE

---

Patched Alice, Bob and Eve.

Luckily, I already sneaked the patched version of Alice and Bob in the code that I have already shown. So, all that it remains to do is to check that the patch meets the desired behavior by writing a new main that combines Alice, Bob and Eve together:

MODULE main
VAR
    a3 : process user(TRUE, NA, IA, KA, KE, IE, e3.aout_1, e3.aout_2, e3.aout_3, e3.aout_k);
    b3 : process user(TRUE, NB, IB, KB, KA, IA, e3.bout_1, e3.bout_2, e3.bout_3, e3.bout_k);
    e3 : process attacker(NE, IE, KE, KA, KB,
                          a3.out_1, a3.out_2, a3.out_3, a3.out_k,
                          b3.out_1, b3.out_2, b3.out_3, b3.out_k);

FAIRNESS running;


CTLSPEC ! EF (a3.state = OK & b3.state = OK & e3.state = OK);
CTLSPEC ! EF (a3.state = ERROR & b3.state = ERROR);

The output follows:

NuSMV > reset; read_model -i ns03.smv ; go ; check_property             
...
-- specification !(EF ((a3.state = OK & b3.state = OK) & e3.state = OK))  is true
-- specification !(EF (a3.state = ERROR & b3.state = ERROR))  is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample 
Trace Type: Counterexample 
  -> State: 1.1 <-
    a3.state = IDLE
    a3.action = NONE
    a3.out_1 = NONE
    a3.out_2 = NONE
    a3.out_3 = NONE
    a3.out_k = NONE
    b3.state = IDLE
    b3.action = NONE
    b3.out_1 = NONE
    b3.out_2 = NONE
    b3.out_3 = NONE
    b3.out_k = NONE
    e3.state = IDLE
    e3.action = NONE
    e3.aout_1 = NONE
    e3.aout_2 = NONE
    e3.aout_3 = NONE
    e3.aout_k = NONE
    e3.bout_1 = NONE
    e3.bout_2 = NONE
    e3.bout_3 = NONE
    e3.bout_k = NONE
  -> Input: 1.2 <-
    _process_selector_ = main
    running = TRUE
    e3.running = FALSE
    b3.running = FALSE
    a3.running = FALSE
  -> State: 1.2 <-
    a3.state = WAIT_RESPONSE
    a3.action = SEND_REQUEST
    a3.out_1 = NA
    a3.out_2 = IA
    a3.out_k = KE
  -> Input: 1.3 <-
  -> State: 1.3 <-
    a3.action = NONE
    e3.state = WAIT_RESPONSE
    e3.action = SEND_REQUEST
    e3.bout_1 = NA
    e3.bout_2 = IA
    e3.bout_k = KB
  -> Input: 1.4 <-
  -> State: 1.4 <-
    b3.state = WAIT_CONFIRMATION
    b3.action = SEND_RESPONSE
    b3.out_1 = NA
    b3.out_2 = NB
    b3.out_3 = IB
    b3.out_k = KA
    e3.action = NONE
  -> Input: 1.5 <-
  -> State: 1.5 <-
    b3.action = NONE
    e3.state = WAIT_CONFIRMATION
    e3.action = SEND_RESPONSE
    e3.aout_1 = NA
    e3.aout_2 = NB
    e3.aout_3 = IB
    e3.aout_k = KA
    e3.bout_1 = NONE
    e3.bout_2 = NONE
    e3.bout_k = NONE
  -> Input: 1.6 <-
  -> State: 1.6 <-
    a3.state = ERROR
    e3.action = NONE
  -> Input: 1.7 <-
  -> State: 1.7 <-
    e3.state = OK
    e3.action = SEND_CONFIRMATION
    e3.aout_1 = NONE
    e3.aout_2 = NONE
    e3.aout_3 = NONE
    e3.aout_k = NONE
    e3.bout_1 = NA
    e3.bout_k = KB
  -> Input: 1.8 <-
  -> State: 1.8 <-a
    b3.state = ERROR
    e3.action = NONE

The first property confirms that the attack fails and the handshake is not completed for neither Alice nor Bob because Eve does not fulfil it. The second property shows how the attack is attempted and how it fails in practice.