-- -- -- IEEE 802.16e 3-way TEK Handshake Protocol -- Vijay Chauhan & Srinivas Inguva -- -- -- Parameters -- const BS_SEND_M1: 6; MS_RECV_M1: 5; MS_SEND_M2: 6; BS_RECV_M2: 5; BS_SEND_M3: 8; MS_RECV_M3: 8; INT_INTERCEPT: 4; INT_COMPOSE: 4; INT_SEND: 4; MS_WAIT_RES_COST: 11; INT_RES_THRESHOLD: 8; INT_THRESHOLD: 16; MS_DONE_COST: 19; BS_DONE_COST: 19; DOS_ENABLED: true; PN_ENABLED: true; --PN_ENABLED: false; -- If PN_ENABLED is set to "false", we expect an invariant violation -- representing a DoS NumMS: 1; NumBS: 1; NumIntruders: 1; NetworkSize: 10; MaxSessions: 1; MaxIntruderActions: 5; MaxIntruderCosts: 200; MaxCost: 200; MaxNonce: 30; MaxPN: 100; -- What intruder can remember MaxKnowledge: 10; type MSId: scalarset(NumMS); BSId: scalarset(NumBS); IntruderId: scalarset(NumIntruders); AgentId: union{MSId, BSId, IntruderId}; Nonce: 0..MaxNonce; PN: -1..MaxPN; SessionId: 0..MaxSessions; -- Key modeling AK: record peer1: AgentId; --MS peer2: AgentId; --BS end; -- -- Message Modeling -- MessageType: enum { M_1, M_2, M_3 }; MAC: record ak: AK; MSnonce: Nonce; BSnonce: Nonce; TEKnonce: Nonce; mtype: MessageType; end; Message: record source: AgentId; dest: AgentId; mtype: MessageType; BSnonce: Nonce; MSnonce: Nonce; TEKnonce: Nonce; address: AgentId; pn: PN; mac: MAC; end; -- MS MSStates: enum { MS_WAIT_CLG, MS_WAIT_RES, MS_DONE }; MSSessions: record state: MSStates; ak: AK; costs: 0..MaxCost; intCosts: 0..MaxIntruderCosts; end; MSAssociations: record session: MSSessions; sid: SessionId; peer: AgentId; MSnonce: Nonce; BSnonce: Nonce; TEKnonce: Nonce; lastKnownPN: PN; end; MS: record associations: array[AgentId] of MSAssociations; end; -- BS BSStates: enum { BS_START, BS_WAIT_REQ, BS_DONE }; BSSessions: record state: BSStates; ak: AK; costs: 0..MaxCost; intCosts: 0..MaxIntruderCosts; end; BSAssociations: record session: BSSessions; sid: SessionId; peer: AgentId; BSnonce: Nonce; MSnonce: Nonce; TEKnonce: Nonce; end; BS: record associations: array[AgentId] of BSAssociations; end; -- Intruder Intruder: record nonces: multiset[MaxKnowledge] of Nonce; TEKnonces: multiset[MaxKnowledge] of Nonce; macs: multiset[MaxKnowledge] of MAC; messages: multiset[MaxKnowledge] of Message; end; -- Other variables var net: multiset[NetworkSize] of Message; ms: array[MSId] of MS; bs: array[BSId] of BS; int: array[IntruderId] of Intruder; actionCount: 0..MaxIntruderActions; nextNonce: Nonce; nextPN: PN; -- Generate a fresh nonce function freshNonce(): Nonce; var tmp: Nonce; begin if (nextNonce = MaxNonce) then error "Run out of nonces!" end; tmp := nextNonce; nextNonce := nextNonce + 1; return tmp; end; -- Generate a fresh PN function freshPN(): PN; var tmp: PN; begin if (nextPN = MaxPN) then error "Run out of PNs!" end; tmp := nextPN; nextPN := nextPN + 1; return tmp; end; -- Use AK for peers. function useAK(peer1: AgentId; peer2: AgentId) : AK; var tmp: AK; begin tmp.peer1 := peer1; tmp.peer2 := peer2; return tmp; end; -- Compute MAC function computeMAC(msg: Message; ak: AK) : MAC; var tmp: MAC; begin tmp.ak := ak; tmp.BSnonce := msg.BSnonce; if (msg.mtype = M_2 | msg.mtype = M_3) then tmp.MSnonce := msg.MSnonce; end; if (msg.mtype = M_3) then tmp.TEKnonce := msg.TEKnonce; end; tmp.mtype := msg.mtype; return tmp; end; -- -- Comparison functions -- function akEqual(key1: AK; key2: AK): boolean; begin return ((key1.peer1 = key2.peer1) & (key1.peer2 = key2.peer2)) | ((key1.peer2 = key2.peer1) & (key1.peer1 = key2.peer2)) ; end; function macEqual(mac1: MAC; mac2: MAC): boolean; begin if (!akEqual(mac1.ak, mac2.ak)) then return false; end; if (!(mac1.mtype = mac2.mtype)) then return false; end; if (!(mac1.BSnonce = mac2.BSnonce)) then return false; end; if ((mac1.mtype = M_2 | mac1.mtype = M_3) & !(mac1.MSnonce = mac2.MSnonce)) then return false; end; if ((mac1.mtype = M_3) & !(mac1.TEKnonce = mac2.TEKnonce)) then return false; end; return true; end; ----------- -- Rules -- ----------- -- -- BS -- -- BS sends message 1 ruleset i: BSId do ruleset j: AgentId do rule 20 "BS sends Message 1 to associated agents" !ismember(j, BSId) & -- no message to BSs !ismember(j, IntruderId) & -- no message to Intruders bs[i].associations[j].sid < MaxSessions & multisetcount(l:net, true) < NetworkSize & (bs[i].associations[j].session.state = BS_START | bs[i].associations[j].session.state = BS_DONE) --(bs[i].associations[j].session.state = BS_START) ==> var outM: Message; -- outgoing message outAK: AK; begin undefine outM; outM.source := i; outM.dest := j; outM.mtype := M_1; outM.BSnonce := freshNonce(); outM.address := i; outM.pn := freshPN(); outAK := useAK(i, j); outM.mac := computeMAC(outM, outAK); multisetadd(outM, net); -- store the states bs[i].associations[j].peer := j; bs[i].associations[j].session.ak := useAK(i, j); bs[i].associations[j].BSnonce := outM.BSnonce; bs[i].associations[j].session.state := BS_WAIT_REQ; bs[i].associations[j].sid := bs[i].associations[j].sid + 1; bs[i].associations[j].session.costs := BS_SEND_M1; end; end; end; -- For a MS. -- Receive message 1. Send message 2. -- ruleset i: MSId do choose j: net do rule 20 "MS processes message 1" net[j].dest = i & net[j].mtype = M_1 & ms[i].associations[net[j].address].sid < MaxSessions & -- (ms[i].associations[net[j].address].session.state = MS_WAIT_CLG | ms[i].associations[net[j].address].session.state = MS_DONE) (ms[i].associations[net[j].address].session.state = MS_WAIT_CLG) ==> var outM: Message; -- outgoing message inM: Message; mac: MAC; outAK: AK; begin inM := net[j]; -- Remove processed message multisetremove (j, net); outAK := useAK(i, inM.address); mac := computeMAC(inM, outAK); --MAC CHECK if (macEqual(mac, inM.mac) & (!PN_ENABLED | (inM.pn > ms[i].associations[inM.address].lastKnownPN))) then -- Store MSNonce ms[i].associations[inM.address].peer := inM.source; ms[i].associations[inM.address].session.ak := useAK(i, inM.address); ms[i].associations[inM.address].BSnonce := inM.BSnonce; ms[i].associations[inM.address].MSnonce := freshNonce(); -- Send message M_2 undefine outM; outM.source := i; outM.dest := inM.address; outM.mtype := M_2; outM.BSnonce := ms[i].associations[inM.address].BSnonce; outM.MSnonce := ms[i].associations[inM.address].MSnonce; outM.address := i; outM.mac := computeMAC(outM, outAK); multisetadd(outM, net); -- Change state to MS_WAIT_RES ms[i].associations[inM.address].session.state := MS_WAIT_RES; if (!DOS_ENABLED) then ms[i].associations[inM.address].sid := ms[i].associations[inM.address].sid + 1; end; ms[i].associations[inM.address].session.costs := ms[i].associations[inM.address].session.costs + MS_RECV_M1 + MS_SEND_M2; if (!PN_ENABLED) then ms[i].associations[inM.address].lastKnownPN := inM.pn; end; end; end; endchoose; end; -- For BS -- Receive message 2. Send message 3. ruleset i: BSId do choose j: net do rule 20 "BS processes message 2" net[j].dest = i & net[j].mtype = M_2 & -- Allow the BS to accept rekey messages (DOS_ENABLED | bs[i].associations[net[j].address].session.state = BS_WAIT_REQ) ==> var outM: Message; -- outgoing message inM: Message; mac: MAC; outAK: AK; begin inM := net[j]; -- Remove processed message multisetremove(j, net); outAK := useAK(i, inM.address); mac := computeMAC(inM, outAK); --MAC CHECK if (macEqual(mac, inM.mac)) then -- Send message M_3 undefine outM; outM.source := i; outM.dest := inM.address; outM.mtype := M_3; outM.BSnonce := inM.BSnonce; outM.MSnonce := inM.MSnonce; outM.TEKnonce := freshNonce(); outM.address := i; outM.mac := computeMAC(outM,outAK); multisetadd(outM, net); -- update states. bs[i].associations[inM.address].peer := inM.source; bs[i].associations[inM.address].MSnonce := inM.MSnonce; bs[i].associations[inM.address].TEKnonce := outM.TEKnonce; bs[i].associations[inM.address].session.state := BS_DONE; --bs[i].associations[inM.address].sid := bs[i].associations[inM.address].sid + 1; if (!DOS_ENABLED) then bs[i].associations[inM.address].session.costs := bs[i].associations[inM.address].session.costs + BS_RECV_M2 + BS_SEND_M3; end; end; --MAC CHECK end; end; endchoose; end; -- For MS -- Receive message 3, done.. -- ruleset i: MSId do choose j: net do rule 20 "MS processes message 3" net[j].dest = i & net[j].mtype = M_3 & ms[i].associations[net[j].address].sid < MaxSessions & ms[i].associations[net[j].address].session.state = MS_WAIT_RES ==> var inM: Message; mac: MAC; outAK: AK; begin inM := net[j]; -- Remove processed message multisetremove (j, net); outAK := useAK(i, inM.address); mac := computeMAC(inM, outAK); --MAC CHECK if (macEqual(mac, inM.mac)) then -- Update states. ms[i].associations[inM.address].peer := inM.source; ms[i].associations[inM.address].TEKnonce := inM.TEKnonce; ms[i].associations[inM.address].session.state := MS_DONE; ms[i].associations[inM.address].session.costs := ms[i].associations[inM.address].session.costs + MS_RECV_M3; end; --MAC CHECK end; end; endchoose; end; -- ruleset i: MSId do ruleset j: AgentId do rule 291 "MS transitions from MS_DONE->MS_WAIT_CLG" ms[i].associations[j].session.state = MS_DONE ==> begin ms[i].associations[j].session.state := MS_WAIT_CLG; if (!DOS_ENABLED) then ms[i].associations[j].session.costs := 0; ms[i].associations[j].session.intCosts := 0; end; end; end; end; /* ruleset i: BSId do ruleset j: AgentId do rule 291 "BS transitions from BS_DONE->BS_START" bs[i].associations[j].session.state = BS_DONE ==> begin bs[i].associations[j].session.state := BS_START; bs[i].associations[j].session.costs := 0; end; end; end; */ -- Intruder -- Intercept a message ruleset i: IntruderId do choose j: net do rule 10 "Intruders intercept a message" actionCount < MaxIntruderActions & multisetcount(l:net, true) > 0 & !ismember(net[j].source, IntruderId) -- do not intercept messages from Intruders ==> var inM: Message; begin alias msg: int[i].messages; nc: int[i].nonces; teknc: int[i].TEKnonces; mc: int[i].macs; do inM := net[j]; -- Remove processed message. multisetremove (j, net); -- store the whole message for replay if (multisetcount(l:msg, msg[l].mtype = inM.mtype & (msg[l].BSnonce = inM.BSnonce) & (msg[l].mtype = M_1 | msg[l].MSnonce = inM.MSnonce) & (msg[l].mtype = M_1 | msg[l].mtype = M_2 | msg[l].TEKnonce = inM.TEKnonce) & (msg[l].address = inM.address) & (macEqual(msg[l].mac, inM.mac))) = 0) then undefine inM.source; undefine inM.dest; multisetadd(inM, int[i].messages); end; -- store BSnonces if (multisetcount(n:nc, nc[n] = inM.BSnonce) = 0) then multisetadd(inM.BSnonce, int[i].nonces); end; -- store MSnonces if (multisetcount(n:nc, (inM.mtype = M_1 | nc[n] = inM.MSnonce)) = 0) then multisetadd(inM.MSnonce, int[i].nonces); end; -- put "#####################DEBUG 1\n"; -- put inM.mtype; -- store TEKnonces if (multisetcount(n:teknc, (inM.mtype = M_1 | inM.mtype = M_2 | teknc[n] = inM.TEKnonce)) = 0) then if (inM.mtype = M_3) then multisetadd(inM.TEKnonce, int[i].TEKnonces); end; end; -- put "#####################DEBUG 2\n"; -- store macs if (multisetcount(m:mc, macEqual(mc[m], inM.mac)) = 0) then multisetadd(inM.mac, int[i].macs); end; -- put "#####################DEBUG 3\n"; actionCount:= actionCount+1; endalias; end; endchoose; end; -- Replay a complete message ruleset i: IntruderId do choose j: int[i].messages do ruleset k: AgentId do rule 30 "Messages Replayed to every agent" actionCount < MaxIntruderActions & i != k & multisetcount(l:net, true) < NetworkSize ==> var outM: Message; -- outgoing message begin undefine outM; outM := int[i].messages[j]; outM.source := i; outM.dest := k; multisetadd (outM, net); -- multisetremove (j, int[i].messages); actionCount:= actionCount+1; if (isMember(k, MSId) & isMember(outM.address, BSId)) then ms[k].associations[outM.address].session.intCosts :=ms[k].associations[outM.address].session.intCosts + INT_INTERCEPT + INT_SEND; end; end; end; endchoose; end; -- Intruder compose message 1 from known nonces and send to agents ruleset i: IntruderId do ruleset j: MSId do ruleset k: BSId do choose n: int[i].nonces do choose m: int[i].macs do rule 30 "Intruders compose message 1 and send to agents" actionCount < MaxIntruderActions & multisetcount(l:net, true) < NetworkSize ==> var outM: Message; -- outgoing message begin undefine outM; outM.source := i; outM.dest := j; outM.mtype := M_1; outM.BSnonce := int[i].nonces[n]; outM.address := k; outM.mac := int[i].macs[m]; outM.pn := -1; multisetadd(outM, net); actionCount:= actionCount+1; ms[j].associations[k].session.intCosts := ms[j].associations[k].session.intCosts + INT_INTERCEPT + INT_COMPOSE; end; endchoose; endchoose; end; end; end; /* -- Intruder compose message 2 from known nonces and send to agents ruleset i: IntruderId do ruleset j: MSId do ruleset k: BSId do choose n: int[i].nonces do choose p: int[i].nonces do choose m: int[i].macs do rule 31 "Intruders compose message 2 and send to agents" actionCount < MaxIntruderActions & multisetcount(l:net, true) < NetworkSize ==> var outM: Message; -- outgoing message begin undefine outM; outM.source := i; outM.dest := k; outM.mtype := M_2; outM.BSnonce := int[i].nonces[n]; outM.MSnonce := int[i].nonces[p]; outM.address := j; outM.mac := int[i].macs[m]; multisetadd(outM, net); actionCount:= actionCount+1; end; endchoose; endchoose; endchoose; end; end; end; -- Intruder compose message 3 from known nonces and send to agents ruleset i: IntruderId do ruleset j: MSId do ruleset k: BSId do choose n: int[i].nonces do choose p: int[i].nonces do choose q: int[i].TEKnonces do choose m: int[i].macs do rule 31 "Intruders compose message 2 and send to agents" actionCount < MaxIntruderActions & multisetcount(l:net, true) < NetworkSize ==> var outM: Message; -- outgoing message begin undefine outM; outM.source := i; outM.dest := j; outM.mtype := M_2; outM.BSnonce := int[i].nonces[n]; outM.MSnonce := int[i].nonces[p]; outM.TEKnonce := int[i].TEKnonces[q]; outM.address := k; outM.mac := int[i].macs[m]; multisetadd(outM, net); actionCount:= actionCount+1; end; endchoose; endchoose; endchoose; endchoose; end; end; end; */ -- -- Start state -- startstate var begin -- Initialize variables nextNonce := 0; nextPN := 0; actionCount := 0; -- Initialize network undefine net; -- Initialize MSs undefine ms; for i:MSId do for j:AgentId do ms[i].associations[j].session.state := MS_WAIT_CLG; ms[i].associations[j].sid := 0; ms[i].associations[j].session.ak := useAK(i, j); ms[i].associations[j].peer := j; ms[i].associations[j].session.costs := 0; ms[i].associations[j].session.intCosts := 0; ms[i].associations[j].lastKnownPN := 0; end; end; -- Initalize BS undefine bs; for i:BSId do for j:AgentId do bs[i].associations[j].session.state := BS_START; bs[i].associations[j].sid := 0; bs[i].associations[j].session.ak := useAK(i, j); bs[i].associations[j].peer := j; bs[i].associations[j].session.costs := 0; end; end; -- Initialize intruders undefine int; for i:IntruderId do undefine int[i].messages; end; end; -- -- If MS is done, so is BS invariant "If MS is DONE => BS is DONE" forall i: BSId do forall j: MSId do (ms[j].associations[i].session.state = MS_DONE & (ms[j].associations[i].sid = bs[i].associations[j].sid)) -> (bs[i].associations[j].session.state = BS_DONE) end end; -- -- If MS is waiting for CLG, BS can't have finished the handshake invariant "If MS is WAIT_CLG => BS is in START/WAIT_REQ" forall i: BSId do forall j: MSId do (ms[j].associations[i].session.state = MS_WAIT_CLG & (ms[j].associations[i].sid = bs[i].associations[j].sid)) -> (!bs[i].associations[j].session.state = BS_DONE) end end; -- -- If MS is waiting for RES then BS must have sent a CLG invariant "If MS is WAIT_RES => BS is in WAIT_REQ/DONE" forall i: BSId do forall j: MSId do (ms[j].associations[i].session.state = MS_WAIT_RES & (ms[j].associations[i].sid = bs[i].associations[j].sid)) -> (!bs[i].associations[j].session.state = BS_START) end end; -- invariant "When MS/BS complete handshake they share a TEK" forall i: BSId do forall j: MSId do (ms[j].associations[i].session.state = MS_DONE & (ms[j].associations[i].sid = bs[i].associations[j].sid) & (bs[i].associations[j].session.state = BS_DONE)) -> (bs[i].associations[j].TEKnonce = ms[j].associations[i].TEKnonce) end end; /* -- If MS is waiting for RES then costs == MS_WAIT_RES_COST invariant "If MS is WAIT_RES => costs = MS_WAIT_RES_COST" forall i: BSId do forall j: MSId do (ms[j].associations[i].session.state = MS_WAIT_RES) -> (ms[j].associations[i].session.costs <= MS_WAIT_RES_COST) end end; */ /* -- If MS is waiting for RES then costs == MS_WAIT_RES_COST and intCosts > threshold invariant "If MS is WAIT_RES => costs = MS_WAIT_RES_COST and intCosts > threshold" forall i: BSId do forall j: MSId do (ms[j].associations[i].session.state = MS_WAIT_RES) -> (ms[j].associations[i].session.costs <= MS_WAIT_RES_COST | ms[j].associations[i].session.intCosts > INT_RES_THRESHOLD) end end; */ /* -- If MS is waiting done then costs == MS_DONE_COST invariant "If MS is DONE => costs = MS_DONE_COST" forall i: BSId do forall j: MSId do (ms[j].associations[i].session.state = MS_DONE) -> (ms[j].associations[i].session.costs <= MS_DONE_COST) end end; */ -- If MS is waiting done then costs == MS_DONE_COST invariant "If MS is DONE => costs = MS_DONE_COST and intCosts > threshold" forall i: BSId do forall j: MSId do (ms[j].associations[i].session.state = MS_DONE) -> (ms[j].associations[i].session.costs <= MS_DONE_COST | ms[j].associations[i].session.intCosts > INT_THRESHOLD) end end; /* -- If BS is waiting for REQ then costs == BS_DONE_COST invariant "If BS is WAIT_REQ => costs = BS_DONE_COST" forall i: BSId do forall j: MSId do (bs[i].associations[j].session.state = BS_WAIT_REQ) -> (bs[i].associations[j].session.costs <= BS_DONE_COST) end end; */