------------------------------ MODULE TagJoin ------------------------------ (***************************************************************************) (* Joining a crew by invite, for a device with a button and no keyboard. *) (* *) (* A tag T starts with no crew. Its owner presses the button: T opens a *) (* *claim window* (60 s in the firmware) and, while it is open, advertises *) (* with a '+' in front of its name. The advert is a plain MeshCore *) (* advert: unencrypted, flooded, heard by anyone in range. *) (* *) (* Any device that hears a '+' advert shows "wants to join", and its user *) (* may send an INVITE: a direct message encrypted to T's public key that *) (* carries the inviter's crew passphrase. T applies an invite only while *) (* its window is open; the first applied invite sets T's crew and closes *) (* the window; anything later is ignored until the button is pressed *) (* again. Holding the button (8 s) forgets the crew, so T can be claimed *) (* again. *) (* *) (* Inviters. Each inviter is identified with its crew (one inviter per *) (* crew is enough: two members of the same crew send the same passphrase). *) (* `Attackers` is the subset of inviters that are not the owner's people. *) (* An attacker plays by the same rules as everyone else: it can invite *) (* only after hearing a '+' advert, and it cannot read anyone else's *) (* invite (those are encrypted to T's key), so an invite is simply a *) (* message addressed to T carrying the inviter's crew. *) (* *) (* Sessions. Every press opens a new window numbered by the press. With *) (* CheckSession = TRUE the '+' advert carries that number, an inviter puts *) (* the newest number it has heard into its invite, and T applies an invite *) (* only if the number matches the open window. With CheckSession = FALSE *) (* the model is the firmware as first built: adverts and invites carry no *) (* session, and any invite that lands while a window is open is applied. *) (* The session field is kept on every message either way, so that the *) (* history variable `stale` can say which window an invite was sent for. *) (* *) (* The medium is `air`, as in PosseBeacons: a growing set of transmitted *) (* messages, any of which may be delivered at any later time, any number *) (* of times, or never. That covers loss, delay, reordering, duplication *) (* and the flood relays at once. The window timer is a free *) (* nondeterministic `Expire`, unordered against every delivery. *) (* *) (* Abstracted away: the passphrase itself (the crew id stands for it), the *) (* crew channel T beacons on after joining (only members of that crew can *) (* see it, which is what makes the attacker case low-stakes), the 10 s *) (* advert cadence while claiming (one advert per window suffices under *) (* `air`), and the 1-byte wrap of a real session counter. *) (***************************************************************************) EXTENDS Naturals, FiniteSets CONSTANTS Inviters, \* devices in range that may invite; each is identified with its crew Attackers, \* the subset of Inviters that are not the owner's people NoCrew, \* the tag's crew before it is claimed MaxPresses, \* button presses that open a window (this is what bounds the model) CheckSession \* TRUE: the fixed design (advert carries a session, invite echoes it) ASSUME /\ Attackers \subseteq Inviters /\ NoCrew \notin Inviters /\ MaxPresses \in Nat \ {0} /\ CheckSession \in BOOLEAN Honest == Inviters \ Attackers Sessions == 1..MaxPresses Adverts == [kind: {"adv"}, session: Sessions] Invites == [kind: {"inv"}, from: Inviters, session: Sessions] Msgs == Adverts \cup Invites VARIABLES presses, \* windows opened so far; the newest window's session is `presses` window, \* 0 = closed, else the session of the open window crew, \* NoCrew, or the crew the tag has joined air, \* set of Msgs ever transmitted and still deliverable heard, \* heard[i]: newest session i has seen a '+' advert for (0 = none) invited, \* invited[i]: sessions i has sent an invite for (at most one each) \* ---- history variables, used only by the properties ---- joins, \* invites applied since the last press stale \* TRUE once an invite sent for one window was applied in another vars == <> Max(a, b) == IF a > b THEN a ELSE b TypeOK == /\ presses \in 0..MaxPresses /\ window \in 0..MaxPresses /\ crew \in {NoCrew} \cup Inviters /\ air \in SUBSET Msgs /\ heard \in [Inviters -> 0..MaxPresses] /\ invited \in [Inviters -> SUBSET Sessions] /\ joins \in Nat /\ stale \in BOOLEAN Init == /\ presses = 0 /\ window = 0 /\ crew = NoCrew /\ air = {} /\ heard = [i \in Inviters |-> 0] /\ invited = [i \in Inviters |-> {}] /\ joins = 0 /\ stale = FALSE (***************************************************************************) (* The owner presses the button on a tag with no crew: a new window opens *) (* (a press while one is open restarts it under a new session) and a '+' *) (* advert for it goes on the air. *) (***************************************************************************) Press == /\ crew = NoCrew /\ presses < MaxPresses /\ presses' = presses + 1 /\ window' = presses + 1 /\ air' = air \cup {[kind |-> "adv", session |-> presses + 1]} /\ joins' = 0 /\ UNCHANGED <> \* The 60 s timer runs out. Expire == /\ window # 0 /\ window' = 0 /\ UNCHANGED <> \* The owner holds the button for 8 s: crew forgotten, any window closed. Forget == /\ crew # NoCrew \/ window # 0 /\ crew' = NoCrew /\ window' = 0 /\ UNCHANGED <> (***************************************************************************) (* An inviter hears a '+' advert. Its peer record keeps the newest advert *) (* (the firmware drops adverts older than the one already held), so what *) (* it remembers is the highest session heard so far. *) (***************************************************************************) HearAdvert(i, m) == /\ m \in air /\ m.kind = "adv" /\ heard' = [heard EXCEPT ![i] = Max(@, m.session)] /\ UNCHANGED <> (***************************************************************************) (* The inviter's user presses "invite" on the device that wants to join. *) (* At most one invite per inviter per window it has heard of. The message *) (* is addressed to T and carries the inviter's crew; under CheckSession it *) (* also carries the session it saw in the advert. *) (***************************************************************************) Invite(i) == /\ heard[i] # 0 /\ heard[i] \notin invited[i] /\ invited' = [invited EXCEPT ![i] = @ \cup {heard[i]}] /\ air' = air \cup {[kind |-> "inv", from |-> i, session |-> heard[i]]} /\ UNCHANGED <> (***************************************************************************) (* An invite lands on T. Applied only while a window is open (and, in the *) (* fixed design, only if it names that window); applying it sets the crew *) (* and closes the window, so every later invite is dropped. *) (***************************************************************************) Deliver(m) == /\ m \in air /\ m.kind = "inv" /\ IF window # 0 /\ (~CheckSession \/ m.session = window) THEN /\ crew' = m.from /\ window' = 0 /\ joins' = joins + 1 /\ stale' = stale \/ (m.session # window) ELSE UNCHANGED <> /\ UNCHANGED <> Next == \/ Press \/ Expire \/ Forget \/ \E i \in Inviters, m \in air : HearAdvert(i, m) \/ \E i \in Inviters : Invite(i) \/ \E m \in air : Deliver(m) \* Terminal states exist (all presses used, every message delivered), so the \* model is checked with CHECK_DEADLOCK FALSE. (***************************************************************************) (* PROPERTIES CHECKED *) (***************************************************************************) \* An open window means the tag has no crew: joining closes the window, and \* the button opens one only on an unclaimed tag. WindowMeansNoCrew == window # 0 => crew = NoCrew \* 1. The tag's crew is never a crew nobody sent an invite for. NoUninvitedJoin == crew # NoCrew => \E m \in air : m.kind = "inv" /\ m.from = crew \* 2. The crew is set only in a step where the window was open, and that \* step closes the window. Two-state, so checked as an action property. JoinStep == crew' # crew /\ crew' # NoCrew WindowGate == [][JoinStep => (window # 0 /\ window' = 0)]_vars \* 3. Between two presses the crew is set at most once. OneJoinPerWindow == joins <= 1 \* 4. The honest-only case: as long as no attacker has sent an invite, the \* tag is either unclaimed or in a crew of someone who pressed invite \* (which NoUninvitedJoin makes exact). With Attackers = {} this is the \* whole story; with an attacker present it says the tag lands in the \* attacker's crew only because the attacker really invited it. HonestUnlessAttacked == (\A a \in Attackers : invited[a] = {}) => crew \in {NoCrew} \cup Honest \* 6. An invite is applied only in the window it was sent for. This is the \* property the session id exists for; without it (CheckSession = FALSE) \* a delayed invite from an earlier window is applied in a later one. NoStaleJoin == ~stale \* 5. NOT a property of this design, kept as a documented non-property: \* with an attacker in range during the window, first invite wins and the \* tag can end up in the attacker's crew. Expected to fail; see the \* README for why that is accepted and what would close it. NoHijack == crew \notin Attackers =============================================================================