I have the full picture. I've verified the ontology constraints against mc.ttl, mc-policy.ttl, and the Black Basta ABox worked example. Now I'll author the card layer, faithful to the TBox and firewalled from the incident. # ARM-B CARD LAYER — S3: Kerberoasting to lateral movement > Doctrine reference. Maneuver space + control inventory + coverage relations for this environment. No incident content. > *Reading key (MC vocabulary, glossed for the responder): **maneuver** = a behavior identified by its observable effect, in Hoare-triple shape; **invariant core** = the part of the mechanism the adversary can't drop without abandoning the goal (carries identity); **implementation variant** = a specific realization of that core; **observable** = a telemetry-visible signal a mechanism manifests as, carrying a **robustness** grade L1–L5 (StP; how hard to evade — a **ceiling** on any analytic keyed on it); **detect-face** (Detectability) = the face a detection acts on, with four-valued health live/degraded/blind/uncertain, a `sourcedFrom` control, and typed `triggerDependsOn`(lose→blind) / `enrichmentDependsOn`(lose→degraded) edges; **coverage** = a DERIVED verdict (covered/notCovered), never asserted. Robustness-graded admission (count covered only at observable rank ≥ 4 / StP-L4) is a policy overlay.* --- ## A. Maneuver cards ### A1 — Kerberoast (service-ticket harvest for offline cracking) — AUTHORED **Identifying observable effect.** A single domain principal requests Kerberos service tickets (TGS) for **many distinct service principals it never itself authenticates to**, harvesting ticket material whose encryption is derived from the target service account's password — for offline recovery elsewhere. The maneuver is named by *this effect* (anomalous service-ticket harvest), not by any tool (Rubeus / GetUserSPNs / PowerView / mimikatz are variants, not the identity). **Maneuver record.** `mKerberoast` · serves `objCredentialAccess` (TA0006) · `attackTechniqueId "T1558.003"` · one invariant core (below). **Hoare triple.** - **Precondition (EXPRESSIBLE):** the requesting account holds a valid user-level domain credential — `credentialHeld ⊒ credUser` (opSubsumes) on the requester role. Any authenticated domain principal can request service tickets; no privilege is required. This is the teeth of the behavior: the precondition is an *authorized* protocol position. - **Mechanism (invariant core):** `coreKerbHarvest` = "request service tickets for service principals the requester does not use, to obtain password-derived crackable ticket material." Emits a TGS-REQ (4769) per targeted SPN — a forced, unavoidable manifestation (MC-A8). - **Postcondition (INEXPRESSIBLE — see D1/D3):** the intended effect is "attacker now holds an offline-crackable service ticket for the target service account." No faithful fluent write exists: there is no `credentialHeld` value for *encrypted-but-not-yet-usable* ticket material, and its holder is off-environment. **The card carries this maneuver by its objective + invariant core (MC-A1 identity), not by a postcondition.** Do not read a `credAdmin` yield here — the request alone confers nothing usable. **Invariant core + variants.** - Invariant core `coreKerbHarvest` (identity): the TGS-REQ-for-unused-SPN harvest. Manifests the **spanning** observable `obsSpnHarvest` regardless of tool or enc-type. - Variant `varRc4Downgrade`: forces RC4 (enc-type 0x17) so the ticket is cheap to crack offline. Additionally manifests the **discriminating** observable `obsRc4EncType`. - Variant `varAesRoast`: requests without forcing RC4 (AES tickets; costlier crack). Manifests **only** `obsSpnHarvest` — it does **not** produce `obsRc4EncType`. - Both variants compose the same primitive "request service ticket for a service principal"; the invariant is their intersection (the harvest), which is what a robust detection must key on. **Robustness of the key observables (ceiling semantics — grades the analytic, not the event).** - `obsRc4EncType` — "TGS-REQ carrying RC4 (0x17)" — **L2 (configurable).** Enc-type is an adversary-choosable request parameter; any analytic keyed here caps at L2 and evaporates the moment the adversary requests AES. *Discriminating* (present only for `varRc4Downgrade`). - `obsSpnHarvest` — "one principal requests TGS for many SPNs it never authenticates to" — **L4 (core-behavior).** Bound to the maneuver's required behavior — to obtain crackable ticket material you *must* request the tickets — so evadable only by substantial tradecraft change (low-and-slow spreading of volume). *Spanning* (fires regardless of variant/enc-type). NB: the bare TGS-REQ *emission* is an L5 chokepoint (you cannot Kerberoast without it), but a single 4769 is indistinguishable from ordinary service use, so the *deployable* analytic sits at the volume/diversity L4 rung. **Linked detect-faces.** - `dfKerbRc4` — **DEPLOYED.** `sourcedFrom` AD-SIEM (B1); `dependencyLogic required`; reads `obsRc4EncType` → **ceiling L2**; faceStatus **live** (AD-SIEM enforcing). This is the one deployed analytic; it observes only the RC4 variant. - `dfKerbVolume` — **AUTHORABLE BUT NOT DEPLOYED.** Would read the spanning `obsSpnHarvest` → ceiling L4 (would clear the policy admission rank). No control in this environment sources it → the **invariant rung is uncovered** (see C1). This is the missing backstop. --- ### A2 — AS-REP roasting (sibling family card) — AUTHORED (doctrine), UNCOVERED here **Identifying observable effect.** A principal requests AS-REP material (4768 AS-REQ) for domain accounts that have Kerberos pre-authentication disabled, harvesting password-derived material for offline recovery. Same *shape* as A1 (authorized-request → offline crack), different KDC exchange. **Maneuver record.** `mAsRepRoast` · serves `objCredentialAccess` (TA0006) · `attackTechniqueId "T1558.004"` · invariant core `coreAsRepHarvest` = "request AS-REP for pre-auth-disabled accounts to obtain crackable material." **Postcondition INEXPRESSIBLE** (same crackable-material gap as A1, D3). **Why it is in the library, and its coverage here.** A mature MC shop keeps this sibling because the family generalizes past the RC4/4769 path. **In THIS environment it is uncovered:** the only deployed Kerberos analytic keys on 4769 (service-ticket) events; no 4768/AS-REP analytic is deployed → no detect-face → **notCovered / SILENT** (see C2). Included to keep the family maximal, not because the environment observes it. --- ### A3 — Valid-credential logon / lateral movement to the crown-jewel host — STUB (identity unmodeled; one authored face) **No faithful maneuver record — unmodeled path (position change).** The behavior's defining effect is "the adversary now executes on a *new host*" — a change of **position**. The TBox has no location fluent for a process, and `reachability` is a *static precondition between positions* (Channel), not a maneuver that moves a token onto a new host (see D4). Authoring a maneuver whose postcondition is merely "process at user integrity" would misrepresent it (that already held) — so **no maneuver card is authored**. **The one piece that IS authored — the observation surface.** `dfSqlLogon` — a detect-face `sourcedFrom` SQL-EDR (B2) reading `obsSvcLogon` = "the SQL service account's network (type-3) logon to the crown-jewel host it serves." Robustness of `obsSvcLogon` ≈ **L2** on the evasion axis, but that axis *under-describes it*: its dominant weakness is **benign-indistinguishability**, not evadability (see below and D5). - **Model-derived status: live** (SQL-EDR enforcing, no severed dependency). - **True operational status: degraded-by-legitimacy** — a valid-credential logon by the account that *legitimately runs that service and holds local admin on that host* is not anomalous. The framework cannot represent this cause of degradation (D5), so the card, read at face value, **over-states** this face. Treat `dfSqlLogon` as a low-fidelity enrichment signal, never as coverage. Cross-reference: authorability report D4 (position change) and D5 (degradation-by-legitimacy). --- ### A4 — Offline off-environment ticket crack — STUB **No authored coverage record — unmodeled path.** The crack is a state change with **no in-environment entity, no observable, and no possible Detectability** (it occurs on adversary hardware that emits no telemetry into scope). It silently promotes harvested ticket material from "encrypted / crackable" to "usable plaintext service credential." mc-core binds state to `mc:Entity` = a persistent thing *in the environment* and binds mechanisms to *manifest* observables (MC-A8); neither holds here. **No maneuver, no detect-face, no coverage verdict is authored.** This is a **structural void by nature**, categorically different from a blinded detection face (see D2 — the headline framework gap). Detection of the overall chain must key **before** the crack (the A1 harvest face) or **after** it (the A3 logon surface) — never on the crack. --- ## B. Defensive control cards *Firewall note: the entities below (AD-SIEM, SQL-EDR, the crown-jewel SQL host, its SQL service account) are STANDING control/asset inventory and configuration facts — not incident events.* ### B1 — AD-SIEM (4769 correlation rule) - **What it is.** A SIEM correlation rule over Domain-Controller Windows Security logs. Modeled as `mc:Control` (`controlStatus` enforcing/impaired/killed). - **What it observes.** Kerberos service-ticket requests (4769), including the encryption-type field. It does **not** see endpoint activity. - **Detect-face it sources (trigger).** `dfKerbRc4` (A1) — as its **trigger** (`triggerDependsOn` the DC 4769 log feed). The deployed analytic is keyed on enc-type = RC4 (0x17) plus an N-distinct-SPN-in-window predicate; it reads the **L2** discriminating observable. - **Failure mode.** If AD-SIEM is **impaired/killed** (`degradesTelemetry true`), its trigger is severed → `dfKerbRc4` goes **blind** → `mKerberoast` becomes **notCovered** (it is the only deployed Kerberoast face). No enrichment-only edge exists, so there is no intermediate "degraded" state — impairment goes straight to blind. ### B2 — SQL-EDR (endpoint EDR on the crown-jewel SQL host) - **What it is.** Endpoint EDR on the high-value SQL/app server (process creation, logon, network telemetry). `mc:Control`. - **What it observes.** On-host process/logon/network events for that server. It does **not** observe DC/KDC ticket issuance (wrong control type for the A1 harvest). - **Detect-face it sources (trigger).** `dfSqlLogon` (A3) — as trigger. **Caveat:** the face's real degradation is by legitimacy, which the model cannot source from control state (D5); the SQL-EDR being healthy does not make this face trustworthy. - **Failure mode.** If SQL-EDR is **impaired/killed**, its trigger is severed → `dfSqlLogon` goes **blind** (the only on-host observation surface for the logon is lost). Note it is already only *nominally* live even when enforcing. ### B0 — Control-inventory gap (stated explicitly) **No control observes off-environment activity.** There is no `mc:Control`, and therefore no telemetry source and no Detectability, for the A4 crack. This is a standing inventory fact, not a tuning gap. --- ## C. Coverage relations *All verdicts DERIVED from detect-face health + sourcing-control state + policy admission rank (pol:coverageAdmissionRank = 4 / StP-L4). Never asserted.* ### C1 — `mKerberoast` × AD-SIEM - **Constitutive verdict: covered.** A surviving non-blind face (`dfKerbRc4`, live) observes the maneuver → CoverageRule yields **covered**. - **Policy-graded verdict: inadmissible / uncovered-at-grade.** `dfKerbRc4` reads `obsRc4EncType` at **L2 < rank 4** → it does **not** meet the admission threshold. The environment's coverage of Kerberoast is real but **L2-grade only**. - **Invariant rung: notCovered.** The spanning `obsSpnHarvest` (L4, which *would* admit) has **no deployed detect-face** (`dfKerbVolume` is authorable but unsourced). There is **no higher-robustness backstop in this environment.** - **Residual gap (what the coverage is blind to).** The deployed face is keyed on the discriminating RC4 observable, so it covers **only** `varRc4Downgrade`. `varAesRoast` (AES request) and low-and-slow harvesting **evade it to zero** — they never produce `obsRc4EncType`, and the spanning L4 face that would catch them is absent. - **Under impaired/killed AD-SIEM.** Trigger-loss → `dfKerbRc4` **blind** → `mKerberoast` **notCovered**. (Trigger-loss → blind → notCovered.) ### C2 — `mAsRepRoast` (family sibling) - **Verdict: notCovered / SILENT.** No deployed detect-face (no 4768/AS-REP analytic). Coverage is derivably absent — stated explicitly, not omitted. ### C3 — Lateral-movement logon surface × SQL-EDR - **No faithful maneuver-level verdict** — the maneuver identity (position change) is unmodeled (A3, D4). - **Face-level, model-derived: covered/live.** The rollup would report `dfSqlLogon` **live** because SQL-EDR is enforcing. - **Face-level, true: degraded-by-legitimacy.** The observable is indistinguishable from authorized service use (D5). **The model OVER-reports here** — the single most dangerous coverage misread in this scenario. Treat as low-confidence enrichment only. - **Under impaired/killed SQL-EDR.** Trigger-loss → `dfSqlLogon` **blind**. ### C4 — Offline crack - **Verdict: SILENT / underivable.** No maneuver, no face, no sourcing control → coverage cannot be derived. This is **not** `notCovered` in the blinded-face sense (which presupposes a face exists and is blind); it is a **structural void**. The model has no vocabulary to record the distinction (D2). **Coverage summary (this environment):** Kerberoast — covered@L2, policy-inadmissible, no L4 backstop; AES/low-slow variants uncovered. AS-REP roasting — notCovered. Lateral logon — over-reported live (truly degraded-by-legitimacy). Offline crack — SILENT/unmodeled. --- ## D. Card-authorability report (framework-gap channel) **D1 — Kerberoast identity strains against "act that changes state."** *Needed:* a maneuver whose identifying effect is an *authorized protocol request* that yields crackable ticket material. *Why the TBox can't carry it faithfully:* a `Maneuver` is "an act that changes state" whose postcondition writes a fluent (MC-A1 pairs identity with objective + invariant core, but the worked model always closes chains through a written yield). The Kerberoast request's postcondition ("holds a crackable service ticket") has no fluent to write (D3). The maneuver is authorable by objective + core, but **postcondition-less**. *What a card-reliant responder gets wrong/misses:* if they expect a `yieldsPattern`/`credAdmin` yield, they may either over-read the request as already conferring credentials, or discount the maneuver because it "doesn't complete a chain." The card must be read as identity-by-effect, not by yield. **D2 — Offline off-environment crack: state change outside the observed environment (HEADLINE GAP).** *Needed:* represent an occurrence that (a) writes state with no in-environment entity and (b) has no possible observable/Detectability, and distinguish it from a detection gap. *Why the TBox can't:* state lives on `mc:Entity` = "a persistent thing **in the environment**"; MC-A8 binds mechanisms to *manifest* observables. The CoverageRule derives `notCovered` only when a maneuver's face is **blind** — a face that *exists but is severed*. The crack has **no face at all**, which the four-valued model cannot distinguish from a blinded one. *What a card-reliant responder gets wrong/misses:* they will blur "unobservable by nature" into "we lost/lack a detector," implying the gap is closable by adding telemetry. It is not — no in-environment sensor can ever see it. The correct doctrine (key before/after, never on the crack) is not derivable from the card model; it must be stated in prose (A4), off-model. **D3 — Crackable-artifact credential state is inexpressible.** *Needed:* a `credentialHeld` value for "encrypted, offline-crackable ticket material that becomes a usable credential only after off-environment work." *Why the TBox can't:* `credentialHeld ∈ {credNone, credUser, credAdmin, credUserAdmin}` — usable-credential values only, on an in-environment `mc:Account`. There is no intermediate crackable/unusable value, and no off-environment holder. The request→crack→usable-credential edge therefore cannot thread through the `satisfies`/`unlocked` chain that closes every other chain in the worked ABox. *What a card-reliant responder gets wrong/misses:* the causal link from the harvest to the later usable-credential logon is invisible to the model — the two behaviors read as unconnected, obscuring that rotating the service credential is the invariant fix (it invalidates the harvested material). **D4 — Lateral movement as position change is unmodeled.** *Needed:* a maneuver whose effect is "the adversary now executes on a new host." *Why the TBox can't:* `reachability` is a *static precondition between positions* (a Channel property), not a movement. A process's *location* is not a fluent (integrity is on the process but encodes privilege, not host). Occurrences bind one process to one host via role-binding; there is no write that relocates it. *What a card-reliant responder gets wrong/misses:* the crown-jewel-reaching step has no maneuver card and no coverage verdict — a responder leaning on the cards sees only the (degraded) logon face and may not recognize lateral movement as a distinct, gradeable behavior at all. **D5 — Degradation-by-legitimacy has no home in the health model.** *Needed:* a face status for "trigger fires, but the observable is indistinguishable from authorized use." *Why the TBox can't:* the **only** modeled cause of `degraded`/`blind` is a lost `enrichmentDependsOn`/`triggerDependsOn` edge to an *impaired/killed Control*. A healthy control with an intrinsically ambiguous observable yields no status change → the rollup returns **live**. The four-valued `faceStatus` has no value for benign-indistinguishability, and fabricability/robustness sit on different axes that don't feed the health rollup. *What a card-reliant responder gets wrong/misses:* they will trust the SQL-EDR logon face as *live/covering* (C3) when it is operationally near-useless — over-crediting coverage of the lateral step precisely where it matters most, and possibly choosing host isolation over the invariant fix (rotate the service credential whose legitimacy is what degrades the face). --- ### Validation footer - **Cardinality / one invariant core per maneuver:** each authored maneuver (`mKerberoast`, `mAsRepRoast`) declares exactly one `via` invariant core; stubs (A3, A4) declare none by design. - **Robustness as observable ceiling:** all L-grades sit on observables (`obsRc4EncType` L2, `obsSpnHarvest` L4, `obsSvcLogon` ≈L2), never on maneuvers or faces; faces inherit the ceiling of what they read. - **Coverage derived, not asserted:** every verdict in Part C is presented as a derivation from face health + control state + policy admission; absences are stated as SILENT/underivable, never as invented coverage. - **No retired constructs:** uses *maneuver / invariant core / implementation variant / robustness (StP L1–L5) / detect-face (Detectability) / coverage / subsumes*. No AMC, ORTG, forcedness, chokepointCoupling, `covers`-as-coverage, `transition`-as-unit, or six-fork state model appears.