-------------------------------- MODULE Gate --------------------------------
(***************************************************************************)
(* The ARBITER gate (gate/worker.js, version gate-2) as a state machine,   *)
(* for the TLC model checker. TLC tries every order of the events below,   *)
(* up to the bounds in the .cfg files, and checks the properties at the    *)
(* end (G1 to G3 of docs/FOUNDATION.md) in every state it reaches.         *)
(*                                                                         *)
(* It checks the DESIGN, not that worker.js matches it. Each action names  *)
(* the function of worker.js it stands for, so a reviewer can compare the  *)
(* two; that comparison is by hand.                                        *)
(*                                                                         *)
(* WHO ACTS                                                                *)
(*  - The owners (Owners) and one approver (Approver): people the design   *)
(*    trusts, with passkeys on their own devices. An owner signs only      *)
(*    changes from GoodOps: it never activates, grants or lists anything   *)
(*    of the attacker's (registration is a moment of trust: the owner      *)
(*    checks the fingerprint). The approver may approve or reject ANY      *)
(*    request the gate shows them: the model does not rely on their        *)
(*    judgement, only on the gate's checks.                                *)
(*  - The attacker is root on the ARBITER server (A5): it holds ARBITER's   *)
(*    real key K and a key KX of its own, so it can ask for any payment;   *)
(*    its own passkey X and key KX are registered (pending) from the       *)
(*    start; it reads the public log, so it can replay every signature     *)
(*    that ever appeared there, owner changes and decisions alike, at any  *)
(*    moment, for any request; and it can sign anything with X. It cannot  *)
(*    sign with an owner's or the approver's passkey, and does not know    *)
(*    SETUP_CODE.                                                          *)
(*                                                                         *)
(* WHAT IS ABSTRACTED                                                      *)
(*  - Signatures are values that say who signed what. A signature over     *)
(*    other terms, or by another key, does not verify, so no action is     *)
(*    given one. WebAuthn's origin, flags and counter checks are not       *)
(*    modelled (they hold against other sites and copied keys, not here).  *)
(*  - Where the code checks something and then, after an `await`, opens    *)
(*    its transaction, the model has two steps, and any other event may    *)
(*    happen between them: intake, decide and owner changes each have a    *)
(*    check step and a transaction step. The design must not depend on     *)
(*    the checks made before the transaction.                              *)
(*  - A step that is never taken is a crash or a call that never           *)
(*    finished: TLC explores those states too, so nothing here needs a     *)
(*    separate crash. An owner's browser sends a change as it is signed.   *)
(*  - The clock moves in whole steps (Tick). Every company is already      *)
(*    added (the "tenant" change only names one). The request fields the   *)
(*    gate only checks for form (currency, intent, the JSON shape) are     *)
(*    left out; at most one intake per request id is in flight at once     *)
(*    (a second one is refused or answered "again" by the transaction).    *)
(*  - The owner flag plays no part in a decision (decideChecked never      *)
(*    reads it), so an owner who also approves is the Approver case.       *)
(*  - A payment instruction that failed may still have been delivered, so  *)
(*    every attempt counts as a payment.                                   *)
(*                                                                         *)
(* Mut names checks to REMOVE, to show that a property fails without them: *)
(* gate-2 is Mut = {}; check.sh runs each mutation and expects TLC to find *)
(* the violation it names.                                                 *)
(***************************************************************************)
EXTENDS Naturals, FiniteSets

CONSTANTS
    Tenants,        \* companies at the gate
    GoodAccounts,   \* payees an owner may list
    BadAccounts,    \* the attacker's accounts: never listed
    MaxAmount,      \* amounts and limits are 1..MaxAmount
    ReqIds,         \* request ids (whoever asks chooses them)
    MaxTime,        \* the clock runs 0..MaxTime
    MaxLife,        \* a request expires at most MaxLife after it arrives
    OpWindow,       \* a signed change is accepted up to OpWindow after it was prepared
    MaxOps,         \* how many changes the owners sign in one run
    Owners,         \* the owners' passkeys
    FirstOwner,     \* the one made at /setup (in Owners)
    Approver,       \* the approver's passkey
    X,              \* the attacker's passkey
    K,              \* ARBITER's real key (root on the server holds it)
    KX,             \* a key the attacker makes
    None,           \* "no value"
    Start,          \* "any": any state owners' changes reach; "granted": everything granted; "setup": nothing yet
    Mut             \* checks removed (a subset of Mutations)

Mutations == {"no_standing", "verify_only", "terms_without_request", "no_single_use",
              "no_used_ops", "no_signer_recheck"}

Passkeys  == Owners \cup {Approver, X}
Honest    == Owners \cup {Approver}
Keys      == {K, KX}
Accounts  == GoodAccounts \cup BadAccounts
Amounts   == 1..MaxAmount
Statuses  == {"none", "pending", "active", "revoked"}
Decisions == {"approve", "reject"}
RStatuses == {"none", "pending", "executing", "executed", "failed", "rejected", "expired"}

ASSUME /\ FirstOwner \in Owners /\ Mut \subseteq Mutations /\ Start \in {"any", "granted", "setup"}
       /\ MaxTime \in Nat /\ MaxLife >= 1

(* An owner change (validateOp): one record shape for every kind. *)
Op(do, p, t, acct, max, key, ts, owner) ==
    [do |-> do, p |-> p, t |-> t, acct |-> acct, max |-> max, key |-> key, ts |-> ts, owner |-> owner]

(* Every change an owner may sign, by kind (tm, ta: a company and an amount, or an
   account). Nothing here names X, KX or a bad account. *)
OpsActivateApprover == {Op("activate", Approver, None, None, 0, None, {}, FALSE)}
OpsActivateOwner    == {Op("activate", p, None, None, 0, None, {}, TRUE) : p \in Owners \ {FirstOwner}}
OpsRevoke           == {Op("revoke", p, None, None, 0, None, {}, FALSE) : p \in Honest}
OpsGrant            == {Op("grant", Approver, tm[1], None, tm[2], None, {}, FALSE) : tm \in Tenants \X Amounts}
OpsUngrant          == {Op("ungrant", Approver, t, None, 0, None, {}, FALSE) : t \in Tenants}
OpsPayee            == {Op("payee", None, ta[1], ta[2], 0, None, {}, FALSE) : ta \in Tenants \X GoodAccounts}
OpsUnpayee          == {Op("unpayee", None, ta[1], ta[2], 0, None, {}, FALSE) : ta \in Tenants \X GoodAccounts}
OpsArbiter          == {Op("arbiter", None, None, None, 0, K, ts, FALSE) : ts \in (SUBSET Tenants) \ {{}}}
OpsUnarbiter        == {Op("unarbiter", None, None, None, 0, K, {}, FALSE)}

GoodOps ==
    OpsActivateApprover \cup OpsActivateOwner \cup OpsRevoke \cup OpsGrant \cup OpsUngrant
    \cup OpsPayee \cup OpsUnpayee \cup OpsArbiter \cup OpsUnarbiter

(* A request's text (intakeChecked): who signed it and what it asks. *)
Bodies == [key : Keys, t : Tenants, acct : Accounts, amt : Amounts, exp : 1..(MaxTime + MaxLife)]

VARIABLES
    now,         \* the gate's clock
    pk,          \* passkeys: status
    own,         \* passkeys: owner flag
    grant,       \* grants: limit per passkey and company, 0 = none
    payees,      \* <<company, account>> pairs an owner listed
    ak,          \* ARBITER keys: status
    akT,         \* ARBITER keys: the companies each may ask for
    rS,          \* requests: status
    rB,          \* requests: text (None until received; never changed after)
    used,        \* used_ops: ids of applied changes
    nextOp,      \* the next fresh change id (opStart)
    loggedOps,   \* owner-change signatures in the public log
    loggedDecs,  \* decision signatures in the public log
    opCalls,     \* opFinish calls past their checks, before their transaction
    decCalls,    \* decide calls past their checks, before their transaction
    inCalls,     \* intake calls past their checks, before their transaction
    effects,     \* approved requests whose payment instruction is not sent yet
    \* What happened, kept only for the properties (not the gate's state):
    approved,    \* requests with an approval recorded (each one goes on to send a payment)
    setups,      \* how many times /setup made an owner
    broken       \* the properties some step broke (each is checked as that step happens)

gate    == <<now, pk, own, grant, payees, ak, akT, rS, rB, used, nextOp>>
calls   == <<loggedOps, loggedDecs, opCalls, decCalls, inCalls, effects>>
history == <<approved, setups, broken>>
vars    == <<gate, calls, history>>

-----------------------------------------------------------------------------
(* Facts the gate's checks read *)

ActiveOwners == {p \in Passkeys : own[p] /\ pk[p] = "active"}

(* setupClosed: an owner exists that is not pending (active, or revoked: closed for good). *)
SetupClosed == \E p \in Passkeys : own[p] /\ pk[p] \in {"active", "revoked"}

(* termsText: what a person signs to decide a request. *)
Terms(r, d) ==
    IF "terms_without_request" \in Mut
    THEN [d |-> d, r |-> None, t |-> rB[r].t, acct |-> rB[r].acct, amt |-> rB[r].amt, body |-> None]
    ELSE [d |-> d, r |-> r, t |-> rB[r].t, acct |-> rB[r].acct, amt |-> rB[r].amt, body |-> rB[r]]

(* decideChecked's grantOk *)
GrantOk(p, r, d) ==
    /\ grant[p, rB[r].t] > 0
    /\ d = "approve" => rB[r].amt <= grant[p, rB[r].t]

(* decideChecked's standingOk (gate-2): the key still granted for the company, the payee still listed *)
StandingOk(r, d) ==
    \/ d = "reject"
    \/ "no_standing" \in Mut
    \/ /\ ak[rB[r].key] = "active"
       /\ rB[r].t \in akT[rB[r].key]
       /\ <<rB[r].t, rB[r].acct>> \in payees

(* The authority section 4 says must hold when an approval is recorded, read from the
   gate's records directly, never through the checks above, so a removed check shows. *)
InForce(p, b) ==
    /\ pk[p] = "active"
    /\ grant[p, b.t] >= b.amt
    /\ ak[b.key] = "active"
    /\ b.t \in akT[b.key]
    /\ <<b.t, b.acct>> \in payees
    /\ b.exp >= now

-----------------------------------------------------------------------------
(* Where it starts *)

Init ==
    /\ now = 0
    /\ CASE Start = "any" ->
            (* Any state an owner's changes can reach from setup: the first owner's
               passkey active; every other honest passkey in any status, the approver
               with any limits once it was active; ARBITER's key in any status and
               companies. *)
            /\ pk \in [Passkeys -> Statuses]
            /\ pk[FirstOwner] = "active"
            /\ pk[X] = "pending"
            /\ own = [p \in Passkeys |-> p \in Owners /\ pk[p] \in {"active", "revoked"}]
            /\ grant \in [Passkeys \X Tenants -> 0..MaxAmount]
            /\ \A p \in Passkeys, t \in Tenants :
                 grant[p, t] > 0 => p = Approver /\ pk[p] \in {"active", "revoked"}
            /\ payees \in SUBSET (Tenants \X GoodAccounts)
            /\ ak \in [Keys -> Statuses]
            /\ ak[KX] = "pending"
            /\ akT \in [Keys -> SUBSET Tenants]
            /\ \A key \in Keys : (akT[key] # {}) <=> (ak[key] \in {"active", "revoked"})
            /\ setups = 1
         [] Start = "granted" ->
            (* Everything granted: the approver for every company up to MaxAmount, every
               good payee listed, ARBITER's key for every company; any further owner
               pending or active. *)
            /\ pk \in [Passkeys -> Statuses]
            /\ pk[FirstOwner] = "active" /\ pk[Approver] = "active" /\ pk[X] = "pending"
            /\ \A p \in Owners \ {FirstOwner} : pk[p] \in {"pending", "active"}
            /\ own = [p \in Passkeys |-> p \in Owners /\ pk[p] = "active"]
            /\ grant = [pt \in Passkeys \X Tenants |-> IF pt[1] = Approver THEN MaxAmount ELSE 0]
            /\ payees = Tenants \X GoodAccounts
            /\ ak = [key \in Keys |-> IF key = K THEN "active" ELSE "pending"]
            /\ akT = [key \in Keys |-> IF key = K THEN Tenants ELSE {}]
            /\ setups = 1
         [] Start = "setup" ->
            /\ pk = [p \in Passkeys |-> IF p = X THEN "pending" ELSE "none"]
            /\ own = [p \in Passkeys |-> FALSE]
            /\ grant = [pt \in Passkeys \X Tenants |-> 0]
            /\ payees = {}
            /\ ak = [key \in Keys |-> IF key = KX THEN "pending" ELSE "none"]
            /\ akT = [key \in Keys |-> {}]
            /\ setups = 0
    /\ rS = [r \in ReqIds |-> "none"]
    /\ rB = [r \in ReqIds |-> None]
    /\ used = {}
    /\ nextOp = 1
    /\ loggedOps = {} /\ loggedDecs = {}
    /\ opCalls = {} /\ decCalls = {} /\ inCalls = {} /\ effects = {}
    /\ approved = {} /\ broken = {}

-----------------------------------------------------------------------------
(* What can happen *)

Tick ==
    /\ now < MaxTime
    /\ now' = now + 1
    /\ UNCHANGED <<pk, own, grant, payees, ak, akT, rS, rB, used, nextOp, calls, history>>

(* setupStart / setupFinish: only the first owner holds SETUP_CODE. *)
Setup ==
    /\ ~SetupClosed
    /\ pk[FirstOwner] = "none"
    /\ pk' = [pk EXCEPT ![FirstOwner] = "active"]
    /\ own' = [own EXCEPT ![FirstOwner] = TRUE]
    /\ setups' = setups + 1
    /\ broken' = IF setups > 0 THEN broken \cup {"G3_SetupOnce"} ELSE broken
    /\ UNCHANGED <<now, grant, payees, ak, akT, rS, rB, used, nextOp, calls, approved>>

(* registerFinish (the approver, a further owner) and arbiterRegister (ARBITER's key):
   anyone may register; it is pending, and a passkey is not an owner. *)
Register(p) ==
    /\ p \in Honest \ {FirstOwner}
    /\ pk[p] = "none"
    /\ pk' = [pk EXCEPT ![p] = "pending"]
    /\ UNCHANGED <<now, own, grant, payees, ak, akT, rS, rB, used, nextOp, calls, history>>

RegisterKey ==
    /\ ak[K] = "none"
    /\ ak' = [ak EXCEPT ![K] = "pending"]
    /\ UNCHANGED <<now, pk, own, grant, payees, akT, rS, rB, used, nextOp, calls, history>>

(* opFinish before its transaction: the terms are fresh, the signature verifies
   (verifyAssertion: an active passkey) and it is an owner's. *)
OpCheckOk(s) == now - s.at <= OpWindow /\ pk[s.by] = "active" /\ own[s.by]

(* An owner prepares a change (opStart: fresh terms, a new id), signs it on their device,
   and their browser sends it. *)
Sign(h, op) ==
    /\ nextOp <= MaxOps
    /\ LET s == [id |-> nextOp, at |-> now, op |-> op, by |-> h]
       IN /\ OpCheckOk(s)
          /\ opCalls' = opCalls \cup {s}
    /\ nextOp' = nextOp + 1
    /\ UNCHANGED <<now, pk, own, grant, payees, ak, akT, rS, rB, used,
                   loggedOps, loggedDecs, decCalls, inCalls, effects, history>>

(* The attacker replays a signed change from the log. *)
Replay(s) ==
    /\ s \in loggedOps
    /\ OpCheckOk(s)
    /\ opCalls' = opCalls \cup {s}
    /\ UNCHANGED <<gate, loggedOps, loggedDecs, decCalls, inCalls, effects, history>>

(* applyOp's preconditions *)
Pre(op) ==
    CASE op.do = "activate"  -> pk[op.p] = "pending"
      [] op.do = "revoke"    -> /\ pk[op.p] \in {"pending", "active"}
                                /\ ~(own[op.p] /\ pk[op.p] = "active" /\ Cardinality(ActiveOwners) <= 1)
      [] op.do = "grant"     -> pk[op.p] = "active"
      [] op.do = "ungrant"   -> grant[op.p, op.t] > 0
      [] op.do = "payee"     -> TRUE
      [] op.do = "unpayee"   -> <<op.t, op.acct>> \in payees
      [] op.do = "arbiter"   -> ak[op.key] \in {"pending", "active"}
      [] op.do = "unarbiter" -> ak[op.key] # "none"

(* opFinish's transaction: the change was not applied before (used_ops), the signer is
   still an active owner, applyOp's preconditions hold; then applyOp, logged. *)
OpTxn(s) ==
    /\ s \in opCalls
    /\ opCalls' = opCalls \ {s}
    /\ IF /\ (s.id \notin used \/ "no_used_ops" \in Mut)
          /\ ((pk[s.by] = "active" /\ own[s.by]) \/ "no_signer_recheck" \in Mut)
          /\ Pre(s.op)
       THEN LET op == s.op IN
            /\ pk' = CASE op.do = "activate" -> [pk EXCEPT ![op.p] = "active"]
                       [] op.do = "revoke"   -> [pk EXCEPT ![op.p] = "revoked"]
                       [] OTHER              -> pk
            /\ own' = IF op.do = "activate" THEN [own EXCEPT ![op.p] = op.owner] ELSE own
            /\ grant' = CASE op.do = "grant"   -> [grant EXCEPT ![op.p, op.t] = op.max]
                          [] op.do = "ungrant" -> [grant EXCEPT ![op.p, op.t] = 0]
                          [] OTHER             -> grant
            /\ payees' = CASE op.do = "payee"   -> payees \cup {<<op.t, op.acct>>}
                           [] op.do = "unpayee" -> payees \ {<<op.t, op.acct>>}
                           [] OTHER             -> payees
            /\ ak' = CASE op.do = "arbiter"   -> [ak EXCEPT ![op.key] = "active"]
                       [] op.do = "unarbiter" -> [ak EXCEPT ![op.key] = "revoked"]
                       [] OTHER               -> ak
            /\ akT' = IF op.do = "arbiter" THEN [akT EXCEPT ![op.key] = op.ts] ELSE akT
            /\ used' = used \cup {s.id}
            /\ loggedOps' = loggedOps \cup {s}
       ELSE UNCHANGED <<pk, own, grant, payees, ak, akT, used, loggedOps>>
    /\ UNCHANGED <<now, rS, rB, nextOp, loggedDecs, decCalls, inCalls, effects, history>>

(* intakeChecked before its transaction. Whoever holds a key may ask anything: the
   attacker holds both. Signed by an active key granted for the company, to a listed
   payee, in the next MaxLife, and some active passkey may approve that amount. *)
IntakeCheck(r, b) ==
    /\ rS[r] = "none"
    /\ ~\E c \in inCalls : c.r = r
    /\ b.exp \in (now + 1)..(now + MaxLife)
    /\ ak[b.key] = "active"
    /\ b.t \in akT[b.key]
    /\ <<b.t, b.acct>> \in payees
    /\ \E p \in Passkeys : pk[p] = "active" /\ grant[p, b.t] >= b.amt
    /\ inCalls' = inCalls \cup {[r |-> r, body |-> b]}
    /\ UNCHANGED <<gate, loggedOps, loggedDecs, opCalls, decCalls, effects, history>>

(* intakeChecked's transaction: it re-checks only that the id is new. *)
IntakeTxn(c) ==
    /\ c \in inCalls
    /\ inCalls' = inCalls \ {c}
    /\ IF rS[c.r] = "none"
       THEN /\ rS' = [rS EXCEPT ![c.r] = "pending"]
            /\ rB' = [rB EXCEPT ![c.r] = c.body]
       ELSE UNCHANGED <<rS, rB>>
    /\ UNCHANGED <<now, pk, own, grant, payees, ak, akT, used, nextOp,
                   loggedOps, loggedDecs, opCalls, decCalls, effects, history>>

(* expireOld *)
Expire(r) ==
    /\ rS[r] = "pending"
    /\ rB[r].exp < now
    /\ rS' = [rS EXCEPT ![r] = "expired"]
    /\ UNCHANGED <<now, pk, own, grant, payees, ak, akT, rB, used, nextOp, calls, history>>

(* decideChecked before its transaction: the request is pending and not expired
   (requestRow runs expireOld first), the signature is over its exact terms by an active
   passkey (verifyAssertion), grantOk, standingOk. *)
DecCheck(s, r, d) ==
    /\ rS[r] = "pending"
    /\ rB[r].exp >= now
    /\ s.terms = Terms(r, d)
    /\ pk[s.pk] = "active"
    /\ GrantOk(s.pk, r, d)
    /\ StandingOk(r, d)

(* A person opens the gate's page for a request and signs its exact terms. A decision
   signature is [pk, terms, chosen]: the gate reads pk and terms; chosen, the request
   the person chose on the page, is read only by the properties. *)
PersonDecides(h, r, d) ==
    /\ rS[r] = "pending"
    /\ LET s == [pk |-> h, terms |-> Terms(r, d), chosen |-> r]
       IN /\ DecCheck(s, r, d)
          /\ decCalls' = decCalls \cup {[sig |-> s, r |-> r, d |-> d]}
    /\ UNCHANGED <<gate, loggedOps, loggedDecs, opCalls, inCalls, effects, history>>

(* The attacker sends a decision signature: one from the log, or one made with X. *)
AttackerDecides(s, r, d) ==
    /\ DecCheck(s, r, d)
    /\ decCalls' = decCalls \cup {[sig |-> s, r |-> r, d |-> d]}
    /\ UNCHANGED <<gate, loggedOps, loggedDecs, opCalls, inCalls, effects, history>>

(* decideChecked's transaction: every fact read again; an approval moves the request to
   executing (single use) and the payment instruction follows after it. When an approval
   is recorded, G1 (section 4) is checked against the gate's records, and G2: decideChecked
   sends a payment after every approval it records, so a second approval of a request is
   a second payment. *)
DecTxn(c) ==
    /\ c \in decCalls
    /\ decCalls' = decCalls \ {c}
    /\ LET r == c.r
           p == c.sig.pk
           d == c.d
           b == rB[r]
       IN IF /\ rS[r] = "pending"
             /\ b.exp >= now
             /\ \/ "verify_only" \in Mut
                \/ pk[p] = "active" /\ GrantOk(p, r, d) /\ StandingOk(r, d)
          THEN /\ rS' = [rS EXCEPT ![r] = IF d = "reject" THEN "rejected"
                                          ELSE IF "no_single_use" \in Mut THEN "pending"
                                          ELSE "executing"]
               /\ loggedDecs' = loggedDecs \cup {c.sig}
               /\ IF d = "approve"
                  THEN /\ effects' = effects \cup {[r |-> r, sig |-> c.sig]}
                       /\ approved' = approved \cup {r}
                       /\ broken' = broken
                            \cup (IF InForce(p, b) THEN {} ELSE {"G1_ApprovedWithAuthorityInForce"})
                            \cup (IF r \in approved THEN {"G2_AtMostOnce"} ELSE {})
                  ELSE UNCHANGED <<effects, approved, broken>>
          ELSE UNCHANGED <<rS, loggedDecs, effects, approved, broken>>
    /\ UNCHANGED <<now, pk, own, grant, payees, ak, akT, rB, used, nextOp,
                   loggedOps, opCalls, inCalls, setups>>

(* effect: the payment instruction is sent (it may fail, and is never retried). G1 (who)
   is checked as it is sent. *)
Effect(e) ==
    /\ e \in effects
    /\ effects' = effects \ {e}
    /\ rS' = [rS EXCEPT ![e.r] = "executed"]
    /\ broken' = broken
         \cup (IF e.sig.pk \in Honest /\ e.sig.chosen = e.r THEN {}
               ELSE {"G1_PaidOnlyAsAPersonApproved"})
         \cup (IF rB[e.r].acct \in GoodAccounts THEN {} ELSE {"G1_PaidOnlyToListedPayees"})
    /\ UNCHANGED <<now, pk, own, grant, payees, ak, akT, rB, used, nextOp,
                   loggedOps, loggedDecs, opCalls, decCalls, inCalls, approved, setups>>

(* The steps by name (TLC's counterexamples name each step by these). *)
OwnerSigns         == \E h \in Owners, op \in GoodOps : Sign(h, op)
AttackerReplaysOp  == \E s \in loggedOps : Replay(s)
ChangeApplied      == \E s \in opCalls : OpTxn(s)
RequestChecked     == \E r \in ReqIds, b \in Bodies : IntakeCheck(r, b)
RequestRecorded    == \E c \in inCalls : IntakeTxn(c)
RequestExpires     == \E r \in ReqIds : Expire(r)
PersonSigns        == \E h \in Honest, r \in ReqIds, d \in Decisions : PersonDecides(h, r, d)
AttackerSendsSig   == \E r \in ReqIds, d \in Decisions :
                        /\ rS[r] = "pending"
                        /\ \E s \in loggedDecs \cup {[pk |-> X, terms |-> Terms(r, d), chosen |-> None]} :
                             AttackerDecides(s, r, d)
DecisionRecorded   == \E c \in decCalls : DecTxn(c)
PaymentSent        == \E e \in effects : Effect(e)

Next ==
    \/ Tick
    \/ Setup
    \/ \E p \in Passkeys : Register(p)
    \/ RegisterKey
    \/ OwnerSigns
    \/ AttackerReplaysOp
    \/ ChangeApplied
    \/ RequestChecked
    \/ RequestRecorded
    \/ RequestExpires
    \/ PersonSigns
    \/ AttackerSendsSig
    \/ DecisionRecorded
    \/ PaymentSent

Spec == Init /\ [][Next]_vars

-----------------------------------------------------------------------------
(* What must hold *)

TypeOK ==
    /\ now \in 0..MaxTime
    /\ pk \in [Passkeys -> Statuses]
    /\ own \in [Passkeys -> BOOLEAN]
    /\ grant \in [Passkeys \X Tenants -> 0..MaxAmount]
    /\ payees \subseteq Tenants \X Accounts
    /\ ak \in [Keys -> Statuses]
    /\ akT \in [Keys -> SUBSET Tenants]
    /\ rS \in [ReqIds -> RStatuses]
    /\ \A r \in ReqIds : (rS[r] = "none") <=> (rB[r] = None)
    /\ \A r \in ReqIds : rB[r] # None => rB[r] \in Bodies

(* G1, section 4: when an approval was recorded, the request had not expired, the ARBITER
   key that asked was active and granted for the company, the payee listed, and the
   approving passkey active and granted for the company with a limit at least the amount. *)
G1_ApprovedWithAuthorityInForce == "G1_ApprovedWithAuthorityInForce" \notin broken

(* G1, who: every payment instruction was approved by a person the design trusts, who
   chose, on the gate's page, to approve exactly that request (whose text never changes):
   the signature it went out on is theirs, and they made it for that request. *)
G1_PaidOnlyAsAPersonApproved == "G1_PaidOnlyAsAPersonApproved" \notin broken

(* G1: nothing is ever paid to an account the owner did not list. *)
G1_PaidOnlyToListedPayees == "G1_PaidOnlyToListedPayees" \notin broken

(* G2: at most once. A request is approved, and so paid, at most once. *)
G2_AtMostOnce == "G2_AtMostOnce" \notin broken

(* G3: setup makes an owner once; the gate always has an active owner after it. *)
G3_SetupOnce == "G3_SetupOnce" \notin broken
G3_AlwaysAnOwner == setups > 0 => ActiveOwners # {}

(* G3: the attacker's passkey and key never gain authority. *)
G3_AttackerNeverGranted ==
    /\ pk[X] # "active"
    /\ ak[KX] # "active"
    /\ \A t \in Tenants : grant[X, t] = 0

(* G3, as a property of every step: authority in force changes only when a change an
   owner signed is applied for the first time while its signer is an active owner, or at
   setup. (Only Sign makes an owner's signature, so every change in opCalls is one.) *)
Authority ==
    [active  |-> {p \in Passkeys : pk[p] = "active"},
     owners  |-> ActiveOwners,
     grant   |-> grant,
     payees  |-> payees,
     keys    |-> {<<key, akT[key]>> : key \in {kk \in Keys : ak[kk] = "active"}}]

G3_AuthorityOnlyByOwners ==
    [][ Authority' # Authority =>
          \/ \E s \in opCalls :
                /\ s.id \notin used
                /\ used' = used \cup {s.id}
                /\ pk[s.by] = "active" /\ own[s.by]
          \/ setups = 0 /\ setups' = 1
      ]_vars

=============================================================================