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 colset TIME = 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