Attack traces in Section 5 (Others can be obtained by running the formal models in the Benchmark)
iRobot RTE trace1
$ userA 'pressButton' deviceB
$ userA 'callAPI:setKey' deviceB | 'key0.0'
$ userA 'callAPI:bind' cloudA | (deviceB ; 'key0.0')
$ userC 'approaches' deviceB
$ userC 'pressButton' deviceB
$ userC 'callAPI:setKey' deviceB | 'SecretC'
$ userC 'leaves' deviceB
$ userC 'callAPI:reset' cloudA | (deviceB ; 'SecretC')
iRobot RTE trace2
$ userA 'pressButton' deviceB
$ userA 'callAPI:setKey' deviceB | 'key0.0'
$ userA 'callAPI:bind' cloudA | (deviceB ; 'key0.0')
$ userC 'approaches' deviceB
$ userC 'pressButton' deviceB
$ userC 'callAPI:getKey' deviceB
$ userC 'leaves' deviceB
$ userC 'callAPI:reset' cloudA | (deviceB ; 'key0.0')
Philips RTE
$ userA 'pressButton' deviceB
$ userA 'callAPI:getKey' cloudA | deviceB
$ userA 'callAPI:bind' cloudA | (deviceB ; 'key2357136044)
$ userC 'approaches' deviceB
$ userC 'pressButton' deviceB
$ userC 'callAPI:getKey' cloudA | deviceB
$ userC 'leaves' deviceB
$ userC 'callAPI:join' cloudA | (userA ; 'key2546248239)
August RTE
$ userA 'leaves' deviceB
$ userC 'approaches' deviceB
$ userC 'pressButton' deviceB
$ userC 'leaves' deviceB
$ userC 'callAPI:bind' cloudA | (deviceB ; 'secret')
$ userC 'callAPI:reset' cloudA | deviceB
Broadlink RTE
$ userA 'pressButton' deviceB
$ userC 'callAPI:invite' cloudA | userA
$ userC 'callAPI:kick' cloudA | userA
$ userC 'approaches' deviceB
$ userC 'pressButton' deviceB
$ userC 'callAPI:getKey' deviceB
$ userC 'callAPI:lock' deviceB | 'KeyB'362609376e
$ userC 'callAPI:invite' cloudA | userA
$ userC 'callAPI:kick' cloudA | userA
$ userC 'leaves' deviceB
Tplink RTE
$ userC 'approaches' deviceB
$ userC 'pressButton' deviceB
$ userC 'callAPI:setKey' deviceB | 'secretC'
$ userC 'pressButton' deviceB
$ userC 'leaves' deviceB
$ userA 'callAPI:discover' deviceB
Tuya CAC
$ userA 'invite' cloudA | userC
$ userC 'callAPI:getKey' cloudA | deviceB
$ userA 'kick' cloudA | userC
$ userC 'callAPI:toggle' deviceB | 'secretOfB'
Aqara INT
$ userA 'callAPI:invite' cloudA | userC
$ userC 'callAPI:openWindow' cloudA | deviceB
$ userC 'callAPI:bind' deviceB | 'KeyA'2357136044
$ userC 'callAPI:invite' cloudA | userA
$ userA 'callAPI:openWindow' cloudA | deviceB
$ userA 'callAPI:kick' cloudA | userC
$ userC 'callAPI:toggle' deviceB
$ userA 'callAPI:invite' cloudA | userC
$ userC 'callAPI:kick' cloudA | userA
CloudEdge RTE
$ userA 'pressButton' deviceB
$ userC 'pressButton' deviceD
$ userA 'callAPI:setKey' deviceB | 'phoneMacA'
$ userA 'callAPI:discover' deviceB
$ userC 'callAPI:setKey' deviceD | 'phoneMacA'
$ userC 'pressButton' deviceD
$ userC 'callAPI:discover' deviceD