------------------------------ MODULE GateProof ------------------------------ (***************************************************************************) (* G1 to G3 for the gate's model (Gate.tla), proved for every behaviour, *) (* with no bounds: any number of companies, requests, owners, payees and *) (* changes, any amounts and limits, any clock. TLC (check.sh) tries every *) (* order of events up to stated bounds; this proves the same properties *) (* for all of them. TLAPS checks every step (prove.sh). *) (* *) (* The bounds in Gate.tla (MaxTime, MaxOps, MaxAmount, MaxLife) are *) (* constants here with nothing assumed of them but that they are numbers, *) (* so the proof covers each of their values: a run of the real gate of any *) (* length is a run of the model for some value of them. *) (* *) (* It is a proof about the design (Mut = {}: gate-2 as modelled), not about *) (* worker.js: that the code does what Gate.tla says is still compared by *) (* hand. *) (* *) (* The method: an invariant Inv that holds in every initial state and that *) (* every step keeps (it is inductive), strong enough that the properties *) (* follow from it. Each part of Inv says why one property holds. *) (***************************************************************************) EXTENDS Gate, TLAPS, FiniteSetTheorems (* What the proof assumes of the constants: the gate as deployed (no check removed), and the attacker's passkeys and keys distinct from the people's and ARBITER's: no attacker's passkey is an owner's or an approver's, no attacker's key is ARBITER's. An owner may also be an approver. *) ASSUME Assumptions == /\ Mut = {} /\ FirstOwner \in Owners /\ Start \in {"any", "granted", "setup", "empty"} /\ Intruders \cap Owners = {} /\ Intruders \cap Approvers = {} /\ ArbiterKeys \cap RootKeys = {} /\ None \notin Bodies /\ MaxAmount \in Nat /\ MaxLife \in Nat /\ OpWindow \in Nat ----------------------------------------------------------------------------- (* What an owner's change can be: every change in GoodOps is one of these. *) GoodOp(op) == \/ op.do = "activate" /\ op.p \in Approvers /\ op.owner = FALSE \/ op.do = "activate" /\ op.p \in Owners /\ op.owner = TRUE \/ op.do = "revoke" /\ op.p \in Passkeys \/ op.do = "grant" /\ op.p \in Approvers /\ op.t \in Tenants /\ op.max \in Amounts \/ op.do = "ungrant" /\ op.p \in Approvers /\ op.t \in Tenants \/ op.do = "payee" /\ op.t \in Tenants /\ op.acct \in GoodAccounts \/ op.do = "unpayee" /\ op.t \in Tenants /\ op.acct \in GoodAccounts \/ op.do = "arbiter" /\ op.key \in ArbiterKeys /\ op.ts \subseteq Tenants \/ op.do = "unarbiter" /\ op.key \in Keys LEMMA GoodOpsAreGood == \A op \in GoodOps : GoodOp(op) <1> SUFFICES ASSUME NEW op \in GoodOps PROVE GoodOp(op) OBVIOUS <1>0. \/ op \in OpsActivateApprover \/ op \in OpsActivateOwner \/ op \in OpsRevoke \/ op \in OpsGrant \/ op \in OpsUngrant \/ op \in OpsPayee \/ op \in OpsUnpayee \/ op \in OpsArbiter \/ op \in OpsUnarbiter BY DEF GoodOps <1>1. CASE op \in OpsActivateApprover <2> PICK p \in Approvers : op = Op("activate", p, None, None, 0, None, {}, FALSE) BY <1>1 DEF OpsActivateApprover <2> QED BY DEF Op, GoodOp <1>2. CASE op \in OpsActivateOwner <2> PICK p \in Owners \ {FirstOwner} : op = Op("activate", p, None, None, 0, None, {}, TRUE) BY <1>2 DEF OpsActivateOwner <2> QED BY DEF Op, GoodOp <1>3. CASE op \in OpsRevoke <2> PICK p \in Passkeys : op = Op("revoke", p, None, None, 0, None, {}, FALSE) BY <1>3 DEF OpsRevoke <2> QED BY DEF Op, GoodOp <1>4. CASE op \in OpsGrant <2> PICK g \in Approvers \X Tenants \X Amounts : op = Op("grant", g[1], g[2], None, g[3], None, {}, FALSE) BY <1>4 DEF OpsGrant <2> QED BY DEF Op, GoodOp <1>5. CASE op \in OpsUngrant <2> PICK pt \in Approvers \X Tenants : op = Op("ungrant", pt[1], pt[2], None, 0, None, {}, FALSE) BY <1>5 DEF OpsUngrant <2> QED BY DEF Op, GoodOp <1>6. CASE op \in OpsPayee <2> PICK ta \in Tenants \X GoodAccounts : op = Op("payee", None, ta[1], ta[2], 0, None, {}, FALSE) BY <1>6 DEF OpsPayee <2> QED BY DEF Op, GoodOp <1>7. CASE op \in OpsUnpayee <2> PICK ta \in Tenants \X GoodAccounts : op = Op("unpayee", None, ta[1], ta[2], 0, None, {}, FALSE) BY <1>7 DEF OpsUnpayee <2> QED BY DEF Op, GoodOp <1>8. CASE op \in OpsArbiter <2> PICK kt \in ArbiterKeys \X ((SUBSET Tenants) \ {{}}) : op = Op("arbiter", None, None, None, 0, kt[1], kt[2], FALSE) BY <1>8 DEF OpsArbiter <2> QED BY DEF Op, GoodOp <1>9. CASE op \in OpsUnarbiter <2> PICK k \in Keys : op = Op("unarbiter", None, None, None, 0, k, {}, FALSE) BY <1>9 DEF OpsUnarbiter <2> QED BY DEF Op, GoodOp <1> QED BY <1>0, <1>1, <1>2, <1>3, <1>4, <1>5, <1>6, <1>7, <1>8, <1>9 (* Facts the steps below use everywhere. *) LEMMA Basics == /\ FirstOwner \in Passkeys /\ Owners \subseteq Passkeys /\ Approvers \subseteq Passkeys /\ Intruders \subseteq Passkeys /\ Honest \subseteq Passkeys /\ Intruders \cap Honest = {} /\ ArbiterKeys \subseteq Keys /\ RootKeys \subseteq Keys /\ {"none", "pending", "active", "revoked"} \subseteq Statuses BY Assumptions DEF Passkeys, Honest, Keys, Statuses ----------------------------------------------------------------------------- (* The invariant *) (* The shape of every variable: the records of authority, then the rest. *) TypeAuth == /\ 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] TypeRest == /\ now \in Nat /\ rS \in [ReqIds -> RStatuses] /\ rB \in [ReqIds -> Bodies \cup {None}] /\ \A r \in ReqIds : (rS[r] = "none") <=> (rB[r] = None) /\ used \subseteq Nat /\ nextOp \in Nat /\ approved \subseteq ReqIds /\ setups \in {0, 1} /\ \A c \in inCalls : c.r \in ReqIds /\ c.body \in Bodies (* Every signed change in a call or in the log was made by an owner, over a good change. *) OpsInv == \A s \in opCalls \cup loggedOps : s.by \in Owners /\ s.id \in Nat /\ s.at \in Nat /\ GoodOp(s.op) (* G3: the attacker's passkeys and keys never gain authority; the owner flag marks only owners' activated passkeys; payees are only ever good accounts; setup closes for good; and after setup there is always an active owner. *) Out == {"none", "pending", "revoked"} AttackerOut == /\ \A x \in Intruders : pk[x] \in Out /\ own[x] = FALSE /\ \A t \in Tenants : grant[x, t] = 0 /\ \A k \in RootKeys : ak[k] \in Out OwnerFlags == \A p \in Passkeys : own[p] => p \in Owners /\ pk[p] \in {"active", "revoked"} GoodPayees == payees \subseteq Tenants \X GoodAccounts SetupInv == /\ setups = 1 => SetupClosed /\ setups = 1 => ActiveOwners # {} (* G1 and G2: every decision on its way, in the log or paying, is a signature a person the owner chose made for that very request; an approved request is never pending again, and its payee was listed when it was approved. *) DecInv == /\ \A c \in decCalls : /\ c.r \in ReqIds /\ c.d \in Decisions /\ c.sig.pk \in Honest /\ c.sig.chosen = c.r /\ c.sig.terms.r = c.r /\ \A s \in loggedDecs : s.pk \in Honest /\ s.chosen = s.terms.r /\ \A e \in effects : e.r \in approved /\ e.sig.pk \in Honest /\ e.sig.chosen = e.r /\ \A r \in approved : rS[r] \in {"executing", "executed"} /\ rB[r] \in Bodies /\ rB[r].acct \in GoodAccounts Inv == /\ TypeAuth /\ TypeRest /\ OpsInv /\ AttackerOut /\ OwnerFlags /\ GoodPayees /\ SetupInv /\ DecInv /\ broken = {} ----------------------------------------------------------------------------- (* Inv holds at the start *) LEMMA InitInv == Init => Inv <1> SUFFICES ASSUME Init PROVE Inv OBVIOUS <1> USE Assumptions, Basics <1>0. /\ now = 0 /\ rS = [r \in ReqIds |-> "none"] /\ rB = [r \in ReqIds |-> None] /\ used = {} /\ nextOp = 1 /\ loggedOps = {} /\ loggedDecs = {} /\ opCalls = {} /\ decCalls = {} /\ inCalls = {} /\ effects = {} /\ approved = {} /\ broken = {} BY DEF Init <1>1. ASSUME setups \in {0, 1} PROVE TypeRest /\ OpsInv /\ DecInv /\ broken = {} BY <1>0, <1>1 DEF TypeRest, OpsInv, DecInv, RStatuses <1>2. CASE Start = "any" <2>0. /\ pk \in [Passkeys -> Statuses] /\ pk[FirstOwner] = "active" /\ \A x \in Intruders : 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 \in Approvers /\ pk[p] \in {"active", "revoked"} /\ payees \in SUBSET (Tenants \X GoodAccounts) /\ ak \in [Keys -> Statuses] /\ \A k \in RootKeys : ak[k] = "pending" /\ akT \in [Keys -> SUBSET Tenants] /\ setups = 1 BY <1>2 DEF Init <2>1. own[FirstOwner] /\ \A x \in Intruders : ~own[x] BY <2>0 <2>2. TypeAuth BY <2>0 DEF TypeAuth, Accounts <2>3. \A x \in Intruders, t \in Tenants : grant[x, t] = 0 BY <2>0 <2>4. AttackerOut /\ OwnerFlags /\ GoodPayees BY <2>0, <2>1, <2>3 DEF AttackerOut, Out, OwnerFlags, GoodPayees <2>5. SetupInv BY <2>0, <2>1 DEF SetupInv, SetupClosed, ActiveOwners <2> QED BY <1>1, <2>0, <2>2, <2>4, <2>5 DEF Inv <1>3. CASE Start = "granted" <2>0. /\ pk \in [Passkeys -> Statuses] /\ pk[FirstOwner] = "active" /\ \A x \in Intruders : pk[x] = "pending" /\ own = [p \in Passkeys |-> p \in Owners /\ pk[p] = "active"] /\ grant = [pt \in Passkeys \X Tenants |-> IF pt[1] \in Approvers THEN MaxAmount ELSE 0] /\ payees = Tenants \X GoodAccounts /\ ak = [key \in Keys |-> IF key \in ArbiterKeys THEN "active" ELSE "pending"] /\ akT = [key \in Keys |-> IF key \in ArbiterKeys THEN Tenants ELSE {}] /\ setups = 1 BY <1>3 DEF Init <2>1. own[FirstOwner] /\ \A x \in Intruders : ~own[x] BY <2>0 <2>2. TypeAuth BY <2>0 DEF TypeAuth, Accounts <2>3. \A x \in Intruders, t \in Tenants : grant[x, t] = 0 BY <2>0 <2>4. \A k \in RootKeys : ak[k] = "pending" BY <2>0 <2>5. AttackerOut /\ OwnerFlags /\ GoodPayees BY <2>0, <2>1, <2>3, <2>4 DEF AttackerOut, Out, OwnerFlags, GoodPayees <2>6. SetupInv BY <2>0, <2>1 DEF SetupInv, SetupClosed, ActiveOwners <2> QED BY <1>1, <2>0, <2>2, <2>5, <2>6 DEF Inv <1>4. CASE Start = "setup" <2>0. /\ pk = [p \in Passkeys |-> IF p \in Intruders THEN "pending" ELSE "none"] /\ own = [p \in Passkeys |-> FALSE] /\ grant = [pt \in Passkeys \X Tenants |-> 0] /\ payees = {} /\ ak = [key \in Keys |-> IF key \in RootKeys THEN "pending" ELSE "none"] /\ akT = [key \in Keys |-> {}] /\ setups = 0 BY <1>4 DEF Init <2>1. TypeAuth /\ AttackerOut /\ OwnerFlags /\ GoodPayees /\ SetupInv BY <2>0 DEF TypeAuth, AttackerOut, Out, OwnerFlags, GoodPayees, SetupInv <2> QED BY <1>1, <2>0, <2>1 DEF Inv <1>5. CASE Start = "empty" <2>0. /\ pk = [p \in Passkeys |-> "none"] /\ own = [p \in Passkeys |-> FALSE] /\ grant = [pt \in Passkeys \X Tenants |-> 0] /\ payees = {} /\ ak = [key \in Keys |-> "none"] /\ akT = [key \in Keys |-> {}] /\ setups = 0 BY <1>5 DEF Init <2>1. TypeAuth /\ AttackerOut /\ OwnerFlags /\ GoodPayees /\ SetupInv BY <2>0 DEF TypeAuth, AttackerOut, Out, OwnerFlags, GoodPayees, SetupInv <2> QED BY <1>1, <2>0, <2>1 DEF Inv <1> QED BY <1>2, <1>3, <1>4, <1>5 ----------------------------------------------------------------------------- (* Every step keeps Inv *) LEMMA NextInv == Inv /\ [Next]_vars => Inv' <1> SUFFICES ASSUME Inv, [Next]_vars PROVE Inv' OBVIOUS <1> USE Assumptions, Basics DEF Inv, TypeAuth, TypeRest, OpsInv, AttackerOut, Out, OwnerFlags, GoodPayees, SetupInv, DecInv <1>1. CASE Tick BY <1>1 DEF Tick, calls, history, SetupClosed, ActiveOwners <1>2. CASE Setup <2>0. setups = 0 BY <1>2 DEF Setup <2>1. FirstOwner \in Passkeys /\ FirstOwner \notin Intruders OBVIOUS <2>2. /\ pk' = [pk EXCEPT ![FirstOwner] = "active"] /\ own' = [own EXCEPT ![FirstOwner] = TRUE] /\ setups' = 1 /\ broken' = broken /\ UNCHANGED <> BY <1>2, <2>0 DEF Setup, calls <2>3. SetupClosed' /\ ActiveOwners' # {} BY <2>1, <2>2 DEF SetupClosed, ActiveOwners <2>4. TypeAuth' BY <2>1, <2>2 <2>5. (TypeRest /\ OpsInv /\ DecInv /\ broken = {})' BY <2>2 <2>6. AttackerOut' BY <2>1, <2>2 <2>7. OwnerFlags' BY <2>1, <2>2 <2>8. GoodPayees' BY <2>2 <2>9. SetupInv' BY <2>2, <2>3 <2> QED BY <2>4, <2>5, <2>6, <2>7, <2>8, <2>9 <1>3. CASE \E p \in Passkeys : Register(p) <2> PICK p \in Passkeys : Register(p) BY <1>3 <2>1. p \in Passkeys /\ ~own[p] /\ pk[p] = "none" BY DEF Register <2>2. /\ pk' = [pk EXCEPT ![p] = "pending"] /\ UNCHANGED <> BY DEF Register, calls, history <2>3. SetupClosed' = SetupClosed /\ ActiveOwners' = ActiveOwners BY <2>1, <2>2 DEF SetupClosed, ActiveOwners <2>4. TypeAuth' BY <2>1, <2>2 <2>5. (TypeRest /\ OpsInv /\ DecInv /\ broken = {})' BY <2>2 <2>6. AttackerOut' BY <2>1, <2>2 <2>7. OwnerFlags' BY <2>1, <2>2 <2>8. GoodPayees' BY <2>2 <2>9. SetupInv' BY <2>2, <2>3 <2> QED BY <2>4, <2>5, <2>6, <2>7, <2>8, <2>9 <1>4. CASE \E key \in Keys : RegisterKey(key) <2> PICK key \in Keys : RegisterKey(key) BY <1>4 <2>1. /\ ak' = [ak EXCEPT ![key] = "pending"] /\ UNCHANGED <> BY DEF RegisterKey, calls, history <2>2. (TypeAuth /\ AttackerOut /\ GoodPayees)' BY <2>1 <2>3. (TypeRest /\ OpsInv /\ DecInv /\ broken = {} /\ OwnerFlags /\ SetupInv)' BY <2>1 DEF SetupClosed, ActiveOwners <2> QED BY <2>2, <2>3 <1>5. CASE OwnerSigns <2> PICK h \in Owners, op \in GoodOps : Sign(h, op) BY <1>5 DEF OwnerSigns <2> GoodOp(op) BY GoodOpsAreGood <2> QED BY DEF Sign, OpCheckOk, history, SetupClosed, ActiveOwners <1>6. CASE AttackerReplaysOp <2> PICK s \in loggedOps : Replay(s) BY <1>6 DEF AttackerReplaysOp <2> QED BY DEF Replay, OpCheckOk, gate, history, SetupClosed, ActiveOwners <1>7. CASE ChangeApplied <2> PICK s \in opCalls : OpTxn(s) BY <1>7 DEF ChangeApplied <2> DEFINE sop == s.op <2>1. GoodOp(sop) /\ s.by \in Owners /\ s.id \in Nat OBVIOUS <2>2. CASE ~(s.id \notin used /\ pk[s.by] = "active" /\ own[s.by] /\ Pre(sop)) BY <2>2 DEF OpTxn, history, SetupClosed, ActiveOwners <2>3. CASE s.id \notin used /\ pk[s.by] = "active" /\ own[s.by] /\ Pre(sop) <3> USE <2>3 <3>1. /\ pk' = CASE sop.do = "activate" -> [pk EXCEPT ![sop.p] = "active"] [] sop.do = "revoke" -> [pk EXCEPT ![sop.p] = "revoked"] [] OTHER -> pk /\ own' = IF sop.do = "activate" THEN [own EXCEPT ![sop.p] = sop.owner] ELSE own /\ grant' = CASE sop.do = "grant" -> [grant EXCEPT ![sop.p, sop.t] = sop.max] [] sop.do = "ungrant" -> [grant EXCEPT ![sop.p, sop.t] = 0] [] OTHER -> grant /\ payees' = CASE sop.do = "payee" -> payees \cup {<>} [] sop.do = "unpayee" -> payees \ {<>} [] OTHER -> payees /\ ak' = CASE sop.do = "arbiter" -> [ak EXCEPT ![sop.key] = "active"] [] sop.do = "unarbiter" -> [ak EXCEPT ![sop.key] = "revoked"] [] OTHER -> ak /\ akT' = IF sop.do = "arbiter" THEN [akT EXCEPT ![sop.key] = sop.ts] ELSE akT /\ used' = used \cup {s.id} /\ loggedOps' = loggedOps \cup {s} /\ opCalls' = opCalls \ {s} /\ UNCHANGED <> BY DEF OpTxn, history (* The parts of Inv that no change of authority touches. *) <3>2. (TypeRest /\ OpsInv /\ DecInv /\ broken = {})' BY <2>1, <3>1 (* A change that leaves passkeys alone keeps the owner flags and setup's parts. *) <3>3. ASSUME pk' = pk, own' = own PROVE (OwnerFlags /\ SetupInv)' BY <3>1, <3>3 DEF SetupClosed, ActiveOwners <3>4. CASE sop.do = "activate" <4>1. pk[sop.p] = "pending" BY <3>4 DEF Pre <4>2. sop.p \in Honest /\ (sop.owner => sop.p \in Owners) /\ sop.owner \in BOOLEAN BY <2>1, <3>4 DEF GoodOp, Honest <4>3. sop.p \in Passkeys /\ sop.p \notin Intruders BY <4>2 <4>4. /\ pk' = [pk EXCEPT ![sop.p] = "active"] /\ own' = [own EXCEPT ![sop.p] = sop.owner] /\ UNCHANGED <> BY <3>1, <3>4 <4>5. TypeAuth' BY <4>2, <4>3, <4>4 <4>8. AttackerOut' BY <4>3, <4>4 <4>9. OwnerFlags' BY <4>2, <4>3, <4>4 <4>10. GoodPayees' BY <4>4 <4>6. ASSUME setups = 1 PROVE SetupClosed' <5>1. PICK q \in Passkeys : own[q] /\ pk[q] \in {"active", "revoked"} BY <4>6 DEF SetupClosed <5>2. q # sop.p BY <5>1, <4>1 <5> QED BY <5>1, <5>2, <4>4 DEF SetupClosed <4>7. ASSUME setups = 1 PROVE ActiveOwners' # {} <5>1. PICK q \in ActiveOwners : TRUE BY <4>7 <5>2. q \in Passkeys /\ own[q] /\ pk[q] = "active" /\ q # sop.p BY <5>1, <4>1 DEF ActiveOwners <5> QED BY <5>2, <4>4 DEF ActiveOwners <4> QED BY <3>1, <3>2, <4>5, <4>6, <4>7, <4>8, <4>9, <4>10 <3>5. CASE sop.do = "revoke" <4>1. sop.p \in Passkeys BY <2>1, <3>5 DEF GoodOp <4>2. /\ pk[sop.p] \in {"pending", "active"} /\ ~(own[sop.p] /\ pk[sop.p] = "active" /\ Cardinality(ActiveOwners) <= 1) BY <3>5 DEF Pre <4>3. sop.p \in Passkeys BY <4>1 <4>4. /\ pk' = [pk EXCEPT ![sop.p] = "revoked"] /\ own' = own /\ UNCHANGED <> BY <3>1, <3>5 <4>5. TypeAuth' BY <4>3, <4>4 <4>8. AttackerOut' BY <4>3, <4>4 <4>9. OwnerFlags' BY <4>3, <4>4 <4>10. GoodPayees' BY <4>4 <4>6. ASSUME setups = 1 PROVE SetupClosed' <5>1. PICK q \in Passkeys : own[q] /\ pk[q] \in {"active", "revoked"} BY <4>6 DEF SetupClosed <5> QED BY <5>1, <4>4 DEF SetupClosed <4>7. ASSUME setups = 1 PROVE ActiveOwners' # {} <5>1. \E q \in ActiveOwners : q # sop.p <6>1. CASE own[sop.p] /\ pk[sop.p] = "active" <7> SUFFICES ASSUME \A q \in ActiveOwners : q = sop.p PROVE FALSE OBVIOUS <7>1. ActiveOwners = {sop.p} BY <4>3, <6>1 DEF ActiveOwners <7>2. Cardinality({sop.p}) = 1 BY FS_Singleton <7> QED BY <4>2, <6>1, <7>1, <7>2 <6>2. CASE ~(own[sop.p] /\ pk[sop.p] = "active") <7>1. PICK q \in ActiveOwners : TRUE BY <4>7 <7> QED BY <6>2, <7>1 DEF ActiveOwners <6> QED BY <6>1, <6>2 <5>2. PICK q \in ActiveOwners : q # sop.p BY <5>1 <5> QED BY <5>2, <4>4 DEF ActiveOwners <4> QED BY <3>1, <3>2, <4>5, <4>6, <4>7, <4>8, <4>9, <4>10 <3>6. CASE sop.do = "grant" <4>1. sop.p \in Approvers /\ sop.t \in Tenants /\ sop.max \in 0..MaxAmount BY <2>1, <3>6 DEF GoodOp, Amounts <4>2. /\ grant' = [grant EXCEPT ![sop.p, sop.t] = sop.max] /\ UNCHANGED <> BY <3>1, <3>6 <4>3. sop.p \in Passkeys /\ sop.p \notin Intruders BY <4>1 DEF Honest <4>4. grant' \in [Passkeys \X Tenants -> 0..MaxAmount] BY <4>1, <4>2, <4>3 <4>5. \A x \in Intruders, t \in Tenants : grant'[x, t] = 0 BY <4>1, <4>2, <4>3 <4>6. (TypeAuth /\ AttackerOut /\ GoodPayees)' BY <4>2, <4>4, <4>5 <4>7. (OwnerFlags /\ SetupInv)' BY <3>3, <4>2 <4> QED BY <3>2, <4>6, <4>7 <3>7. CASE sop.do = "ungrant" <4>1. sop.p \in Approvers /\ sop.t \in Tenants BY <2>1, <3>7 DEF GoodOp <4>2. /\ grant' = [grant EXCEPT ![sop.p, sop.t] = 0] /\ UNCHANGED <> BY <3>1, <3>7 <4>3. sop.p \in Passkeys /\ sop.p \notin Intruders BY <4>1 DEF Honest <4>4. grant' \in [Passkeys \X Tenants -> 0..MaxAmount] BY <4>1, <4>2, <4>3 <4>5. \A x \in Intruders, t \in Tenants : grant'[x, t] = 0 BY <4>1, <4>2, <4>3 <4>6. (TypeAuth /\ AttackerOut /\ GoodPayees)' BY <4>2, <4>4, <4>5 <4>7. (OwnerFlags /\ SetupInv)' BY <3>3, <4>2 <4> QED BY <3>2, <4>6, <4>7 <3>8. CASE sop.do = "payee" <4>1. sop.t \in Tenants /\ sop.acct \in GoodAccounts BY <2>1, <3>8 DEF GoodOp <4>2. /\ payees' = payees \cup {<>} /\ UNCHANGED <> BY <3>1, <3>8 <4> QED BY <3>2, <3>3, <4>1, <4>2 DEF Accounts <3>9. CASE sop.do = "unpayee" <4>1. /\ payees' = payees \ {<>} /\ UNCHANGED <> BY <3>1, <3>9 <4> QED BY <3>2, <3>3, <4>1 <3>10. CASE sop.do = "arbiter" <4>1. sop.key \in ArbiterKeys /\ sop.ts \subseteq Tenants BY <2>1, <3>10 DEF GoodOp <4>2. /\ ak' = [ak EXCEPT ![sop.key] = "active"] /\ akT' = [akT EXCEPT ![sop.key] = sop.ts] /\ UNCHANGED <> BY <3>1, <3>10 <4>3. sop.key \in Keys /\ sop.key \notin RootKeys BY <4>1 <4>4. /\ ak' \in [Keys -> Statuses] /\ akT' \in [Keys -> SUBSET Tenants] /\ \A k \in RootKeys : ak'[k] = ak[k] BY <4>1, <4>2, <4>3 <4>5. (TypeAuth /\ AttackerOut /\ GoodPayees)' BY <4>2, <4>4 <4>6. (OwnerFlags /\ SetupInv)' BY <3>3, <4>2 <4> QED BY <3>2, <4>5, <4>6 <3>11. CASE sop.do = "unarbiter" <4>1. sop.key \in Keys BY <2>1, <3>11 DEF GoodOp <4>2. /\ ak' = [ak EXCEPT ![sop.key] = "revoked"] /\ UNCHANGED <> BY <3>1, <3>11 <4>3. sop.key \in Keys BY <4>1 <4>4. /\ ak' \in [Keys -> Statuses] /\ \A k \in RootKeys : ak'[k] \in Out BY <4>2, <4>3 <4>5. (TypeAuth /\ AttackerOut /\ GoodPayees)' BY <4>2, <4>4 <4>6. (OwnerFlags /\ SetupInv)' BY <3>3, <4>2 <4> QED BY <3>2, <4>5, <4>6 <3> QED BY <2>1, <3>4, <3>5, <3>6, <3>7, <3>8, <3>9, <3>10, <3>11 DEF GoodOp <2> QED BY <2>2, <2>3 <1>8. CASE RequestChecked <2> PICK r \in ReqIds, b \in Bodies : IntakeCheck(r, b) BY <1>8 DEF RequestChecked <2> QED BY DEF IntakeCheck, gate, history, SetupClosed, ActiveOwners <1>9. CASE RequestRecorded <2> PICK c \in inCalls : IntakeTxn(c) BY <1>9 DEF RequestRecorded <2>1. CASE rS[c.r] = "none" <3>1. c.r \notin approved BY <2>1 <3> QED BY <2>1, <3>1 DEF IntakeTxn, history, SetupClosed, ActiveOwners, RStatuses <2>2. CASE rS[c.r] # "none" BY <2>2 DEF IntakeTxn, history, SetupClosed, ActiveOwners <2> QED BY <2>1, <2>2 <1>10. CASE RequestExpires <2> PICK r \in ReqIds : Expire(r) BY <1>10 DEF RequestExpires <2> QED BY DEF Expire, calls, history, SetupClosed, ActiveOwners, RStatuses <1>11. CASE PersonSigns <2> PICK h \in Honest, r \in ReqIds, d \in Decisions : PersonDecides(h, r, d) BY <1>11 DEF PersonSigns <2>1. Terms(r, d).r = r BY DEF Terms <2> QED BY <2>1 DEF PersonDecides, DecCheck, gate, history, SetupClosed, ActiveOwners <1>12. CASE AttackerSendsSig <2> PICK r \in ReqIds, d \in Decisions : \E s \in loggedDecs \cup {[pk |-> x, terms |-> Terms(r, d), chosen |-> None] : x \in Intruders} : AttackerDecides(s, r, d) BY <1>12 DEF AttackerSendsSig <2> PICK s \in loggedDecs \cup {[pk |-> x, terms |-> Terms(r, d), chosen |-> None] : x \in Intruders} : AttackerDecides(s, r, d) OBVIOUS <2>1. s \in loggedDecs BY DEF AttackerDecides, DecCheck <2>2. Terms(r, d).r = r BY DEF Terms <2>3. s.terms = Terms(r, d) BY DEF AttackerDecides, DecCheck <2> QED BY <2>1, <2>2, <2>3 DEF AttackerDecides, DecCheck, gate, history, SetupClosed, ActiveOwners <1>13. CASE DecisionRecorded <2> PICK c \in decCalls : DecTxn(c) BY <1>13 DEF DecisionRecorded <2> DEFINE cr == c.r cp == c.sig.pk cd == c.d cb == rB[cr] <2>1. cr \in ReqIds /\ cd \in Decisions /\ cp \in Honest /\ c.sig.chosen = cr /\ c.sig.terms.r = cr OBVIOUS <2>2. CASE ~(rS[cr] = "pending" /\ cb.exp >= now /\ pk[cp] = "active" /\ GrantOk(cp, cr, cd) /\ StandingOk(cr, cd)) BY <2>2 DEF DecTxn, SetupClosed, ActiveOwners <2>3. CASE rS[cr] = "pending" /\ cb.exp >= now /\ pk[cp] = "active" /\ GrantOk(cp, cr, cd) /\ StandingOk(cr, cd) <3> USE <2>3 <3>1. cr \notin approved /\ cb \in Bodies OBVIOUS <3>2. cd = "approve" => InForce(cp, cb) /\ cb.acct \in GoodAccounts BY <3>1 DEF GrantOk, StandingOk, InForce, Bodies <3>3. CASE cd = "approve" <4> USE <3>3 <4>1. /\ rS' = [rS EXCEPT ![cr] = "executing"] /\ loggedDecs' = loggedDecs \cup {c.sig} /\ effects' = effects \cup {[r |-> cr, sig |-> c.sig]} /\ approved' = approved \cup {cr} /\ broken' = broken /\ decCalls' = decCalls \ {c} /\ UNCHANGED <> BY <3>1, <3>2 DEF DecTxn <4> QED BY <2>1, <3>1, <3>2, <4>1 DEF SetupClosed, ActiveOwners, RStatuses <3>4. CASE cd = "reject" <4> USE <3>4 <4>1. /\ rS' = [rS EXCEPT ![cr] = "rejected"] /\ loggedDecs' = loggedDecs \cup {c.sig} /\ UNCHANGED <> /\ decCalls' = decCalls \ {c} /\ UNCHANGED <> BY DEF DecTxn <4> QED BY <2>1, <3>1, <4>1 DEF SetupClosed, ActiveOwners, RStatuses <3> QED BY <2>1, <3>3, <3>4 DEF Decisions <2> QED BY <2>2, <2>3 <1>14. CASE PaymentSent <2> PICK e \in effects : Effect(e) BY <1>14 DEF PaymentSent <2> QED BY DEF Effect, SetupClosed, ActiveOwners, RStatuses <1>15. CASE UNCHANGED vars BY <1>15 DEF vars, gate, calls, history, SetupClosed, ActiveOwners <1> QED BY <1>1, <1>2, <1>3, <1>4, <1>5, <1>6, <1>7, <1>8, <1>9, <1>10, <1>11, <1>12, <1>13, <1>14, <1>15 DEF Next THEOREM InvAlways == Spec => []Inv BY InitInv, NextInv, PTL DEF Spec ----------------------------------------------------------------------------- (* The properties *) THEOREM G1_G2_G3_Invariants == Spec => [](/\ G1_ApprovedWithAuthorityInForce /\ G1_PaidOnlyAsAPersonApproved /\ G1_PaidOnlyToListedPayees /\ G2_AtMostOnce /\ G3_SetupOnce /\ G3_AlwaysAnOwner /\ G3_AttackerNeverGranted) <1>1. Inv => /\ G1_ApprovedWithAuthorityInForce /\ G1_PaidOnlyAsAPersonApproved /\ G1_PaidOnlyToListedPayees /\ G2_AtMostOnce /\ G3_SetupOnce /\ G3_AlwaysAnOwner /\ G3_AttackerNeverGranted BY DEF Inv, TypeRest, AttackerOut, Out, SetupInv, G1_ApprovedWithAuthorityInForce, G1_PaidOnlyAsAPersonApproved, G1_PaidOnlyToListedPayees, G2_AtMostOnce, G3_SetupOnce, G3_AlwaysAnOwner, G3_AttackerNeverGranted <1> QED BY InvAlways, <1>1, PTL (* 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. *) AuthorityStep == 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 LEMMA StepAuthority == Inv /\ [Next]_vars => [AuthorityStep]_vars <1> SUFFICES ASSUME Inv, [Next]_vars PROVE [AuthorityStep]_vars OBVIOUS <1> USE Assumptions, Basics DEF Inv, TypeAuth, TypeRest, SetupInv <1>0. ASSUME UNCHANGED <> PROVE AuthorityStep BY <1>0 DEF AuthorityStep, Authority, ActiveOwners <1>1. CASE Tick BY <1>1, <1>0 DEF Tick <1>2. CASE Setup BY <1>2 DEF Setup, AuthorityStep <1>3. CASE \E p \in Passkeys : Register(p) <2> PICK p \in Passkeys : Register(p) BY <1>3 <2>1. {q \in Passkeys : pk'[q] = "active"} = {q \in Passkeys : pk[q] = "active"} BY DEF Register <2>2. ActiveOwners' = ActiveOwners BY DEF Register, ActiveOwners <2> QED BY <2>1, <2>2 DEF Register, AuthorityStep, Authority <1>4. CASE \E key \in Keys : RegisterKey(key) <2> PICK key \in Keys : RegisterKey(key) BY <1>4 <2>1. {kk \in Keys : ak'[kk] = "active"} = {kk \in Keys : ak[kk] = "active"} BY DEF RegisterKey <2> QED BY <2>1 DEF RegisterKey, AuthorityStep, Authority, ActiveOwners <1>5. CASE OwnerSigns BY <1>5, <1>0 DEF OwnerSigns, Sign <1>6. CASE AttackerReplaysOp BY <1>6, <1>0 DEF AttackerReplaysOp, Replay, gate <1>7. CASE ChangeApplied <2> PICK s \in opCalls : OpTxn(s) BY <1>7 DEF ChangeApplied <2>1. CASE s.id \notin used /\ pk[s.by] = "active" /\ own[s.by] /\ Pre(s.op) <3>1. used' = used \cup {s.id} BY <2>1 DEF OpTxn <3> QED BY <2>1, <3>1 DEF AuthorityStep <2>2. CASE ~(s.id \notin used /\ pk[s.by] = "active" /\ own[s.by] /\ Pre(s.op)) BY <2>2, <1>0 DEF OpTxn <2> QED BY <2>1, <2>2 <1>8. CASE RequestChecked BY <1>8, <1>0 DEF RequestChecked, IntakeCheck, gate <1>9. CASE RequestRecorded BY <1>9, <1>0 DEF RequestRecorded, IntakeTxn <1>10. CASE RequestExpires BY <1>10, <1>0 DEF RequestExpires, Expire <1>11. CASE PersonSigns BY <1>11, <1>0 DEF PersonSigns, PersonDecides, gate <1>12. CASE AttackerSendsSig BY <1>12, <1>0 DEF AttackerSendsSig, AttackerDecides, gate <1>13. CASE DecisionRecorded BY <1>13, <1>0 DEF DecisionRecorded, DecTxn <1>14. CASE PaymentSent BY <1>14, <1>0 DEF PaymentSent, Effect <1>15. CASE UNCHANGED vars BY <1>15 DEF vars, gate, calls, history <1> QED BY <1>1, <1>2, <1>3, <1>4, <1>5, <1>6, <1>7, <1>8, <1>9, <1>10, <1>11, <1>12, <1>13, <1>14, <1>15 DEF Next THEOREM G3_Steps == Spec => G3_AuthorityOnlyByOwners <1>1. Spec => [][AuthorityStep]_vars BY InvAlways, StepAuthority, PTL DEF Spec <1> QED BY <1>1 DEF G3_AuthorityOnlyByOwners, AuthorityStep =============================================================================