Composable Model Identity — Formal Hardening of Structural Attestations in the Enterprise Identity Stack
Abstract
Enterprise identity systems can authenticate workloads, credentials, and attested platforms, but they do not close the composition layer where runtime model identity enters authorization. A token can verify that a service is running in a trusted environment, that its credentials are valid, and that its actions are authorized — without ever establishing which neural network is actually computing. When model identity evidence is inserted into standard authorization flows, new security properties emerge that are not inherited from the underlying protocols and must be formally established rather than presumed. This paper presents a live integration architecture for model-identity attestations in JWT and SPIFFE-style token flows, grounded in real measurements from six neural networks executed inside an NVIDIA H100 Confidential Computing enclave. It formally verifies four composition properties — non-separability, temporal binding, issuer authenticity, and reference integrity — across three Coq proof files with zero unfinished proof obligations. Every remaining trust dependency is explicitly named, traced to an integration control, and paired with a concrete falsification witness. The result is a formally hardened composition layer where no security property is left implicit and no assumption is left silent. Supplementary Material This paper is accompanied by three Coq proof files — ComposableIdentity.v, IssuerAuthenticity.v, and ReferenceIntegrity.v — that formally verify the four composition properties described in §§4–6: non-separability, temporal binding necessity, issuer authenticity, and reference integrity. Together the files prove thirteen theorems from eleven named axioms, each paired with a concrete falsification witness and an integration control. No file contains unresolved obligations (Admitted), and all three compile cleanly under the Rocq Prover 9.1.1 (the current release of the Coq proof assistant, compiled with OCaml 5.4.0). They are available for download as supplementary files attached to this record. The Neural Network Identity Series — Mathematical foundations, empirical validation, and governance frameworks for verifying which model is running Newest addition: Technical Note: The Disappearing Window — AI Logprob Access Withdrawal and the Structural Verifiability of Frontier Model Contracts (DOI: 10.5281/zenodo.20362098) Paper 1: The δ-Gene: Inference-Time Physical Unclonable Functions from Architecture-Invariant Output Geometry (DOI: 10.5281/zenodo.18704275) Paper 2: Template-Based Endpoint Verification via Logprob Order-Statistic Geometry (DOI: 10.5281/zenodo.18776711) Paper 3: The Geometry of Model Theft: Distillation Forensics, Adversarial Erasure, and the Illusion of Spoofing (DOI: 10.5281/zenodo.18818608) Paper 4: Provenance Generalization and Verification Scaling for Neural Network Forensics (DOI: 10.5281/zenodo.18872071) Paper 5: Beneath the Character: The Structural Identity of Neural Networks — Mathematical Evidence for a Non-Narrative Layer of AI Identity (DOI: 10.5281/zenodo.18907292) Paper 6: Which Model Is Running?: Structural Identity as a Prerequisite for Trustworthy Zero-Knowledge Machine Learning (DOI: 10.5281/zenodo.19008116) Paper 7: The Deformation Laws of Neural Identity (DOI: 10.5281/zenodo.19055966) Paper 8: What Counts as Proof? — Admissible Evidence for Neural Network Identity Claims (DOI: 10.5281/zenodo.19058540) Paper 9: Composable Model Identity — Formal Hardening of Structural Attestations in the Enterprise Identity Stack (DOI: 10.5281/zenodo.19099911) Paper 10:Where Identity Comes From: Path Sensitivity and Endpoint Underdetermination in Neural Network Training (DOI: 10.5281/zenodo.19118807) Paper 11: Post-Hoc Disclosure Is Not Runtime Proof: Model Identity at Frontier Scale (DOI: 10.5281/zenodo.19216634) Paper 12: Family-Dependent Response to Reasoning Distillation Across Structural and Functional Identity Layers (DOI: 10.5281/zenodo.19298857) Paper 13: Safety-Alignment Removal as a Model-Identity Failure — Structural Evidence from Published Weight-Level Mutation Checkpoints (DOI: 10.5281/zenodo.19383019) Technical Note: Agent Identity Is Not Model Identity (DOI: 10.5281/zenodo.19240883) Technical Note: Gap Invariance: Why PPP Measurements Are Domain-Independent by Construction (DOI: 10.5281/zenodo.19275524) Technical Note: Measured Model Substitution Under Valid Agent Credentials (DOI: 10.5281/zenodo.19342848) Technical Note: Artifact Identity Is Not Runtime Identity — Trustfall Lite and the Boundary of File-Level Model Verification (DOI: 10.5281/zenodo.20019127) Formal Verification Stack for Neural Network Structural Identity (IT-PUF Coq Proofs) (DOI: 10.5281/zenodo.18930621) Copyright (c) 2026 Anthony Ray Coslett / Fall Risk AI, LLC. All Rights Reserved. Confidential and Proprietary. Patent Pending (Applications 63/982,893, 63/990,487, 63/996,680, 64/003,244).
Community
0 commentsNo discussion yet
Be the first to share a question or observation.