{var%20f='http://v.t.sina.com.cn/share/share.php?appkey=1515056452',u=z||d.location,p=['&url=',e(u),'&title=',e(t||d.title),'&source=',e(r),'&sourceUrl=',e(l),'&content=',c||'gb2312','&pic=',e(p||'')].join('');function%20a(){if(!window.open([f,p].join(''),'mb',['toolbar=0,status=0,resizable=1,width=440,height=430,left=',(s.width-440)/2,',top=',(s.height-430)/2].join('')))u.href=[f,p].join('');};if(/Firefox/.test(navigator.userAgent))setTimeout(a,0);else%20a();})(screen,document,encodeURIComponent,'','','https://www.manongdao.com/data/attach/logo/logo.png', '推荐 够拽才男人 的问题《How to use NuSMV to witness the man-in-the-middle》','https://www.manongdao.com/q-942508.html','页面编码gb2312|utf-8默认gb2312'));){kind=link}
I have the following simplified public-key Needham-Schroeder protocol:
A → B: {Na, A} KbB → A: {Na, Nb} KaA → 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),
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:
- (1A)
A → E: {Na, A} Ke(Awants to talk toE) - (1B)
E → B: {Na, A} Kb(Ewants to convinceBthat it isA) - (2B)
B → E: {Na, Nb} Ka(Breturns nonces encrypted byKa) - (2A)
E → A: {Na, Nb} Ka(Eforwards the encrypted message toA) - (3A)
A → E: {Nb} Ke(Aconfirms it is talking toE) - (3B)
E → B: {Nb} Kb(EreturnsB’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(Bsends its identity along with the nonces back toA)A → B: {Nb} Kb
The questions are:
- How can I write an LTL formula and a NuSMV module
eveto model the attacker and witness the man-in-the middle attack? - 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!
(note: modeling and verifying the system you have in mind with some other tool (e.g.
Spinor theSTIATE Toolkit) would be much more simple.)Alice and Bob.
Here we model the type of
userthat behaves in a honest, transparent manner and that in your use-case can be instantiated as eitherAliceorBob.As a simplification, i hard-coded the fact that if the
userisAlicethen it will initiate the protocol by trying to contact the other entity.The inputs
my_nonce,my_idandmy_keydefine auser's identity, whereasother_keyandother_idrepresent the publicly available information about the otheruserwe want to get in touch with. Inputsin_1,in_2andin_kare just like in your code example, whereasin_3is reserved for exchanging the third value used in the patched version of the protocol.A
usercan be in one of five states:IDLE: initial state,Alicewill initiate the protocol whereasBobwaits for some request.WAIT_RESPONSE: whenAlicewaits to a response to herrequestWAIT_CONFIRMATION: whenBobwaits to a confirmation to hisresponseOK: whenAliceandBobhandshake 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.We add a very simple
mainmodule and a simpleCTLproperty to check thatAliceandBobbehave in the expected way and are able to complete the handshake in normal circumstances:The output is the following one:
Alice, Bob and Eve.
In order to model our attack scenario, we first need to model the
attacker. This is very similar toAliceandBob, only that it has doubleinputsandoutputsso that it can communicate with bothAliceandBobat the same time.Its design is very similar to that of
AliceandBob, so I won't spend many words on it. As a simplification, i removed any error checking on theattacker, 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.Again, we add a very simple
mainmodule and a simpleCTLproperty to check thatEveis able to successfully attackAliceandBob.. at the end of it,Alicethinks to be talking toEve(as it is) andBobthinks to be talking withAlicewhen it's truly talking withEve.The output follows:
Patched Alice, Bob and Eve.
Luckily, I already sneaked the patched version of
AliceandBobin 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 newmainthat combinesAlice,BobandEvetogether:The output follows:
The first property confirms that the attack fails and the handshake is not completed for neither
AlicenorBobbecauseEvedoes not fulfil it. The second property shows how the attack is attempted and how it fails in practice.