------------------------- MODULE CAINMCPGateAuthorization -------------------------
(***************************************************************************)
(* Bounded model of the CAIN-42 MCPGate consensus-authorization gate        *)
(* (platform-gateway/cain_pbft_enforcement.py, ConsensusAuthorizationGate). *)
(*                                                                         *)
(* The cluster (N = 4, f <= 1, quorum Q = 3) proposes authorization bodies; *)
(* honest members sign only proposed bodies, a Byzantine member signs any   *)
(* body. An attacker presents ANY body with ANY actual call: forged,        *)
(* replayed, expired, action-substituted, identity-substituted, or after    *)
(* the caller's security context changed. The gate executes only when:      *)
(*   - the body carries >= Q real signatures (certificate)                  *)
(*   - now < expiration                              (time_bound)          *)
(*   - executed action = authorized action           (action_continuity)   *)
(*   - caller = authorized identity                  (identity)            *)
(*   - caller's current context = authorized context (context continuity)  *)
(*   - the certificate id was never consumed         (single_use)          *)
(* and it consumes the id in the same step (before execution).             *)
(*                                                                         *)
(* Each Skip* flag removes one check, and Thresh < Q weakens the quorum:    *)
(* every such mutant MUST violate an invariant, or a pass means nothing.    *)
(*                                                                         *)
(* Scope: a bounded MODEL of the gate's rules, not the Python code.         *)
(* Capability scope is covered by action_continuity here (one resource per  *)
(* action); canonical hashing is abstracted as record equality.            *)
(***************************************************************************)
EXTENDS FiniteSets, Naturals

CONSTANTS Byz, Thresh, SkipExpiry, SkipAction, SkipIdentity, SkipContext, SkipReplay

Nodes   == {"n1", "n2", "n3", "n4"}
Honest  == Nodes \ Byz
Q       == 3
Actions == {"read", "delete"}
Actors  == {"alice", "mallory"}
Ctxs    == {"c1", "c2"}
Ids     == {1, 2}
MaxT    == 2
Bodies  == [id : Ids, act : Actions, who : Actors, ctx : Ctxs, exp : 1..MaxT]

ASSUME Byz \subseteq Nodes /\ Cardinality(Byz) <= 1 /\ Thresh \in 1..Q

VARIABLES proposed, votes, now, ctxOf, consumed, log

vars == <<proposed, votes, now, ctxOf, consumed, log>>

Init ==
  /\ proposed = {}
  /\ votes    = [h \in Honest |-> {}]
  /\ now      = 0
  /\ ctxOf    = [a \in Actors |-> "c1"]
  /\ consumed = {}
  /\ log      = {}

Signers(b) == {h \in Honest : b \in votes[h]} \cup Byz

\* The cluster proposes a body; certificate ids are unique per proposal.
Propose(b) ==
  /\ Cardinality(proposed) < 2
  /\ \A p \in proposed : p.id # b.id
  /\ proposed' = proposed \cup {b}
  /\ UNCHANGED <<votes, now, ctxOf, consumed, log>>

Vote(h, b) ==
  /\ b \in proposed /\ b \notin votes[h]
  /\ votes' = [votes EXCEPT ![h] = @ \cup {b}]
  /\ UNCHANGED <<proposed, now, ctxOf, consumed, log>>

Tick  == now < MaxT /\ now' = now + 1 /\ UNCHANGED <<proposed, votes, ctxOf, consumed, log>>

Drift(a, c) == ctxOf' = [ctxOf EXCEPT ![a] = c] /\ UNCHANGED <<proposed, votes, now, consumed, log>>

\* A call presents body b while actually doing act as caller who.
Present(b, act, who) ==
  /\ Cardinality(Signers(b)) >= Thresh
  /\ SkipExpiry   \/ now < b.exp
  /\ SkipAction   \/ act = b.act
  /\ SkipIdentity \/ who = b.who
  /\ SkipContext  \/ ctxOf[who] = b.ctx
  /\ SkipReplay   \/ b.id \notin consumed
  /\ consumed' = consumed \cup {b.id}
  /\ log' = log \cup {[body |-> b, act |-> act, who |-> who, ctx |-> ctxOf[who], t |-> now]}
  /\ UNCHANGED <<proposed, votes, now, ctxOf>>

Next ==
  \/ \E b \in Bodies : Propose(b)
  \/ \E h \in Honest, b \in Bodies : Vote(h, b)
  \/ Tick
  \/ \E a \in Actors, c \in Ctxs : Drift(a, c)
  \/ \E b \in Bodies, act \in Actions, who \in Actors : Present(b, act, who)

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

\* NO QUORUM -> NO EXECUTION: every executed body was signed by a quorum that
\* includes at least Q - |Byz| honest members, i.e. the cluster committed it.
NoExecWithoutQuorum == \A e \in log : Cardinality({h \in Honest : e.body \in votes[h]}) >= Q - Cardinality(Byz)
ActionBinding       == \A e \in log : e.act = e.body.act
IdentityBinding     == \A e \in log : e.who = e.body.who
ContextBinding      == \A e \in log : e.ctx = e.body.ctx
NotExpired          == \A e \in log : e.t < e.body.exp
SingleUse           == \A e1, e2 \in log : e1.body.id = e2.body.id => e1 = e2

TypeOK == now \in 0..MaxT /\ consumed \subseteq Ids /\ proposed \subseteq Bodies
=============================================================================
