Standard priorities val P_HIGH = 100; val P_HIGH = 100; val P_NORMAL = 1000; val P_NORMAL = 1000; val P_LOW = 10000; val P_LOW = 10000; Standard declarations MSG colset MSG = string; DEVID colset DEVID = string; DEVKEY colset DEVKEY = string; DEVPAIR DEVID DEVKEY colset DEVPAIR = product DEVID * DEVKEY; DHKEY colset DHKEY = string; ENCMSG DHKEY MSG colset ENCMSG = product DHKEY * MSG; SERVENCMSG DEVKEY ENCMSG colset SERVENCMSG = product DEVKEY * ENCMSG; SERVENCMSG2 DEVKEY MSG colset SERVENCMSG2 = product DEVKEY * MSG; SERVENCMSG3 DEVKEY MSG ENCMSG colset SERVENCMSG3 = product DEVKEY * MSG * ENCMSG; SERVMSG DEVID SERVENCMSG colset SERVMSG = product DEVID * SERVENCMSG; DEVIDxENCMSG DEVID ENCMSG colset DEVIDxENCMSG = product DEVID * ENCMSG; UNIT colset UNIT = unit; BOOL INT INTINF colset INTINF = intinf; STRING TIME REAL colset REAL = real; DEVID devid var devid: DEVID; MSG msg msg1 msg2 var msg,msg1,msg2: MSG; DHKEY dhkey dhkeyI1 dhkeyI2 var dhkey,dhkeyI1,dhkeyI2 : DHKEY; DEVKEY devkey var devkey : DEVKEY; DEVPAIR devpair var devpair : DEVPAIR; ENCMSG encmsg var encmsg : ENCMSG; ENCMSG encmsg_from_server encmsg_from_dev encmsg_from_gw var encmsg_from_server,encmsg_from_dev,encmsg_from_gw: ENCMSG; BOOL boolean var boolean : BOOL; SERVENCMSG servencmsg var servencmsg : SERVENCMSG; SERVENCMSG2 servencmsg2 var servencmsg2 : SERVENCMSG2; SERVENCMSG3 servencmsg3 var servencmsg3 : SERVENCMSG3; SERVMSG servmsg var servmsg : SERVMSG; STRING str var str : STRING; M1 ENCMSG DEV_Km DEVKEY 1`"DEVKEY0001" M2 SERVMSG MITM_not_checked MSG 1`"DETECT_MITM_NONCE" M3 DEVIDxENCMSG Received_DevID DEVID 1`"IOTDEV0001" DevID DEVID 1`"IOTDEV0001" M4 ENCMSG MITM_TEST_RESULT STRING c6 MSG 1`"GW_IS_REAL" M5 SERVENCMSG3 M0_DEV DHKEY M0_GW DHKEY MITM_MESSAGE MSG 1`"DETECT_MITM" c10 DEVPAIR 1`("IOTDEV0001","DEVKEY0001")++ 2`("IOTDEV0002","DEVKEY0002") FakeDevice STRING GW_IS_FAKE MSG GW_IS_REAL MSG GW_VALIDATION_EXPECTED_MESSAGE MSG 1`"GW_IS_REAL" Intruder DH Key Distribution DHKEY 1`"mitm_dhkey" Evesdrop MSG Dev_Key DHKEY GW_Key DHKEY M1_I ENCMSG MITM Perform DH input (dhkey) output (dhkeyI1,dhkeyI2) action let val res1 = "dhkey01" val res2 = "dhkey01" in (res1,res2) end IoT_Device IoT_GW IoT_Server Decrypt input (dhkey,encmsg) output (msg) action let val res = #2(encmsg) in (res) end Encrypt input (dhkey,msg) output (encmsg) action let val result = (dhkey,msg) in (result) end dhkeyI2 dhkeyI1 dhkey dhkey msg msg encmsg dhkey encmsg dhkeyI2 dhkeyI1 b5 SERVMSG recvMsg SERVENCMSG3 Dev_Km1 DEVKEY b4 SERVENCMSG Start_MITM_CHECK_1 UNIT DEV_Ks DHKEY b1 ENCMSG b2 MSG b3 ENCMSG M1_I ENCMSG M0_DEV DHKEY GW_VALIDATION_EXPECTED_MESSAGE MSG 1`"GW_IS_REAL" M5 SERVENCMSG3 DevID DEVID 1`"IOTDEV0001" DEV_Km DEVKEY 1`"DEVKEY0001" M2 SERVMSG MITM_MESSAGE MSG 1`"DETECT_MITM" GW_IS_REAL MSG GW_IS_FAKE MSG ConcatDevIDandEncryptedMsg input (devid,servencmsg) output (servmsg) action let val res = (devid,servencmsg) in (res) end Send Server Recv Server Encrypt_Km input (devkey,encmsg) output (servencmsg) action let val res = (devkey, encmsg) in (res) end Decrypt [dhkey= #1(encmsg)] input (dhkey,encmsg) output (msg) action let val res = #2(encmsg) in (res) end get DH DEV Recv Check_MITM_msg [msg2=substring(msg,0,11)] falseCheck [devkey<> #1(servencmsg3) orelse msg<> #2(servencmsg3)] input (servencmsg3) output (msg2) action let val res = #2(servencmsg3) in (res) end DecryptServEncMsg2 [devkey= #1(servencmsg3) andalso msg2= #2(servencmsg3)] input (servencmsg3) output (msg) action let val res = #2(servencmsg3) in (res) end Check_MITM_failcase [msg2<>substring(msg1,0,11)] input (msg1,msg2) output (msg) action let val res = (msg1) in (res) end dhkey 1`() dhkey servmsg devkey servencmsg3 1`() servencmsg3 msg encmsg msg devkey encmsg encmsg servencmsg devkey servencmsg3 encmsg servencmsg servmsg encmsg dhkey msg servencmsg3 devid devkey servmsg msg2 msg2 msg msg2 msg1 msg2 msg a4 ENCMSG a5 ENCMSG a2 ENCMSG GW_Ks DHKEY a1 ENCMSG M1 ENCMSG Received_DevID DEVID 1`"IOTDEV0001" MITM_not_checked MSG 1`"DETECT_MITM" M3 DEVIDxENCMSG M4 ENCMSG M0_GW DHKEY MITM_TEST_RESULT STRING get DH GW Send Compare_MITM_Test_Msgs input (encmsg,encmsg_from_server) output (str) action let val orig_key = #1(encmsg) val orig_msg = #2(encmsg) val recv_key = #1(encmsg_from_server) val recv_msg = #2(encmsg_from_server) in if orig_key=recv_key andalso orig_msg=recv_msg then "PASSED" else "FAILED" end RecvFromServer SetupSSL_with_Server Encrypt input (dhkey,msg) output (encmsg) action let val result = (dhkey,msg) in (result) end encmsg encmsg encmsg encmsg dhkey dhkey encmsg_from_server encmsg encmsg devid (devid,encmsg) encmsg dhkey str msg encmsg encmsg c2 ENCMSG c12 DEVPAIR c11 DEVKEY c8 DEVID c9 SERVENCMSG c1 SERVMSG c4 ENCMSG c7 SERVENCMSG3 c5 DEVPAIR c3 DEVID c10 DEVPAIR 1`("IOTDEV0001","DEVKEY0001")++ 2`("IOTDEV0002","DEVKEY0002") M5 SERVENCMSG3 M3 DEVIDxENCMSG M4 ENCMSG c6 MSG 1`"GW_IS_REAL" FakeDevice STRING M2 SERVMSG dh_enc_msg_GW ENCMSG dh_enc_msg_dev ENCMSG gw_encmsg ENCMSG CopiedFakeDevice STRING ServEncMSG_Decrypt input (servencmsg, devkey) output (encmsg,str) action let val res = #2(servencmsg) in if devkey= #1(servencmsg) then (res,"0") else (("0","0"),"WRONG DEVKEY") end GW_RequestMatch [devid= #1(devpair)] findTheKey [devid= #1(devpair)] input (devpair) output (devkey) action let val res_devkey= #2(devpair) in (res_devkey) end Disassemble SERVMSG input (servmsg) output (devid, servencmsg) action let val res_devid = #1(servmsg) val res_servencmsg = #2(servmsg) in (res_devid, res_servencmsg) end RecvFromDev Wait_for_SSLConnection Send2GW_DevMsg SendRequestMatch_Msg Encrypt_K_DevID input (devpair,msg,encmsg,msg1) output (servencmsg3) action let val res_servencmsg3= (#2(devpair),msg,encmsg) in if msg1="MITM_DETECTED" then (#2(devpair),msg1,encmsg) else (res_servencmsg3) end compare_dh_enc_msgs input (encmsg_from_dev, encmsg_from_gw) output (msg1) action let val res = "MITM_DETECTED" in if encmsg_from_dev<> encmsg_from_gw then (res) else ("NO_MITM_DETECTED") end devid servencmsg3 devpair encmsg devpair devpair encmsg devkey servmsg encmsg devkey servencmsg devid servencmsg3 devid encmsg servmsg devpair servencmsg devid devpair servencmsg3 (devid,encmsg) encmsg msg if str<>"0" then str else "DEVICE AUTHENTICATED" servmsg encmsg encmsg encmsg_from_dev encmsg_from_gw msg1 encmsg encmsg msg1 msg1