"""Published standardized procedures, modeled as explicit-state machines for counterexample hunting. Each entry models a REAL, published IEEE 802.11 / 3GPP procedure and a named safety property, with its spec clause and (where applicable) a CITATION to a known finding. The foundry (scripts/hunt_counterexamples.py) runs the model checker and classifies each procedure HONESTLY from the result: * KNOWN_COUNTEREXAMPLE — the safety property is violated AND a published citation exists (e.g. the 802.11 4-way-handshake key reinstallation behind KRACK). * CANDIDATE_COUNTEREXAMPLE — the property is violated with NO published citation -> flagged "unconfirmed — needs expert review" (never asserted as a novel vuln). * PROVEN_SAFE — the property holds over all reachable states. `build()` models the procedure AS PUBLISHED; `build_fixed()` (when present) is the metadata-gated fix, included to show the counterexample is removable (and to seed a change-request). """ from . import ieee, cellular from .. import pqc_wifi, cxl_fwd # flagship models reused to reproduce documented cross-domain findings # name -> metadata. classification_hint is a sanity cross-check, NOT the source of truth (the verdict # is derived from the actual model-checking result + presence of a citation). PUBLISHED = { # ---------------- IEEE 802.11 ---------------- "ieee_4way_handshake_krack": { "build": ieee.four_way_handshake, "build_fixed": ieee.four_way_handshake_fixed, "property": "nonce_never_reused", "body": "IEEE", "spec": "IEEE 802.11-2020 §12.7.6 (4-way handshake) / IEEE 802.11i", "citation": "Vanhoef & Piessens, \"Key Reinstallation Attacks: Forcing Nonce Reuse in WPA2\", " "ACM CCS 2017; CVE-2017-13077..13088 (KRACK).", "known_finding": "Retransmitted/replayed EAPOL-Key msg3 triggers PTK reinstallation, resetting " "the TX nonce and replay counter -> nonce reuse.", "classification_hint": "KNOWN_COUNTEREXAMPLE", }, "ieee_ft_handshake_802_11r": { "build": ieee.ft_handshake, "property": "no_data_before_key_confirm", "body": "IEEE", "spec": "IEEE 802.11-2020 §13 (Fast BSS Transition)", "citation": None, "known_finding": None, "classification_hint": "PROVEN_SAFE", }, "ieee_mlo_tid_to_link": { "build": ieee.mlo_tid_to_link, "property": "no_tx_on_inactive_link", "body": "IEEE", "spec": "IEEE 802.11be/bn MLO TID-to-link mapping (§35)", "citation": None, "known_finding": None, "classification_hint": "PROVEN_SAFE", }, "ieee_block_ack_scoreboard": { "build": ieee.block_ack, "property": "no_duplicate_delivered", "body": "IEEE", "spec": "IEEE 802.11-2020 §10.25 (Block Ack reordering / scoreboard)", "citation": None, "known_finding": None, "classification_hint": "PROVEN_SAFE", }, "ieee_twt_wake_sleep": { "build": ieee.twt, "property": "no_delivery_while_asleep", "body": "IEEE", "spec": "IEEE 802.11ax/be Target Wake Time (§26.8)", "citation": None, "known_finding": None, "classification_hint": "PROVEN_SAFE", }, "ieee_uapsd_pspoll": { "build": ieee.uapsd, "property": "no_delivery_without_trigger", "body": "IEEE", "spec": "IEEE 802.11-2020 §11.2 (U-APSD / PS-Poll power save)", "citation": None, "known_finding": None, "classification_hint": "PROVEN_SAFE", }, "ieee_sa_query": { "build": ieee.sa_query, "property": "no_spoofed_disassoc_accepted", "body": "IEEE", "spec": "IEEE 802.11-2020 §11.3 / §12 (SA Query, protected management frames / 802.11w)", "citation": None, "known_finding": None, "classification_hint": "PROVEN_SAFE", }, "ieee_fils_auth": { "build": ieee.fils, "property": "no_data_before_key", "body": "IEEE", "spec": "IEEE 802.11ai Fast Initial Link Setup (§12.12)", "citation": None, "known_finding": None, "classification_hint": "PROVEN_SAFE", }, # ---------------- 3GPP ---------------- "3gpp_rrc_state_machine": { "build": cellular.rrc_state_machine, "property": "no_data_in_idle", "body": "3GPP", "spec": "3GPP TS 38.331 §4.2 (RRC states: IDLE/INACTIVE/CONNECTED)", "citation": None, "known_finding": None, "classification_hint": "PROVEN_SAFE", }, "3gpp_pdcp_reordering": { "build": cellular.pdcp_reordering, "property": "no_duplicate_delivered", "body": "3GPP", "spec": "3GPP TS 38.323 §5.2 (PDCP reordering / duplication discard)", "citation": None, "known_finding": None, "classification_hint": "PROVEN_SAFE", }, "3gpp_rlc_am_retx": { "build": cellular.rlc_am_retx, "property": "retx_bounded_no_runaway", "body": "3GPP", "spec": "3GPP TS 38.322 §5.2/§5.3 (RLC AM retransmission, maxRetxThreshold)", "citation": None, "known_finding": None, "classification_hint": "PROVEN_SAFE", }, "3gpp_drx_timers": { "build": cellular.drx_timers, "property": "awake_when_pdcch_expected", "body": "3GPP", "spec": "3GPP TS 38.321 §5.7 (DRX onDuration / inactivity / RTT timers)", "citation": None, "known_finding": None, "classification_hint": "PROVEN_SAFE", }, "3gpp_rach_contention": { "build": cellular.rach, "property": "no_undetected_collision", "body": "3GPP", "spec": "3GPP TS 38.321 §5.1 (Random access, contention resolution)", "citation": None, "known_finding": None, "classification_hint": "PROVEN_SAFE", }, "3gpp_beam_failure_recovery": { "build": cellular.beam_failure_recovery, "property": "recover_before_rlf", "body": "3GPP", "spec": "3GPP TS 38.321 §5.17 / TS 38.213 §6 (Beam failure recovery)", "citation": None, "known_finding": None, "classification_hint": "PROVEN_SAFE", }, "3gpp_xn_handover_premature_release": { "build": cellular.xn_handover, "build_fixed": cellular.xn_handover_fixed, "property": "always_one_serving_context", "body": "3GPP", "spec": "3GPP TS 38.300 §9.2.3 / TS 38.423 (Xn handover, data forwarding & path switch)", "citation": None, "known_finding": None, "note": "Modeled NAIVE variant releases the source context before path-switch acknowledgement, " "opening a no-context window with data loss. Whether a compliant Xn handover can reach " "this depends on exact timer/forwarding configuration -> flagged for expert review; NOT " "asserted as a spec defect.", "classification_hint": "CANDIDATE_COUNTEREXAMPLE", }, # ---------------- cross-domain: the method reproduces DOCUMENTED findings beyond wireless ---------------- "pqc_hybrid_downgrade": { "build": lambda: pqc_wifi.build(False), "build_fixed": lambda: pqc_wifi.build(True), "property": "no_insecure_handshake", "body": "IEEE/PQC", "spec": "IEEE 802.11bt (PQC amendment, PAR) — hybrid post-quantum key exchange", "citation": "Stebila, Fluhrer & Gueron, \"Hybrid Key Exchange in TLS 1.3\" " "(IETF draft-ietf-tls-hybrid-design): downgrade-resilience requires binding the " "negotiated groups into the handshake transcript.", "known_finding": "Accepting a peer's classical/weaker fallback without binding the negotiated " "suite into the transcript admits a SILENT HYBRID-DOWNGRADE; transcript " "binding removes it.", "classification_hint": "KNOWN_COUNTEREXAMPLE", }, "interconnect_cyclic_deadlock": { "build": lambda: cxl_fwd.build(False), "build_fixed": lambda: cxl_fwd.build(True), "property": "ordered_acquisition", "body": "CXL/PCIe", "spec": "Cache-coherent interconnect (CXL.cache/.mem) shared-resource acquisition", "citation": "Coffman, Elphick & Shoshani, \"System Deadlocks\", ACM Computing Surveys 3(2), " "1971: circular wait is a necessary deadlock condition; a global resource ordering " "removes it.", "known_finding": "Ungated out-of-order acquisition of two shared resources by two agents forms " "a circular hold-and-wait -> DEADLOCK; a global acquisition order eliminates it.", "classification_hint": "KNOWN_COUNTEREXAMPLE", }, } def build(name, fixed=False): meta = PUBLISHED[name] if fixed and "build_fixed" in meta: return meta["build_fixed"]() return meta["build"]()