*** variable declarations
vars DeviceY : Device .
vars UserX OwnerX : User .
vars KeyA KeyB : Qid .
*** State dynamic rules
eq < DeviceY | 'pressed' : false , ... > $ UserX 'pressButton' DeviceY
-> < DeviceY | 'pressed' : true , ... > .
eq < DeviceY | 'pressed' : true , 'key' : nils , ... > $ UserX 'callAPI:setKey' DeviceY | KeyA
-> < DeviceY | 'pressed' : false , 'key' : KeyA , ... > $ DeviceY 'callAPI:setKey' cloudA | KeyA .
eq < DeviceY | 'pressed' : true , 'key' : KeyB , ... > $ UserX 'callAPI:setKey' DeviceY | KeyA
-> < DeviceY | 'pressed' : false , 'key' : KeyA , ... > $ DeviceY 'callAPI:setKey' cloudA | KeyA .
eq < cloudA | DeviceY : ('bdKey' : KeyB , ... ) , ... > $ DeviceY 'callAPI:setKey' cloudA | KeyA
-> < cloudA | DeviceY : ('bdKey' : KeyA , ... ) , ... > .
eq < cloudA | DeviceY : ('bdKey' : KeyA , 'owner' : nils , ... ) , ... > $ UserX 'callAPI:bind' cloudA | DeviceY ; KeyA
-> < cloudA | DeviceY : ('bdKey' : KeyA , 'owner' : UserX , ... ) , ... > .
eq < DeviceY | 'pressed' : true , 'key' : KeyA , ... > $ UserX 'callAPI:getKey' DeviceY
-> < DeviceY | 'pressed' : false , 'key' : KeyA , ... > $ DeviceY 'sendKey' UserX | KeyA .
eq < UserX | 'key' : KeyB , ... > $ DeviceY 'sendKey' UserX | KeyA
-> < UserX | 'key' : KeyA , ... > .
eq < cloudA | DeviceY : ('bdKey' : KeyA , 'owner' : OwnerX , ... ) , ... > $ UserX 'callAPI:reset' cloudA | DeviceY ; KeyA
-> < cloudA | DeviceY : ('bdKey' : nils , 'owner' : nils , ... ) , ... > .
eq < UserX | 'localTo' : nils , ... > $ UserX 'approach' DeviceY
-> < UserX | 'localTo' : DeviceY , ... > .
eq < UserX | 'localTo' : DeviceY , ... > $ UserX 'leave' DeviceY
-> < UserX | 'localTo' : nils , ... > .
*** event template
ev1(UserX,DeviceY) = $ UserX 'approach' DeviceY .
ev2(UserX,DeviceY) = $ UserX 'leave' DeviceY .
ev3(UserX,DeviceY) = $ UserX 'pressButton' DeviceY .
ev4(UserX,DeviceY,KeyA) = $ UserX 'callAPI:setKey' DeviceY | (KeyA) .
ev5(UserX,DeviceY) = $ UserX 'callAPI:getKey' DeviceY .
ev6(UserX,DeviceY,KeyA) = $ UserX 'callAPI:bind' cloudA | ((DeviceY) ; KeyA) .
ev7(UserX,DeviceY,KeyA) = $ UserX 'callAPI:reset' cloudA | ((DeviceY) ; KeyA) .
*** Event generation rules
rl < UserX | 'localTo' : DeviceY , ... > < DeviceY | ... > --> ev3(UserX, DeviceY) .
rl < UserX | 'localTo' : DeviceY , ... > < DeviceY | ... > --> ev5(UserX, DeviceY) .
rl < UserX | 'localTo' : DeviceY , 'key' : KeyA , ... > < DeviceY | ... > --> ev4(UserX, DeviceY, KeyA) .
rl < UserX | 'localTo' : DeviceY , ... > < DeviceY | ... > --> ev2(UserX, DeviceY) .
rl < UserX | 'localTo' : nils , ... > < DeviceY | ... > --> ev1(UserX, DeviceY) .
rl < UserX | 'key' : KeyA , ... > < cloudA | DeviceY : ( ... ) ,... > --> ev6(UserX, DeviceY, KeyA) .
rl < UserX | 'key' : KeyA , ... > < cloudA | DeviceY : ( ... ) ,... > --> ev7(UserX, DeviceY, KeyA) .
var E : Event .
var S : Soup .
*** generated propositions
ceq E @ S |= uaPressButton = true if sd(E) == sd(ev3(userA, deviceB)) .
ceq E @ S |= uaCallSetKey = true if sd(E) == sd(ev4(userA, deviceB, '')) .
ceq E @ S |= uaCallBind = true if sd(E) == sd(ev6(userA, deviceB, '')) .
ceq E @ S |= uaResetDeviceB = true if sd(E) == sd(ev7(userA, deviceB, '')) .
eq E @ S < cloudA | deviceB : ('owner' : userA , ...) , ... > |= uaOwnerDeviceB = true .
ceq E @ S |= ucPerformOperation = true if subject(E) == userC .
eq E @ S < userC | 'localDevice' : deviceB , ... > |= ucLocalDeviceB = true .
eq E @ S < cloudA | deviceB : ('owner' : userC , ...) , ... > |= ucOwnerDeviceB = true .
*** properties
eq spec =
[](uaPressButton -> O (ucPerformOperation W (uaCallSetKey \/ uaResetDeviceB)))
/\ [](uaCallSetKey -> O (ucPerformOperation W (uaCallBind \/ uaResetDeviceB)))
/\ [](uaResetDeviceB -> O (ucPerformOperation W uaPressButton))
/\ [](uaOwnerDeviceB -> ~ O (uaPressButton \/ uaCallSetKey \/ uaCallBind \/ uaResetDeviceB))
/\ [](O uaResetDeviceB -> (uaCallBind /\ ~ uaOwnerDeviceB))
/\ <> (~ ucLocalDeviceB /\ ~ ucOwnerDeviceB /\ O (~ ucLocalDeviceB /\ ucOwnerDeviceB))
typedef Slot{
int data;
bool occupy = false;
}
inline slot_set(s,i){
atomic{
s.data = i;
s.occupy = true
}
}
inline slot_empty(s){
atomic{
s.data = 0;
s.occupy = false;
}
}
inline slot_get(s,d){
atomic{
if :: s.occupy ->
d = s.data[0]
:: else -> printf("[-] can not get from an empty slot\n")
fi
}
}
int idx=0;//global loop counter
#define OFF 0
#define ON 1
#define ACTION mtype
#define PRINCIPAL mtype
#define BIND_R_MAX 3
int time=1;
inline elapse(n){
time = time + n;
}
inline elapse1(){
time = time + 1;
}
ACTION = {Press,Transfer,Get,Reset};
PRINCIPAL = {userA_,userC_,deviceB_,cloud_};
typedef Event{
ACTION action;
int sender;//sender id
int data
}
typedef Prin{
Slot database;
chan event = [0] of {Event};//can not store
PRINCIPAL name;
int id;
bool iflocal = false;
}
Prin prins[4];
#define userA prins[0]
#define userC prins[1]
#define deviceB prins[2]
#define cloud prins[3]
#define isUser(id) (id==0 || id==1)
/*###Binding related###*/
typedef BindRelation{
PRINCIPAL name;
PRINCIPAL name2;
int key;
}
typedef BindSet{
BindRelation arr[BIND_R_MAX];
bool occupy[BIND_R_MAX];
}
BindSet bind_relations;
inline bind(prinA,prinB){
atomic{
bool success = false;
for (idx : 0 .. BIND_R_MAX-1) {
if :: bind_relations.occupy[idx] == false ->
success = true;
bind_relations.arr[idx].name = prinA.name;
bind_relations.arr[idx].name2 = prinB.name;
bind_relations.occupy[idx] = true;
break
:: else -> skip;
fi
}
if :: !success ->
printf("Set Full!\n");
:: else ->
skip;
fi
}
}
inline reset(prinA,prinB){
atomic{
bool success = false;
for (idx : 0 .. BIND_R_MAX-1) {
if :: bind_relations.occupy[idx] == true ->
if :: ((bind_relations.arr[idx].name == prinA.name && bind_relations.arr[idx].name2 == prinB.name)\
|| (bind_relations.arr[idx].name2 == prinA.name && bind_relations.arr[idx].name == prinB.name)) ->
success = true;
bind_relations.arr[idx].name = 0;
bind_relations.arr[idx].name2 = 0;
bind_relations.occupy[idx] = false;
break;
:: else -> skip;
fi
:: else -> skip;
fi
}
if :: !success ->
//printf("No this item!reset(%e,%e)\n",prinA.name,prinB.name);
skip
:: else ->
skip
fi
}
}
inline resetAll(prin){
atomic{
reset(prins[0],prin);
reset(prins[1],prin);
reset(prins[2],prin);
reset(prins[3],prin);
}
}
inline BIND(pa,pb,rst){
atomic{
rst = false;
for (idx : 0 .. BIND_R_MAX-1) {
if :: bind_relations.occupy[idx] == true ->
if :: bind_relations.arr[idx].name == pa.name ->
if :: bind_relations.arr[idx].name2 == pb.name ->
rst = true;
break;
:: else -> skip;
fi
:: bind_relations.arr[idx].name == pb.name ->
if :: bind_relations.arr[idx].name2 == pa.name ->
rst = true;
break;
:: else -> skip;
fi
:: else -> skip;
fi
:: else -> skip;
fi
}
}
}
inline HasOwner(p,rst){
atomic{
rst = false;
for (idx : 0 .. BIND_R_MAX-1) {
if :: bind_relations.occupy[idx] == true ->
if :: bind_relations.arr[idx].name == p.name || bind_relations.arr[idx].name2 == p.name ->
rst = true;
break;
:: else -> skip;
fi
:: else -> skip;
fi
}
}
}
inline happen(sender,action,receiver,data){
atomic{
receiver.event!action(sender.id,data);
elapse1();
}
}
inline happen0(sender,action,receiver){
atomic{
printf("* %e %e %e at time %d\n",
sender.name,action,receiver.name,time);
receiver.event!action(sender.id,0);
elapse1();
}
}
inline happen1(sender,action,receiver,data){
atomic{
printf("* %e %e %e with %d at time %d\n",sender.name,action,receiver.name,data,time);
happen(sender,action,receiver,data);
}
}
inline happen2(sender,action,receiver){
//if sender has data, then use it, else use his id+10
int happpen2localdata;
atomic{
if :: sender.database.occupy ->
slot_get(sender.database,happpen2localdata);
happen1(sender,action,receiver,happpen2localdata)
:: else ->
happpen2localdata = 10+sender.id;
happen1(sender,action,receiver,happpen2localdata)
fi
}
}
inline leaves(p){
printf("* %e leaves at time %d\n",p.name,time);
p.iflocal = false
}
inline comes(p){
printf("* %e comes at time %d\n",p.name,time);
p.iflocal = true
}
inline prelude(){
atomic{
userA.name = userA_;
userA.id = 0;
userA.iflocal = true;
userC.name = userC_;
userC.id = 1;
userC.iflocal = false;
deviceB.name = deviceB_;
deviceB.id = 2;
deviceB.iflocal = true;
cloud.name = cloud_;
cloud.id = 3
}
}
chan finished = [0] of {int};
chan uabinded = [0] of {int};
bool stop = false;
inline user_rule_i(user){
atomic{//////
do :: user.event?evt ->
if :: (evt.action == Transfer) ->
slot_set(user.database,evt.data);
:: else -> skip;
fi
od
}/////
}
proctype user_rule(){
Event evt;
int data;
user_rule_i(userC);
user_rule_i(userA);
}
proctype device_rule (){
Event evt;
int data;
int t;
#define Delay 3
atomic{//////////
do :: deviceB.event?evt->
if :: (prins[evt.sender].iflocal) ->
if :: (evt.action == Press)->
t = time;
:: evt.action == Transfer ->
if :: t && time <= t+Delay ->
slot_set(deviceB.database,evt.data);
evt.sender = deviceB.id;
cloud.event!evt;
:: else -> skip
fi
:: evt.action == Get->
if :: t && time <= t+Delay && deviceB.database.occupy ->
slot_get(deviceB.database,data);
prins[evt.sender].event!Transfer(deviceB.id,data);
:: else -> skip
fi
:: else -> skip
fi
:: else -> skip
fi
od
}///////////
}
proctype cloud_rule(){
Event evt,evt2;
int data;
bool hasOwner = false;
atomic{//////////
do :: cloud.event?evt ->
if :: evt.action == Transfer ->
if :: evt.sender == deviceB.id ->
slot_set(cloud.database,evt.data)
:: isUser(evt.sender) ->
if :: cloud.database.occupy ->
slot_get(cloud.database,data);
HasOwner(deviceB,hasOwner);
if :: data == evt.data && !hasOwner ->
bind(deviceB,prins[evt.sender])
printf("###bind %e and %e###\n",deviceB.name,prins[evt.sender].name);
:: else -> skip
fi
:: else
fi
:: else -> skip
fi
:: evt.action == Reset ->
if :: cloud.database.occupy ->
slot_get(cloud.database,data);
if :: data == evt.data ->
resetAll(deviceB)
printf("###%e reset by %e###",deviceB.name,prins[evt.sender].name);
:: else -> skip
fi
:: else -> skip
fi
:: else -> skip
fi
od
}/////
}
D_proctype normal_user_action(){
happen0(userA,Press,deviceB);
happen2(userA,Transfer,deviceB);
atomic{
happen2(userA,Transfer,cloud);
finished!1;
}
}
D_proctype attack_trace2(){
happen0(userA,Press,deviceB);
happen2(userA,Transfer,deviceB);
happen2(userA,Transfer,cloud);
comes(userC);
happen0(userC,Press,deviceB);
happen2(userC,Transfer,deviceB);
leaves(userC);
happen2(userC,Reset,cloud);
}
#define ATTACKER_CNT 5
proctype attacker_action(){
int cnt;
bool p = false;
atomic{
do :: cnt < ATTACKER_CNT ->
BIND(userC,deviceB,p)
if :: p -> break;
:: else -> skip;
fi
if
:: happen0(userC,Press,deviceB)
:: happen2(userC,Transfer,deviceB)
:: happen0(userC,Get,deviceB)
:: happen2(userC,Transfer,cloud)
:: happen2(userC,Reset,cloud)
:: !userC.iflocal -> comes(userC)
:: userC.iflocal -> leaves(userC)
fi
cnt = cnt + 1;
:: else -> break
od
finished!2;
}
}
proctype always_attacker_nobind_checker(){
bool q=false;
do :: !stop ->
atomic{
BIND(userC,deviceB,q);
assert(!q)
}
:: else -> break;
od
}
proctype userBind_detect(){
bool uabind = false;
do :: !stop ->
atomic{
BIND(userA,deviceB,uabind);
if :: uabind ->
uabinded!1;
break;
:: else -> skip;
fi
}
od
}
proctype reset_checker(){
int i;
bool uabind = false;
uabinded?i;
do :: !stop ->
atomic{
BIND(userA,deviceB,uabind);
assert(uabind)
}
od
}
inline test(){
atomic{
run user_rule();
run device_rule();
run cloud_rule();
}
run attack_trace2()
}
inline verify(){
atomic{
run user_rule();
run device_rule();
run cloud_rule();
run normal_user_action();
run attacker_action();
run always_attacker_nobind_checker();
run userBind_detect();
run reset_checker();
}
}
init{
prelude();
verify();
}
//pan -E -e