I have the following simplified public-key Needham-Schroeder protocol:
A → B: {Na, A} KbB → A: {Na, Nb} KaA → B: {Nb} Kbwhere 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),
Ainitiates the protocol by sending a nonce and its identity (encrypted byB’s public key) toB. Using its private key,Bdeciphers the message and getsA’s identity.At Step (2),
BsendsA’s and its nonces (encrypted byA’s public key) back toA. Using its private key,Adecodes the message and checks its nonce is returned.At Step (3),
AreturnsB’s nonce (encrypted byB’s public key) back toB.
Here is the main-in-the-middle attack to the above simplified protocol:
A → E: {Na, A} Ke (A wants to talk to E) E → B: {Na, A} Kb (E wants to convince B that it is A)B → E: {Na, Nb} Ka (B returns nonces encrypted by Ka) E → A: {Na, Nb} Ka (E forwards the encrypted message to A) A → E: {Nb} Ke (A confirms it is talking to E)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):
A → B: {Na, A} KbB → A: {Na, Nb, B} Ka (B sends its identity along with the nonces back to A)A → B: {Nb} KbThe questions are:
eve to model the attacker and witness the man-in-the middle 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!
(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 requestWAIT_CONFIRMATION: when Bob waits to a confirmation to his responseOK: when Alice and Bob handshake has been successfulERROR: when something goes wrong in the handshake (e.g. unexpected inputs)A user can perform one of the following actions:
SEND_REQUEST: {Na, IA} KbSEND_RESPONSE: {Na, Nb} KaSEND_CONFIRMATION: {Nb} KbAs 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.