arXiv CSopen access

From Public-Key Linting to Operational Post-Quantum X.509 Assurance for ML-KEM and ML-DSA: Registry-Driven Policy, Mutation-Based Evaluation, and Import Validation

2026 · arxiv_cs

arXiv CS · Papers · License: Open Access · 2026

cryptography cybersecurity privacy security

cryptography, security, privacy, cybersecurity

From Public-Key Linting to Operational Post-Quantum X.509 Assurance for ML-KEM and ML-DSA: Registry-Driven Policy, Mutation-Based Evaluation, and Import Validation José Luis Delgado

arXiv:2604.17003v1 [cs.CR] 18 Apr 2026

Universitat Oberta de Catalunya [email protected]

Abstract Final FIPS and PKIX standards for ML-KEM and ML-DSA settle the normative floor, yet they do not by themselves provide assurance. In practical post-quantum X.509 deployments, failures still emerge at certificate-profile semantics, SubjectPublicKeyInfo representation, and private-key container import, while current PQ public-key linting does not yet provide a reproducible workflow that says which checks belong to the certification authority, which belong to the artifact importer, and how those checks should act under deployment-facing policy. We present an operational post-quantum X.509 assurance framework for ML-KEM and ML-DSA in a narrow executable profile, pkix-core. The framework reifies 17 final-standards requirements into an assurance registry indexed by owner, stage, detector kind, normative strength, and mode-specific action; packages those requirements into three operator gate packs; spans certificate/profile, SPKI/public-key, and private-key-container/import surfaces; and evaluates them through a frozen mutation-based corpus backed by bounded public-appendix and cross-tool supporting evidence. Across a controlled corpus of 48 artifacts, comprising 21 valid and 27 invalid cases, the artifact detects all expected invalid artifacts in both strict and deployable modes with zero false positives. Strict blocks all 17 active requirements; deployable preserves the same underlying detection coverage while downgrading exactly one exercised ML-KEM canonicality condition from block to warning. On the importer-owned private-key surface, all 7 active requirements are covered, with 7/7 expected invalid detections and no open detector gaps. On a comparable certificate subset, a frozen JZLint baseline meets 5/10 expected invalid detections and fatally rejects 3 valid ML-KEM certificates, whereas the local artifact meets 10/10 with no fatal valid rejections. A bounded public appendix of 26 artifacts across two providers and all six ML-KEM/ML-DSA private-key parameter sets, together with a cross-tool matrix over 57 artifacts, further shows that parse acceptance and policy conformance diverge materially while keeping the paper out of the territory of prevalence studies and benchmark shootouts. Overall, the results support an operational X.509 assurance workflow for CA pre-issuance and private-key import that extends prior PQ public-key linting work.

Keywords: post-quantum cryptography, X.509, PKIX, ML-KEM, ML-DSA, assurance engineering, certificate profiling, private-key import validation

Contents Part I. Foundations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

1 Introduction

2 Related Work

3 Problem Setting and Scope

4 Normative Basis and Translation Method

Part II. Realization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

5 Operational Assurance Model

6 Artifact Architecture and Implementation

7 Requirement Registry and Policy Model

Part III. Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

8 Corpus Design, Mutation Families, and Evaluation Protocol

9 Controlled Results

10 Baseline Insufficiency Analysis

11 Policy Closure Case Studies

Part IV. Significance . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

12 Operator Workflow and Deployment Guidance

13 Supporting External Evidence

14 Limitations and Threats to Validity

15 Conclusion

A Full Requirement Catalogue

B Controlled Corpus Inventory and Mutation Catalogue

C Detailed Baseline Comparison Tables

D Public Appendix Ledger

E Cross-Tool Full Matrix

F Reproduction and Release Manifest

Part I Foundations

Introduction

Why final standards do not eliminate operational assurance risk The standardization line for lattice-based post-quantum cryptography has crossed a decisive threshold. At the algorithmic layer, ML-KEM and ML-DSA are fixed by FIPS 203 and FIPS 204 [6, 5]. At the X.509/PKIX layer, the conventions for signatures, subject public keys, and private-key encodings are specified by RFC 9881 for ML-DSA and RFC 9935 for ML-KEM [3, 7]. That closure removes much of the ambiguity that surrounded draft-era engineering and gives implementation work a final normative floor. The remaining task is operational assurance. Standards specify the shape of conforming algorithms and artifacts, yet they do not assign enforcement to a stage, identify the owner of that enforcement decision, or define how a violation should propagate through a deployment-facing workflow. A certification authority, an issuance pipeline, and a private-key importer occupy different operational positions. They inspect different artifact surfaces, carry different responsibilities, and require different failure semantics. The remaining task is to turn final requirements into accountable gates before issuance and before import. The PQ setting sharpens this problem because the failure modes span more than one syntactic layer. An artifact may identify the correct algorithm family and still fail at certificate-profile semantics, SubjectPublicKeyInfo representation, or private-key import consistency. Conversely, an implementation may parse an artifact successfully while still accepting a semantically invalid or misprofiled object. Standardization fixes the normative floor, assurance still has to turn that floor into executable operational decisions. Failure surfaces across certificate, SPKI, and import boundaries In the scope of this paper, operational assurance lives across three distinct surfaces. The first is the certificate/profile surface, where failures arise from PKIX semantics rather than from raw encoding alone. Examples include keyUsage requirements, constraints on the signature AlgorithmIdentifier, and PKIX-specific prohibitions such as the exclusion of HashML-DSA from the covered certificate profile [3, 7]. They are issuance-time policy conditions whose failure should be attributed to the CA-side workflow. The second surface is SPKI/public-key. Here the relevant defects include algorithm-identifier family mismatches, parameters that must be absent, exact public-key lengths tied to the parameter set, and canonicality conditions on represented public-key material. A public key may therefore be attached to the right certificate skeleton and still be structurally or semantically wrong at the representation boundary. Such defects belong to the pre-issuance path as well, but they are not identical to certificateprofile defects and should not be collapsed into the same undifferentiated bucket.

The third surface is private-key-container/import. This surface is easy to neglect if one thinks only in terms of certificate linting, yet it is indispensable for assurance. Private-key containers can be malformed, use the wrong CHOICE form, encode the wrong seed or expanded-key length, or violate seed-to-expanded consistency conditions. Some of these checks depend on import-side validation logic rather than certificate parsing. For that reason, they should be modeled as importer-owned assurance requirements within the import path itself. These three surfaces are operationally adjacent but not reducible to one another. A certificate can be well-formed while the associated public-key payload is not canonical. A public key can parse while the private key supplied for import is internally inconsistent. A tool can accept an object at parse time while failing to enforce a deployment-relevant PKIX constraint. These observations show that parse acceptance, structural well-formedness, profile conformance, and import validity are related but non-identical judgments. From public-key linting to operational assurance Recent work by Karatsiolis et al. opened the line of public-key linting for ML-KEM and ML-DSA and showed that post-quantum X.509 requires dedicated checks rather than a naive transplantation of classical certificate logic [2]. That contribution is the closest prior step. This paper extends that line into operational assurance. With final standards in place, the main challenge is to organize their clauses into a reproducible assurance workflow that answers four operator questions at once: what is checked, where it is checked, who owns the check, and how the result should act under policy. Accordingly, this paper presents a workflow-centric assurance artifact for X.509/PKIX around ML-KEM and ML-DSA instead of an expanded lint catalogue. This framing also determines how comparison evidence is used. A certificate-level baseline remains supporting evidence, especially when it reveals incompleteness or runtime fragility, but it is not the main contribution. Ecosystem behavior observations are also supporting evidence, because they help separate parse acceptance from policy conformance. The central claim is architectural: the field needs accountable post-quantum X.509 assurance rather than isolated PQ public-key lints. Thesis and paper identity The central claim is the following. Once final PQ standards exist, the central assurance problem is the execution of accountable decisions across certificate, SPKI, and private-key import boundaries. This paper addresses that problem with a narrow but executable profile, pkix-core, for ML-KEM and ML-DSA. The profile reifies final-standards requirements into a registry whose records are assigned by owner and stage, grouped into operator gate packs, evaluated under two policy modes, and tested against a frozen mutation-based corpus. The artifact is designed both for operator use and for reproducible evaluation. Reference implementation, frozen corpus, and reproduction materials are available at github.com/hypergalois/PQC-X509-ASSURANCE.

Related Work

Public-key linting for ML-KEM and ML-DSA The nearest prior work is the public-key linting line opened by Karatsiolis et al. [2]. It shows that ML-KEM and ML-DSA demand dedicated PQ-aware lint logic and cannot be handled by an unmodified inheritance of classical X.509 checking. This paper builds on that work, but changes the unit of

contribution. The focus here is a workflow-centric assurance artifact with owner/stage assignment, gate packs, policy modes, import validation, and frozen replay outputs. Final standards as normative foundations FIPS 203 and FIPS 204 provide the algorithmic floor for ML-KEM and ML-DSA respectively [6, 5], while RFC 9881 and RFC 9935 provide the final PKIX/X.509 conventions that close the draft-era uncertainty for the certificate, SPKI, and private-key encodings in scope [3, 7]. JZLint as frozen baseline The frozen JZLint snapshot is used as a certificate-level implementation baseline [4]. Its proper function is to provide supporting comparative evidence about current certificate-level capability and runtime fragility under a fixed local replay environment. libcrux as narrow import substrate The libcrux snapshot [1] acts as the narrow cryptographic substrate used by the import-validation bridge, especially for the private-key container checks whose validity depends on seed, expanded-key, and consistency semantics. The paper therefore cites libcrux as implementation substrate. Prior work establishes the need for PQ-aware linting; final standards establish the normative floor; and the frozen baseline and import substrate provide bounded implementation anchors. This paper builds on that base to study operational post-quantum X.509 assurance. Contributions • We define an operational post-quantum X.509 assurance model for ML-KEM and ML-DSA in pkix-core, organized by owner, stage, and gate pack rather than by lints alone. • We realize that model as a registry-driven policy artifact with 17 active requirements distributed across three artifact surfaces and three operator-facing gate packs, together with explicit strict and deployable semantics. • We provide a controlled mutation-based evaluation over a frozen corpus of 48 artifacts, comprising 21 valid and 27 invalid cases, and show full expected invalid detection with zero false positives in the declared scope. • We extend assurance beyond certificate material by including private-key-container/import validation as a first-class surface, covering all 7 importer-owned requirements in the current profile. • We present disciplined supporting evidence through a certificate-level frozen baseline comparison and a bounded public appendix, while keeping both subordinate to the workflow-centric claim of the paper.

Problem Setting and Scope

The precise assurance question Given final FIPS and PKIX standards for ML-KEM and ML-DSA, how can their executable requirements be translated into a reproducible, owner-assigned, mode-aware assurance workflow across certificate issuance and private-key import, without claiming runtime coverage that the artifact does not execute? First, the paper is about executable requirements grounded in standards text. Second, it is about workflow assignment, meaning that responsibility must be attached to concrete owners and stages. Third, it rejects the common temptation to let certificate-side evidence stand in for runtime behavior. 6

The pkix-core profile The pkix-core profile is the paper’s executable profile boundary. It captures the intersection of final algorithmic standards and final PKIX/X.509 conventions that the artifact can instantiate, mutate, and evaluate reproducibly for ML-KEM and ML-DSA. Artifact surfaces in scope The active profile spans three artifact surfaces. 1. Certificate/profile. This surface covers X.509 certificate semantics whose assurance meaning is determined by PKIX policy, including keyUsage obligations and signature AlgorithmIdentifier requirements. 2. SPKI/public-key. This surface covers SubjectPublicKeyInfo and the embedded public-key payload, including algorithm-identifier encoding, absent-parameters rules, length constraints, and canonicality conditions. 3. Private-key-container/import. This surface covers private-key encodings and import-side validity conditions, including CHOICE form, exact lengths, and seed-to-expanded consistency. Figure 1 summarizes how these surfaces are mapped to owners, gate packs, and operator actions in the current profile.

Figure 1: pkix-core assurance scope by surface, owner, and operational role. The profile contains 17 active requirements: 10 owned by CA pre-issuance and 7 owned by the artifact importer.

Surface / gate pack

Owner

Artifact unit

Certificate/profile ca-certificate-profile

ca-preissuance

X.509 certificate profile

ML-KEM CA issuance keyUsage must be gate keyEnciphermentonly when present; ML-DSA certificates must carry at least one signing-related bit; signature AlgorithmIdentifier parameters must be absent; HashML-DSA is forbidden in the covered PKIX profile

SPKI/public-key ca-spki-public-key

ca-preissuance

SubjectPublicKeyInfo and public-key payload

OID family and absent-parameters rules; exact public-key lengths for parameter sets; ML-KEM encode/decode identity as a canonicality condition

CA issuance gate

artifact-importer PKCS#8-style private-key container and import substrate

Import acceptance gate

runtime-consumer Consumer-time behavior

Seed and expanded-key lengths; CHOICE form; seed/expanded consistency; ML-KEM expanded-key hash check Explicitly modeled as a future boundary rather than silently implied by certificate-side evidence

Private-keycontainer/import import-private-key

Runtime-consumer boundary

Active reqs.

Representative obligations

Default role in workflow

Out of executable scope

Owners and stages The owner-stage split is the organizing abstraction of pkix-core. In pkix-core, ca-preissuance owns two stages: certificate/profile and SPKI/public-key. The artifact-importer owns the private-key-container/import stage. The runtime-consumer is kept explicit as a boundary role but remains out of executable scope until it can be supported by active requirements and evidence. This

structure answers a practical question that many standards-conformant tools still leave blurred: who is responsible for running which gate before an artifact crosses into the next stage of the workflow? Final normative floor: FIPS 203, FIPS 204, RFC 9881, RFC 9935

CA pre-issuance

Artifact importer

Runtime consumer

import-private-key 7 requirements

Explicit boundary 0 active requirements

ca-certificate-profile 5 requirements ca-spki-public-key 5 requirements

7 importer-owned requirements

10 CA-owned requirements across two issuance stages

Figure 2: Operational assurance boundaries in pkix-core. Final standards provide the normative floor, but the actionable workflow emerges only after requirements are assigned by owner and stage. The notion of gate pack makes this split usable. A gate pack is the smallest operator-facing assurance bundle that answers what should be run at a specific stage by a specific owner. In the current profile there are exactly three packs: one for certificate/profile checks, one for SPKI/public-key checks, and one for private-key/import checks. This packaging is what lets the artifact produce playbooks, pack-level summaries, and mode-aware outputs that can be consumed without reading the implementation first. Non-goals and explicit exclusions • Benchmark breadth. The paper does not claim to be a comprehensive benchmark across all ecosystem tools or all possible PQ X.509 implementations. • Prevalence claims. The bounded public appendix is external-validity support rather than a census of Internet-deployed PQ artifacts. • Runtime-consumer execution. Runtime-consumer behavior remains explicit but out of executable scope in pkix-core. • Algorithm-family breadth. The artifact is limited to ML-KEM and ML-DSA, it does not attempt to cover every PQ family or hybrid issuance profile. • Baseline-centered framing. The certificate-level baseline and cross-tool observations are supporting evidence rather than the center of the contribution. Threat model and operational assumptions The operational threat model is the threat model of malformed, misprofiled, or semantically inconsistent artifacts crossing the wrong boundary unchecked. The artifact is designed to intercept such failures before certificate issuance and before private-key import. It therefore assumes a deployment pipeline in which the relevant objects can be inspected at those stages and in which the owners of those stages can act on block-or-warn outputs. The work does not model every conceivable security failure. It does not address side channels, keygeneration entropy failures, runtime protocol misuse, or consumer behavior after artifact acceptance. It 9

also does not claim that every external toolchain will behave identically. Instead, the paper assumes a final normative floor, a frozen set of third-party snapshots, a controlled corpus with labeled mutations, and a bounded public appendix for external support.

Normative Basis and Translation Method

Final normative floor At the algorithmic layer it consists of FIPS 203 for ML-KEM and FIPS 204 for ML-DSA [6, 5]. At the PKIX/X.509 layer it consists of RFC 9881 for ML-DSA and RFC 9935 for ML-KEM [3, 7]. These documents are treated as the authoritative source of algorithm identifiers, absent-parameter rules, public-key sizes, certificate keyUsage semantics, and private-key encoding conventions in the covered profile. Draft-era PQ engineering accumulated a considerable amount of provisional logic, partial implementations, and quietly outdated assumptions. A workflow-centric assurance artifact cannot rest on such sediment if it wants to produce operator-facing policy. It needs fixed clauses, stable identifiers, and a basis on which disagreements can be localized to a requirement rather than to a shifting standards landscape. Requirement extraction procedure The procedure consists of five steps. 1. Locate an executable clause. We identify a final-standards clause that imposes a concrete condition on an artifact representation, profile semantic, or import boundary. 2. Normalize it into a requirement sentence. The clause is rewritten into a single explicit requirement whose truth value can be checked against an artifact. 3. Assign operational placement. The requirement is mapped to an artifact type, stage, owner, and gate pack. 4. Bind it to evaluation design. The record is linked to mutation families, an expected detector path, and a baseline-status annotation describing whether a frozen external baseline appears to cover, partially cover, or miss the requirement. 5. Bind it to policy. The record receives a normative-strength label, a constructibility status, mode-specific actions, and a short operational justification. The result is a registry record that is simultaneously normative, operational, and evaluable. It preserves traceability to the standards text through explicit source locators, but it also records enough structure to generate policy matrices, owner-stage summaries, coverage reports, and operator gate packs. Requirement schema and fields The registry schema is designed to prevent a requirement from floating free of provenance, workflow, or evidence. Table 1 groups the fields by their manuscript function.

Table 1: Registry field groups and their role in the assurance workflow. The schema keeps each requirement traceable to final standards, placeable in the workflow, and testable against frozen evidence.

Field group

Representative fields

Purpose in the artifact

Normative provenance

source, source_locators, requirement, normative_strength algorithm, artifact_type, stage, profile, fault_family

Anchors each record in the final standards corpus and preserves the exact clause that justifies the check. States where the requirement lives: which algorithm family it concerns, which artifact surface it targets, and which defect family it represents. Assigns responsibility, groups the requirement into an operator-facing bundle, and determines whether a finding blocks or warns under each mode. Connects the normative claim to the controlled corpus, to detector expectations, to comparative evidence, and to whether the requirement is currently executable in the profile. Gives each requirement a stable manuscript-facing handle and a report-facing severity label.

Artifact placement

Operational ownership

owner, gate_pack, mode_action, justification

Evaluation linkage

mutation_family, expected_detector, baseline_status, constructibility

Identity and reporting

id, severity

This schema prevents a common failure of security-engineering papers, the detector exists, but no one can tell why it exists, where it should run, or how it is tied to evidence. In the present artifact, a requirement that lacks one of these dimensions is incomplete by design. Constructibility and activation criteria A requirement becomes active only when it satisfies the constructibility discipline of the profile. In the current release line, active requirements must belong to pkix-core, be marked covered, map consistently to the owner-stage expectations of their declared gate pack, carry valid actions for both strict and deployable, and include a non-empty operational justification. The schema can represent future states such as planned or externally dependent coverage, but the current profile activates only the 17 requirements whose execution path is present and evidenced. The registry limits claims to requirements that are both implemented and evidenced. From normative text to executable requirement Figure 3 illustrates the translation pipeline from standards clause to operator-facing gate. Consider the ML-KEM certificate rule that, when keyUsage is present, keyEncipherment must be the only active bit [7]. In the registry, this becomes MLKEM-CERT-KU-KEYENCIPHERMENT-ONLY. The record is assigned to artifact_type=certificate, stage=certificate/profile, owner=ca-preissuance, gate_pack=ca-certificate-profile, and detector_kind=policy. It is then linked to mutation families such as missing keyEncipherment, extra prohibited bits, and empty keyUsage; finally, it receives block as its action in both modes. What matters here is the complete operational context around the detector. It has a normative anchor, a workflow owner, a corpus realization, and an output policy. The same discipline applies to structural constraints such as absent parameters and exact public-key lengths, and it also applies to import-side conditions such as seed/expanded consistency checks.

Final standards clause RFC/FIPS rule

Normalized requirement single checkable sentence

Registry record owner, stage, gate pack, mode

Evaluation link mutation family + detector

Operatorfacing outcome block / warn / pass

Example clause: ML-KEM cert. keyUsage must be keyEnciphermentonly

MLKEM-CERT-KUKEYENCIPHERMENT -ONLY

ca-preissuance certificate/ profile ca-certificateprofile

Mutations: missing bit, extra bit, empty KU

strict: block deployable: block

Figure 3: From normative text to executable gate. The registry is the mechanism that turns standards prose into an operator-owned, corpus-exercised assurance requirement.

Registry-driven policy A registry-driven policy model resolves three issues that ordinary detector lists leave open. First, it solves traceability: every active check can be traced back to final standards text and forward to evidence. Second, it solves accountability: every check belongs to an owner, a stage, and a gate pack rather than floating in a generic lint namespace. Third, it solves operational differentiation: the same underlying detector evidence can be mapped to distinct actions under strict and deployable without duplicating the normative record. It also constrains the manuscript to claims backed by registry records, policy outputs, corpus mutations, and frozen summaries. In that sense, the registry is the point at which standards, workflow, policy, and evaluation are bound together.

Part II Realization

Operational Assurance Model

Owner-stage workflow Part I fixed the normative floor, the executable scope, and the requirement schema. The next step is to turn those records into a workflow that an operator can run. The present artifact does so by placing every active requirement at the intersection of an owner and a stage. In the current pkix-core release line, two owners carry executable responsibility: CA pre-issuance and artifact importer. The CA owns the two issuance-side stages, certificate/profile and SPKI/public-key, which together account for 10 active requirements. The importer owns the private-key-container/import stage, which accounts for the remaining 7. The runtime-consumer role is retained explicitly in the workflow model, but with zero active requirements, exactly as anticipated by the scope boundary in Figures 1 and 2. This split is the answer to the operator question that standards text alone does not settle: who must run which gate before the artifact is allowed to cross into the next stage of the pipeline? CA-side defects and importer-side defects are both “assurance” defects, but they arise under different authority, different failure semantics, and different remediation paths. A certificate-profile violation must be corrected before issuance. A malformed private-key container must be rejected before import. The owner-stage assignment is frozen into the workflow package emitted by the artifact. The machinereadable workflow view records the active owners, their stages, their commands, and their modespecific requirement actions. The human-readable workflow view translates the same information into an operator recipe. Because both views are generated from the registry, there is no separate hand-maintained “deployment guidance” document that can drift away from the actual artifact.

Mode layer: strict = 17 block | deployable = 16 block + 1 warn ca-certificate-profile 5 requirements Requirement registry 17 active records

Owner/stage split 10 CA, 7 importer

ca-spki-public-key 5 requirements CA pre-issuance packs

Runtime consumer explicit boundary 0 active requirements

import-private-key 7 requirements

reference_workflow.json reference_workflow.md stage_owner_summary. json operator_gate_matrix. {json,csv} operator_readiness_ summary.json notes/operatorplaybook.md

artifact-importer pack

Figure 4: From registry records to operator workflow. Requirements are assigned to owners and stages, grouped into gate packs, and emitted as machine-readable and human-readable workflow outputs.

Gate packs and accountability Gate packs operationalize the owner-stage model. Each pack is the smallest operator-facing assurance bundle that can be invoked, reviewed, and assigned without reading the source tree. The current profile defines three packs, each mapped one-to-one to an owner-stage row: ca-certificate-profile, ca-spki-public-key, and import-private-key. The policy layer enforces this mapping, so a requirement cannot be assigned to the wrong owner or stage. Because each pack carries explicit responsibility, failures map directly to the relevant workflow: cacertificate-profile to issuance and import-private-key to the importer. Table 2 captures the current view: three packs, three active owner-stage rows, 17 requirements, and one mode-dependent non-blocking path. Table 2: Operator-facing gate packs in the current pkix-core release line. The the one-to-one mapping between pack, owner, and stage. The artifact can tell a CA and an importer what to run and which outputs to inspect.

Gate pack

Owner

Stage

Req.

strict

deployable

ca-certificate-profile

CA pre-issuance

certificate/profile

5 block

ca-spki-public-key

CA pre-issuance

SPKI/public-key

5 block

4 block, 1 warn

import-private-key

Artifact importer

private-keycontainer/import

7 block

Total

—

17 block

16 block, 1 warn

Principal operator outputs extended_registry_summary*, policy_summary*, certificate_spki_coverage*, operator_readiness_summary.json extended_registry_summary*, policy_summary*, certificate_spki_coverage*, operator_gate_matrix.json extended_registry_summary*, policy_summary*, private_key_coverage*, operator_gate_matrix.json reference_workflow.{json,md} and notes/operator-playbook.md provide the workflow-wide view.

Mode semantics: strict and deployable The policy model separates detection from operator action. This is a central architectural choice in the artifact. Detectors produce findings against artifact content; policy then interprets those findings under a selected mode. In the current profile, both modes operate over the same 17 active requirements and the same implemented detector set. strict is the assurance-maximizing interpretation: every active requirement blocks. By contrast, deployable is the operator-facing issuance posture: it preserves the same detector evidence, but allows the policy layer to downgrade selected conditions from block to warning when that yields a lower-noise deployment-facing surface without discarding the underlying signal. The present release line exercises that split exactly once. The single warning path is MLKEM-SPKI-ENCODE-DECODE-IDENTITY, a canonicality condition on ML-KEM public-key material that is implemented locally and exercised by an unreduced ByteEncode12 mutation in the controlled corpus. In strict the condition blocks; in deployable it warns. Every other active requirement remains blocking in both modes. The artifact is using modes to distinguish assurance-maximizing posture from deployment-facing posture while keeping the raw evidence intact. same detector evidence different operator action

strict 17 blocking requirements

deployable 16 blocking requirements

certificate/profile: 5 block SPKI/public-key: 5 block private-key/import: 7 block

certificate/profile: 5 block SPKI/public-key: 4 block, 1 warn private-key/import: 7 block

No warning path

Warning path: MLKEM-SPKI-ENCODEDECODE-IDENTITY

Figure 5: Mode-aware policy in the current artifact.x.

Runtime-consumer as explicit boundary The runtime-consumer role is modeled and then held outside the executable profile. Many papers quietly slide from issuance-side or importer-side evidence into statements about runtime consumer assurance, as though parse acceptance or import acceptance were already a proxy for end-to-end runtime behavior. This artifact keeps runtime visible as a role in the workflow package, records that it has zero active executable requirements, and declines to manufacture pseudo-coverage from certificate-only or importer-only results. Outputs produced for operators The artifact emits outputs in two strata. The first stratum is policy- and workflow-facing. This includes policy_summary_strict.json, policy_summary_deployable.json, stage_owner_summary.json, reference_workflow.json, reference_workflow.md, operator_gate_matrix.json, operator_gate_matrix.csv, and operator_readiness_summary.json. These files answer questions such as which requirements belong to which owner, what each mode does, which pack a requirement inhabits, and what the default operator posture should be. The second stratum is execution-facing. Here the primary outputs are the mode-specific evaluation summaries and coverage reports, including extended_registry_summary_*.json, 15

certificate_spki_coverage_*.json, and private_key_coverage_*.json. These outputs are what an operator or reviewer inspects after actually running the relevant gate-pack commands. The humanreadable playbook in notes/operator-playbook.md sits across both strata: it names the commands to execute and the files to inspect. This design allows the artifact to serve both as a paper companion and as an operational recipe. A reviewer can read the workflow files without running the code. An operator can run the commands and inspect the matching summaries. An author can write the paper against outputs that are already frozen and hashable. These are three different users of the same package, not three divergent documentation paths. Operational interpretation The artifact is an assurance workflow package that can be delegated, audited, and replayed. In that form, it extends public-key linting into an assurance workflow [2]. What matters now is whether a defect is assigned to the correct owner, rendered under a defensible action policy, and presented in a form that an operator can use before issuance or before import. The workflow also clarifies why deployable defaults to the CA-facing path while strict remains the reference assurance posture. Issuance pipelines benefit from a low-noise default gate that still preserves policy evidence. Audit and pre-release review benefit from the maximal blocking interpretation. The importer path, by contrast, blocks all currently modeled private-key defects in both modes because the current profile offers no operational reason to soften those checks.

Artifact Architecture and Implementation

Repository design The repository is organized according to an evidence-first discipline. Normative sources are frozen and documented under reference/; the machine-readable assurance registry lives in requirements.json; local implementation code lives in src/; valid and mutated artifacts plus their ledgers live in corpus/; reproducible runner entrypoints live in experiments/; raw machine-readable outputs accumulate under results/; and playbooks, and manuscript-lock materials live under notes/ The layout addresses three recurrent risks in reproducible assurance work: undocumented provenance, undocumented evaluation, and manuscript drift. The repository design counters all three. Provenance is captured through reference manifests, corpus hashes, and package manifests. Evaluation is captured through replayable scripts and machine-readable summaries. Manuscript drift is countered by locating claim maps, visual plans, related-work positioning, and release-bundle plans in the same tree as the executable artifact.

third_party/ frozen upstream snapshots

reference/ frozen norms

requirements. json registry

tools/ libcrux_import_check narrow import substrate

src/ assurance engine

corpus/ valid + mutated

experiments/ replay + runners

executable artifact core

results/ machinereadable evidence

notes/ playbooks + locks

artifact_release_ package.json

evidence, locks, and release packaging

Figure 6: Artifact realization and evidence flow. Project claims are first fixed in the registry, corpus, replay scripts, and packaging discipline; the paper sits downstream of that evidence flow.

Assurance engine The principal runner loads the registry, loads the corpus manifest, resolves artifact paths, and dispatches on artifact type. Certificates are evaluated through a certificate-specific DER and X.509 extractor; raw SubjectPublicKeyInfo artifacts are evaluated through an SPKI extractor; and private-key containers are evaluated through a dedicated PKCS#8 / OneAsymmetricKey parser. Each detector produces requirement-tagged findings. The policy layer then computes the applicable requirement set, interprets findings under the selected mode, and emits a final disposition of pass, warn, or block together with first-hit, redundancy, and missing-expected-detection summaries. Detector code answers whether a given artifact violates a given condition. Policy code answers what the artifact’s operational fate should be under the active profile and mode. The same underlying findings can therefore be rendered differently in strict and deployable without creating two separate detector universes. The engine also emits CSV and JSON views of the registry itself, making it possible to audit the evaluation outputs alongside the policy topology that produced them. A further practical detail is that the engine never assumes that manifest paths are anchored at one hard-coded root. It resolves the manifest root from the actual file layout before running the corpus, which keeps replay stable across packaged and unpackaged environments. Detector classes The implemented detector inventory currently spans three classes. Structural detectors capture exact container and representation constraints: absent AlgorithmIdentifier parameters, OID-to-length consistency, public-key payload size, signatureAlgorithm parameter absence, canonical encode/decode identity, and private-key seed or expanded-key length. Policy detectors capture profile semantics that are not exhausted by representation alone: ML-KEM keyUsage, ML-DSA positive signing semantics, prohibited encipherment/agreement bits, and the PKIX-specific HashML-DSA exclusion. Finally, importcrypto detectors perform checks whose meaning depends on the semantics of the imported key material itself, such as seed-to-expanded consistency and the ML-KEM expanded-key hash condition. All 17 active requirements in the current registry map to implemented detector metadata. Quantitatively, the current artifact contains 10 structural requirements, 4 policy requirements, and 3 import-crypto requirements.

Import-validation bridge The importer-owned slice is where a certificate-centric design would be most likely to fail. To avoid that failure, the artifact uses a deliberately narrow import-validation bridge backed by a frozen libcrux snapshot [1]. The bridge is a small, measured import-validation substrate that exposes the one operation the current profile needs for executable consistency checks: whether a given seed and a given expanded private key correspond for a stated parameter set. Concretely, the local wrapper invokes a dedicated binary under tools/libcrux_import_check, passing the parameter set and the two private-key components as hexadecimal arguments. A zero exit code indicates consistency, an exit code of one indicates a mismatch, and any other exit code is treated as a bridge failure. The private-key parser calls this bridge only after the relevant container forms and lengths have already been validated, which keeps the import-crypto checks narrow, interpretable, and subordinate to the local parsing logic. Within this paper, libcrux serves as a precise import-validation substrate rather than as a general runtime oracle. This design keeps the importer slice explicit about which cryptographic import semantics are delegated to a frozen external substrate, while still covering checks that go beyond container lengths and address seed/expanded coherence. Corpus generation and mutation pipeline The corpus pipeline is built to preserve provenance at the level of individual artifacts. Valid artifacts are generated locally through explicit corpus scripts and then recorded in corpus/manifest.jsonl with stage, algorithm, parameter set, source note, and SHA-256 hash. Invalid artifacts are produced in three ways: scripted OpenSSL-side generation for certificate-profile cases, deterministic DER mutation for fine-grained container and SPKI faults, and private-key-container reconstruction for importer-side failures. Every invalid artifact carries its own expected_detection set and its mutation-family labels, which lets the evaluation layer distinguish missed expectations from redundant or unexpected findings. The corpus therefore functions as a ledger rather than as a loose directory of “good” and “bad” files. The current controlled corpus contains 48 artifacts in total, with 21 valid and 27 invalid cases, balanced across ML-KEM and ML-DSA, and spread across the three active stages. The invalid side spans encoding, size/shape, inter-field consistency, policy, field-domain, and import-validation fault families. Because the mutation layer is deterministic, the same mutation family can be regenerated and replayed without ambiguity once the frozen valid input artifacts are fixed. The valid OpenSSL-generated corpus is frozen by hash on first generation and then reused on later replays. Freeze/replay pipeline The canonical executable entrypoint is ./experiments/replay_freeze.sh. Its job is to rerun detectors and regenerate the entire paper-facing evidence surface. In its current form the replay pipeline checks the execution environment; prepares frozen third-party material; builds the import-validation bridge; reuses or regenerates the controlled corpus and DER mutations; reruns the extended suite in both modes; reruns stage-specific coverage for the certificate/SPKI and private-key slices; regenerates policy summaries, owner-stage summaries, workflow files, and operator gate packs; reruns the certificate-level baseline comparison; refreshes the bounded public appendix and the cross-tool layer; rewrites claim locks, visual locks, and positioning locks; refreshes the artifact release package; records an explicit upgrade decision; and finally executes the local smoke tests.

Requirement Registry and Policy Model

Global inventory of 17 active requirements

The active registry currently contains 17 requirements, all marked covered in the constructibility field and all mapped to implemented detector metadata. The inventory is nearly balanced by algorithm family, with 8 ML-KEM requirements and 9 ML-DSA requirements, but more importantly it is balanced by workflow semantics: 10 requirements belong to CA pre-issuance and 7 belong to the artifact importer. The resulting distribution is 5 requirements in certificate/profile, 5 in SPKI/public-key, and 7 in privatekey-container/import. Table 3 presents the current inventory in full. Table 3: Active registry inventory in pkix-core. The current artifact is not built around one family of homogeneous checks, but around a mixed topology of structural, policy, and import-crypto requirements with explicit mode actions. Gate pack

Requirement ID

Operational intent

Detector kind

Norm.

strict

deployable

Enforce that an ML-KEM certificate uses keyEncipherment as the sole active keyUsage bit when the extension is present. Require absent parameters in ML-DSA certificate signature AlgorithmIdentifiers at both TBS and outer layers. Enforce the positive PKIX condition that an ML-DSA certificate expose at least one signingrelated keyUsage bit. Forbid encipherment and agreement semantics for ML-DSA certificates. Block HashML-DSA certificate signatures inside the covered PKIX profile.

policy

must

block

structural

must

block

policy

must

block

policy

must

block

policy

must

block

Require an ML-KEM SPKI AlgorithmIdentifier with absent parameters. Enforce parameter-set-specific ML-KEM public-key payload lengths. Require decode/re-encode identity for ML-KEM public-key canonicality. Require an ML-DSA SPKI AlgorithmIdentifier with absent parameters. Enforce parameter-set-specific ML-DSA public-key payload lengths.

structural

must

block

structural

must

block

structural

must

block

warn

structural

must

block

structural

must

block

Enforce 64-byte ML-KEM seedform private-key containers. Enforce parameter-set-specific ML-KEM expanded private-key lengths. Check that the seed and expanded ML-KEM representations in both form are mutually consistent.

structural

must

block

structural

must

block

importcrypto

should

block

CA certificate/profile ca-certificateprofile

MLKEM-CERT-KU-KEYENCI PHERMENT-ONLY

ca-certificateprofile

MLDSA-CERT-SIGNATURE-A ID-PARAMS-ABSENT

ca-certificateprofile

MLDSA-CERT-KU-AT-LEA ST-ONE-SIGNING-BIT

ca-certificateprofile

MLDSA-CERT-KU-NO-ENC IPHERMENT-OR-AGREEMENT

ca-certificateprofile

MLDSA-PKIX-HASHML-FOR BIDDEN

CA SPKI/public-key ca-spki-public-key

MLKEM-SPKI-AID-PARAM S-ABSENT

ca-spki-public-key

MLKEM-SPKI-PUBLIC-KEY -LENGTH

ca-spki-public-key

MLKEM-SPKI-ENCODE-DEC ODE-IDENTITY

ca-spki-public-key

MLDSA-SPKI-AID-PARAM S-ABSENT

ca-spki-public-key

MLDSA-SPKI-PUBLIC-KEY -LENGTH

Artifact importer private-key/import import-privatekey import-privatekey

MLKEM-PRIVATE-SEED-LEN GTH MLKEM-PRIVATE-EXPANDE D-LENGTH

import-privatekey

MLKEM-PRIVATE-BOTH-CON SISTENCY

Continued on next page

Gate pack

Requirement ID

Operational intent

Detector kind

Norm.

strict

deployable

import-privatekey

MLKEM-PRIVATE-EXPANDE D-HASH-CHECK

importcrypto

must

block

import-privatekey import-privatekey

MLDSA-PRIVATE-SEED-LEN GTH MLDSA-PRIVATE-EXPANDE D-LENGTH

structural

must

block

structural

must

block

import-privatekey

MLDSA-PRIVATE-BOTH-CON SISTENCY

Validate the ML-KEM expandedkey hash relation required by the final container layout. Enforce 32-byte ML-DSA seedform private-key containers. Enforce parameter-set-specific ML-DSA expanded private-key lengths. Check that the seed and expanded ML-DSA representations in both form are mutually consistent.

importcrypto

should

block

CA certificate/profile requirements The certificate/profile slice contains 5 requirements, all owned by the CA and all blocking in both modes. Their common character is that they express issuance semantics that go beyond DER well-formedness. The ML-KEM certificate requirement is a positive and negative keyUsage rule: if the extension is present, keyEncipherment must be the only active bit. The ML-DSA slice contains two keyUsage rules, one positive and one negative. The positive rule requires at least one signing-related bit; the negative rule forbids encipherment and agreement semantics. The remaining certificate/profile requirements close two final-standards AlgorithmIdentifier seams. One requires absent parameters for ML-DSA signature identifiers in certificates. The other blocks HashMLDSA certificate signatures inside the covered PKIX profile [3]. Together, these five requirements define a meaningful CA-side profile gate: they tell the issuance path whether the certificate is profilable in the way the final PKIX rules demand, beyond basic parse success. CA SPKI/public-key requirements The SPKI/public-key slice also contains 5 requirements, all CA-owned. Unlike the certificate/profile slice, however, the SPKI slice is entirely structural in the current profile. It requires absent parameters in SPKI AlgorithmIdentifiers for both algorithms, enforces parameter-set-specific payload lengths for both algorithms, and adds a canonicality check for ML-KEM public-key encodings [6, 7]. These checks are structurally motivated, but they are still issuance-side checks because the CA is the last party that can prevent a malformed or semantically suspicious public key from being embedded into a certificate and pushed downstream. This slice can be exercised both on raw SPKI artifacts and on certificates that carry SPKI defects inside a larger X.509 container. Artifact-importer private-key requirements The importer slice contains 7 requirements and marks the extension beyond certificate-only linting. Four requirements belong to ML-KEM and three to ML-DSA. Both algorithm families require checks for seed-form length, expanded-form length, and seed/expanded consistency in the both representation. ML-KEM adds a further expanded-key hash check, which follows from the final container and key-layout semantics in the standards corpus [6, 7]. All 7 requirements block in both modes. The two consistency checks are labeled should rather than must, but they still block in the current profile because the importer boundary is a high-consequence boundary and because executable evidence for those checks exists through the narrow bridge. This example shows why the registry keeps normative strength and mode action as distinct fields. A requirement can be derived from a should-level standards statement and still be given a blocking operational action in a profile that prioritizes safe import behavior.

Detector-kind distribution and normative strength The current registry contains 10 structural requirements, 4 policy requirements, and 3 import-crypto requirements. Likewise, the normative-strength distribution is not homogeneous: 15 requirements are labeled must and 2 are labeled should. Importantly, the two should-level rows are active importer checks with implemented detectors and blocking action. Policy requirements bring the PKIX semantics into the registry. Import-crypto requirements bring the importer boundary into the registry. The paper’s claim to be about assurance, rather than about a slightly larger structural linter, rests precisely on the coexistence of these classes in one executable profile. Single exercised mode split The single exercised mode split illustrates how the policy model is used. The requirement MLKEM-SPKI-ENCODE-DECODE-IDENTITY is implemented locally and triggered by a controlled SPKI mutation that preserves outer container shape while violating public-key canonicality. In strict the artifact blocks the case. In deployable it warns. The underlying detector evidence is the same, and the coverage summary still records the expected detection as met. Only the operator consequence changes. This avoids maintaining separate detector sets or using a deployable mode that suppresses evidence. The warning path remains visible in policy summaries, workflow outputs, and coverage reports. Policy outputs and operator-ready matrices The policy model is made inspectable through a family of generated outputs. The pair of policy summaries provides the mode-specific top-line view. The policy matrix freezes row-level actions across the registry. The stage-owner summary collapses the inventory by workflow boundary. The operatorgate matrix re-expresses the same policy in pack form. The workflow files bind these pieces into an owner/stage recipe, and the operator-readiness summary freezes the current default mode, reference mode, pack purposes, command lines, and files to inspect. This output family is the practical answer to a question that standards alone do not answer and that raw detector code answers only badly: what should an operator run, in which mode, at which stage, and how should the result be read? Because all of these outputs are generated from the same registry, the artifact creates a tight equivalence between policy as data, workflow as data, and paper claims about both.

Part III Evaluation

Corpus Design, Mutation Families, and Evaluation Protocol

Controlled corpus composition The empirical center of the paper is a frozen controlled corpus of 48 artifacts. The corpus is balanced by algorithm family, with 24 ML-KEM artifacts and 24 ML-DSA artifacts; it is nearly balanced by validity, with 21 valid and 27 invalid artifacts; and it is topologically balanced across the three active workflow surfaces fixed in Parts I and II, namely 14 certificate/profile artifacts, 20 SPKI/public-key artifacts, and 14 private-key-container/import artifacts. Because the corpus is indexed by stage, fault family, and expected detection, it functions as executable evidence for the operational model rather than as an undifferentiated box of “test files.” Table 4 freezes the composition of the primary evidence layer. The current artifact is evaluated against all three surfaces that matter operationally, and the SPKI slice is split between raw representation artifacts and certificate-carried SPKI defects. Table 4: Controlled corpus design. The table records the empirical geometry of the primary evidence layer: every active owner-stage row is exercised, every stage contains both valid and invalid material, and the SPKI slice is tested both on raw SPKI objects and on certificate-carried defects. Stage

Owner

Artifact forms

Valid

Invalid

Total

Representative exercised faults

certificate/profile

CA pre-issuance

14 certificates

SPKI/public-key

CA pre-issuance

17 raw SPKI objects + 3 certificate-carried SPKI defects

private-keycontainer/import

Artifact importer

14 private-key containers

PKIX keyUsage semantics, signature AlgorithmIdentifier parameter defects, HashML-DSA policy prohibition absent-parameters violations, payload-length defects, OID/payload inconsistency, ML-KEM canonicality mutation seed-form and expanded-form length defects, both inconsistency, ML-KEM expanded-key hash mismatch

Total

—

17 certificates, 17 raw SPKI objects, 14 private-key containers

7 fault families across certificate, SPKI, and importer boundaries

The type distribution is as follows: among the 48 artifacts, 17 are raw certificates, 17 are raw SPKI objects, and 14 are private-key containers. Valid artifact generation The 21 valid artifacts are generated locally through a deterministic OpenSSL path and then frozen by manifest and hash. They are not scraped from the public web, borrowed from the baseline, or post-edited 22

by hand. In the current corpus, there are 7 valid artifacts for each active stage: 7 valid certificates, 7 valid SPKI/public-key artifacts, and 7 valid private-key containers. Every active gate was exercised on a non-trivial valid set and produced no findings on that set. Invalid mutation families The 27 invalid artifacts are arranged into 7 labeled fault families: encoding/container, size/shape, interfield consistency, profile/usage-policy, field-domain, algorithm-policy, and import-validation. Each invalid artifact has a declared fault identity and a declared detection expectation before the detector is run. Table 5 summarizes the current mutation catalogue. For instance, the absent-parameters obligations are exercised separately with NULL and non-NULL parameter values; the ML-KEM canonicality rule is exercised by an unreduced ByteEncode12 coefficient mutation that preserves outer container shape; and the private-key importer slice includes a dedicated ML-KEM expanded-key hash mismatch rather than only trivial truncation cases. Table 5: Invalid mutation-family catalogue. Each family has an explicit operational purpose and a traceable relation to one or more requirement rows in the registry. Fault family

Count

Principal stage(s)

Representative artifacts

Assurance purpose

encoding/container

SPKI/public-key, certificate/profile

size/shape

SPKI/public-key, private-key/import

Exercise absent-parameters obligations for SPKI and certificate signature AlgorithmIdentifier fields Exercise parameter-set-specific payload, seed, and expanded-key length checks

inter-field consistency

SPKI/public-key, private-key/import

profile/usage-policy

certificate/profile

field-domain

SPKI/public-key

der-mut-mlkem768-spki-aid-n ull-pub, der-mut-mldsa44-cer t-signature-aid-octet-params der-mut-mlkem768-spki-paylo ad-truncated-pub, der-mut-mld sa44-key-expanded-short der-mut-mlkem512-spki-oid-s wapped-to-mlkem768-pub, der-m ut-mldsa44-key-both-mismatch openssl-mut-mlkem768-keyusag e-digital-signature-cert, der-mut-mldsa65-cert-keyusag e-empty der-mut-mlkem768-spki-unred uced-byteencode12-pub

algorithm-policy

certificate/profile

import-validation

private-key/import

der-mut-mldsa44-cert-signatu re-hashmldsa44 der-mut-mlkem512-key-hash-m ismatch

Exercise OID/payload agreement and both-form seed/expanded consistency Exercise positive and negative PKIX keyUsage semantics

Exercise ML-KEM decode/re-encode canonicality rather than mere container shape Exercise final-standards PKIX prohibition of HashML-DSA certificate signatures Exercise import-side cryptographic validation that cannot be reduced to certificate linting

Expected-detection labeling Every invalid artifact in the controlled corpus carries an explicit expected_detection label in the manifest. The label is requirement centric, an artifact therefore counts as successfully covered when the local run recovers the requirement identifiers that the corpus says ought to fire. The certificate mutations der-mut-mldsa44-cert-signature-aid-null and der-mut-mldsa44-c ert-signature-aid-octet-params, for example, trigger redundant error instances because the same absent-parameters rule is exercised at more than one certificate locus. Yet their first useful hit remains the same registry row, MLDSA-CERT-SIGNATURE-AID-PARAMS-ABSENT, and the evaluation should not overweight them merely because the certificate offers more than one place for the defect to surface. Evaluation protocol and success criteria The local artifact is executed twice over the full controlled corpus, once in strict and once in deployable. The success criteria are: 1. every invalid artifact should meet its expected detection set; 23

2. no valid artifact should be blocked or warned; 3. no unexpected requirement should become outcome-critical; and 4. stage-local coverage summaries should show no open detector gaps inside the declared scope. Figure 7 shows how the primary and supporting evidence lanes fit together. The controlled corpus is the primary lane. The certificate-only baseline comparison, the bounded public appendix, and the cross-tool behavior matrix are supporting lanes.

Deterministic valid generation 21 valid artifacts Manifest labeling stage, validity, fault family, expected detection, SHA-256

Requirement registry 17 active rows

Dual-mode local evaluation strict and deployable

Primary outputs extended_registry_ summary* certificate_spki_ coverage* private_key_ coverage*

Deterministic mutation families 27 invalid artifacts

Comparable certificate subset 17 certificates = 7 valid + 10 invalid

Public appendix 26 public artifacts

Cross-tool behavior layer 57 artifacts, 4 tool rows

Supporting outputs certificate-only baseline compare bounded public appendix cross-tool behavior matrix

Figure 7: Evaluation design with primary and supporting evidence lanes. The controlled corpus is the paper’s primary evidence layer; the baseline, appendix, and cross-tool layers remain supporting evidence.

Baseline comparison protocol The frozen baseline comparison is certificate-only. This is the fair slice, because the baseline can be executed on certificates in a way that is not directly matched for raw SPKI objects and private-key containers in the same CLI path [4]. The comparable slice therefore contains 17 certificates: 7 valid and 10 invalid. The 10 invalid cases include pure certificate-profile defects and certificate-carried SPKI defects. The local artifact is evaluated on that same slice, and the comparison is normalized in terms of useful detection, miss, pass, and fatal runtime failure. Bounded public appendix protocol The public appendix is a bounded support layer, it currently contains 26 public artifacts, split into 8 certificates and 18 private-key containers, across two provider paths, ossl35 and bc. The appendix is valid-only material: its job is to support external-validity discussion by showing that the operator-facing workflow is not confined to one local generation path. Cross-tool behavior protocol The cross-tool layer is behavioral, it covers 57 artifacts in total, comprising 31 controlled artifacts and the 26 appendix artifacts, for a total of 25 certificates and 32 private-key containers. Each row records tool behavior in one of five coarse classes: accepted, rejected-semantic, rejected-structural, runtime-failure,

or not-applicable. The purpose is to make visible the difference between parse/import acceptance and policy conformance. That distinction is especially important for OpenSSL. In this matrix, OpenSSL is read only as a parse/import signal. Reproducibility conditions All three evidence lanes are pinned to frozen local state. The replay entrypoint rebuilds or reuses the frozen third-party snapshots, reruns corpus generation and mutation, replays strict and deployable evaluation, regenerates coverage and policy outputs, refreshes baseline comparison and cross-tool behavior, and refreshes release and claim-lock metadata. The importer slice depends on a narrow local bridge over a frozen libcrux substrate; the baseline lane depends on a frozen JZLint snapshot with explicitly recorded runtime behavior on this host [1, 4].

Controlled Results

Overall strict/deployable outcomes In strict the 48-artifact corpus yields 27 invalid blocks and 21 passes. In deployable it yields 26 invalid blocks, 1 invalid warning, and the same 21 passes. In both modes, all 27 invalid artifacts meet their expected detection labels, no valid artifact is blocked or warned, and no unexpected errors become outcome-critical. The deployable warning preserves detection and changes only the operator action on a single known condition. Table 6 records these results at the stage level. All three stages meet the declared success criteria without valid-set findings. Table 6: Controlled results by stage and mode. The only mode split in the entire corpus is a single ML-KEM SPKI canonicality artifact that blocks in strict and warns in deployable. Valid pass

Strict block

Strict warn

Deployable block

Deployable warn

certificate/profile SPKI/public-key private-keycontainer/import

7 7 7

7 13 7

0 0 0

7 12 7

0 1 0

7/7 13/13 7/7

0 0 0

Total

27/27

Stage

Expected invalid False positives detected

Per-stage outcomes The certificate/profile slice contributes 7 valid passes and 7 invalid blocks in both modes. The privatekey/import slice has the same shape. The SPKI slice is larger, with 7 valid passes and 13 invalid artifacts, and it is also the only stage where mode action changes: one invalid artifact, the unreduced ML-KEM ByteEncode12 case, blocks in strict and warns in deployable.

strict block

deployable block

Invalid artifacts

deployable warn

13 12

10 7 7

7 7

5 1

0 fi

certi

file /pro cate

SPK

b I/pu

y ic-ke

0 ate-k priv

port ey/im

Figure 8: Mode action by stage over the invalid side of the controlled corpus. Each stage also has 7 valid passes in both modes, omitted here for readability.

Certificate/profile results The certificate/profile stage contains 7 invalid artifacts spanning PKIX usage semantics, signature AlgorithmIdentifier conformance, and final-policy closure. All 7 are blocked in both modes. The stage exercises all 5 active certificate/profile requirements, and the most interesting point is qualitative: the stage covers positive semantics as well as negative bit forbiddance. Two invalid artifacts exercise MLKEM-CERT-KU-KEYENCIPHERMENT-ONLY; two exercise the positive ML-DSA signing-bit requirement MLDSA-CERT-KU-AT-LEAST-ONE-SIGNING-BIT; two exercise the ML-DSA certificate-signature absentparameters rule; and one exercises the HashML-DSA PKIX prohibition [3, 7]. If the certificate stage were only catching malformed AlgorithmIdentifier parameters, the work would still be useful, but what makes the stage stronger is that it also catches semantic emptiness and policy violations that matter directly to a CA operator. An empty keyUsage extension in an ML-KEM or ML-DSA certificate is a misprofiled issuance artifact. The local results treat it that way. SPKI/public-key results The SPKI/public-key stage is the richest slice of the controlled corpus. Its 13 invalid artifacts comprise 10 raw SPKI defects and 3 certificate-carried SPKI defects. Four cases exercise MLKEM-SPKI-AID-PAR AMS-ABSENT, two exercise MLDSA-SPKI-AID-PARAMS-ABSENT, four exercise MLKEM-SPKI-PUBLIC-K EY-LENGTH, two exercise MLDSA-SPKI-PUBLIC-KEY-LENGTH, and one exercises the canonicality rule MLKEM-SPKI-ENCODE-DECODE-IDENTITY. In strict all 13 are blocked. In deployable 12 are blocked and the canonicality case warns. Some defects are pure representation failures on raw SPKI material. Some are inter-field consistency failures where OID and payload geometry disagree. Some are carried through a certificate shell but still conceptually belong to the SPKI boundary. The stage therefore tests exactly what the paper claims to cover: assurance across representation and profile boundaries rather than only at the certificate surface [6, 7]. Private-key/import results The importer slice matches the CA slices on the reported metrics, and this is one of the central empirical results in the paper. All 7 active private-key/import requirements are covered, all 7 corresponding invalid artifacts are detected in both modes, and the stage carries no false positives. Four invalid artifacts belong to the ML-KEM importer slice and three to the ML-DSA importer slice. Each invalid artifact yields the expected first useful requirement hit, which means the stage is complete in aggregate and interpretable artifact by artifact. 26

Table 7: Importer-stage detection grid. The private-key slice is fully exercised and detected in both modes. Family

Exercised importer requirements

Invalid artifacts

Outcome

ML-KEM ML-DSA

seed length, expanded length, both consistency, expanded-key hash check seed length, expanded length, both consistency

4 3

4/4 detected in both modes 3/3 detected in both modes

Total

all 7 active importer requirements covered

7/7 detected in both modes

Redundant detections and first-hit interpretation Two artifacts in the controlled corpus deliberately produce redundant error instances: der-mut-mldsa 44-cert-signature-aid-null and der-mut-mldsa44-cert-signature-aid-octet-params. Both exercise the same certificate-signature absent-parameters rule at more than one certificate location. The local artifact reports two error instances but only one unique requirement. Error-free valid set and false-positive analysis All 21 valid artifacts pass in both modes. There are no blocking valid artifacts, no warning valid artifacts, and no unexpected errors on the valid side. The valid set is evenly distributed across stages, with 7 valid certificate/profile artifacts, 7 valid SPKI/public-key artifacts, and 7 valid private-key containers. This is the practical complement to the 27/27 invalid coverage result.

Baseline Insufficiency Analysis

Why certificate-only is the fair slice The frozen baseline comparison must be read through a narrow lens. The lens is certificate-only, and that is the fairest lens available. The baseline is a real current-state artifact and remains useful as secondary evidence, but it is not directly executable over raw SPKI objects and private-key containers in the same workflow shape as the local artifact [4]. For that reason, the comparison slice is fixed to 17 certificates: 7 valid and 10 invalid. The invalid side includes both direct certificate-profile defects and certificate-carried SPKI defects. Headline result: 5/10 versus 10/10 Within the fair certificate slice, the gap is already substantial. The frozen baseline meets 5 of the 10 expected invalid detections. The local artifact meets all 10 of 10. At the same time, the baseline fatally rejects 3 valid ML-KEM certificates, while the local artifact fatally rejects none. These numbers leave the baseline informative, but insufficient as an operator assurance path for the covered profile. Frozen baseline

10 Artifacts

Extended local artifact

7 5

3 0 ted Detec

0 id inval

d Misse

0 alid atal v

id inval

Figure 9: Certificate-only comparison on the fair slice. 27

pass Valid

The gap is split between two operator-relevant failure modes: incomplete invalid detection and runtime fragility on valid material. Fatal valid-certificate fragility The three fatal valid failures all occur on valid ML-KEM end-entity certificates for parameter sets 512, 768, and 1024. In the local evidence frame, it is evidence about the frozen baseline path on this host rather than a universal theorem about every future environment or every possible build of the baseline. A certificate-level assurance path that can fatally fail on valid PQ certificates is operationally brittle. The local artifact avoids that brittleness on the same slice. For an operator, a fatal rejection on valid input is worse than a quiet miss on some invalid cases as it breaks trust in the gate itself. Positive semantics versus prohibited-bit checking One of the most informative requirement-level patterns is the contrast between positive semantics and prohibited-bit checking. The baseline does recover the encipherment/agreement prohibition on the ML-DSA certificate mutation openssl-mut-mldsa65-keyusage-key-encipherment-cert; yet it does not recover the positive requirement that at least one signing-related bit be set. Consequently, it misses the empty-keyUsage case der-mut-mldsa65-cert-keyusage-empty and does not fully model the operational semantics of a valid ML-DSA certificate profile. A parallel pattern appears on the ML-KEM side. The baseline catches the explicitly prohibited digitalSignature mutation but misses the empty keyUsage case. The local artifact detects both, because MLKEM-CERT-KU-KEYENCIPHERMENT-ONLY is implemented as a profile rule rather than as a partial prohibited-bit test. These two patterns show that final PKIX assurance cannot be reduced to looking for the wrong bits; it also has to reason about the required semantics of the right ones [3, 7]. Requirement-level gap analysis Table 8 gives the requirement-level decomposition of the certificate-only comparison. Part III specifies which requirement families are fully recovered, which are only partially recovered, which are absent, and which are blocked by runtime fragility rather than by a true semantic detector. Table 8: Requirement-level decomposition of the fair certificate-only comparison. “Baseline useful detections” counts semantic or structural hits; “blocked by fatal” counts cases where the baseline never reached a useful decision because the runtime path failed. Expected invalids

Baseline useful detections

Blocked by fatal

Extended detections

certificate/profile

incomplete

certificate/profile

covered-for-prohibitedbits partial

certificate/profile

gap

SPKI/public-key

partial

SPKI/public-key

gap-or-unverified

certificate/profile

incomplete

SPKI/public-key

partial

SPKI/public-key

covered-by-external-lintpath covered-for-encoded-key

Requirement

Stage

MLDSA-CERT-KU-AT-LEAST -ONE-SIGNING-BIT MLDSA-CERT-KU-NO-ENCIP HERMENT-OR-AGREEMENT MLDSA-CERT-SIGNATURE-A ID-PARAMS-ABSENT MLDSA-PKIX-HASHML-FOR BIDDEN MLDSA-SPKI-AID-PARAM S-ABSENT MLDSA-SPKI-PUBLIC-KEY -LENGTH MLKEM-CERT-KU-KEYENCI PHERMENT-ONLY MLKEM-SPKI-AID-PARAM S-ABSENT MLKEM-SPKI-ENCODE-DEC ODE-IDENTITY MLKEM-SPKI-PUBLIC-KEY -LENGTH

Baseline status

Three patterns stand out. First, positive certificate semantics are the clearest coverage gap, especially for ML-DSA signing-bit presence and the empty keyUsage cases. Second, final-policy closure on HashMLDSA remains a true gap rather than merely a runtime casualty. Third, some ML-KEM structural coverage is entangled with the baseline’s external encoded-key path, which means that even where there is conceptual coverage, there may still be unusable runtime behavior on the way to that coverage. What the baseline comparison does and does not prove The comparison proves a bounded and useful proposition: on the fair certificate-only slice, the frozen baseline is insufficient as an assurance path for the covered profile because it both misses expected invalid artifacts and shows runtime fragility on valid material. That result supports the paper’s architectural claim that workflow-centric PQ assurance has not been solved by simply adding some PQ lints to an existing certificate path. The comparison does not prove that the baseline is worthless, that no other environment could improve its behavior, or that raw-SPKI and private-key surfaces are directly comparable to its current CLI.

Policy Closure Case Studies

HashML-DSA prohibition A direct example of policy closure in the current corpus is the HashML-DSA prohibition for the covered PKIX certificate profile. RFC 9881 fixes the final ML-DSA PKIX conventions and excludes HashML-DSA from the covered certificate-signature path [3]. The local artifact turns that clause into the blocking requirement MLDSA-PKIX-HASHML-FORBIDDEN. The mutation der-mut-mldsa44-cert-signature -hashmldsa44 then exercises that requirement directly. The clause becomes an executable gate: the artifact blocks the case, the expected detection is met, and the baseline leaves the case uncovered. ML-DSA positive signing semantics The ML-DSA keyUsage rules illustrate why operational assurance needs positive semantics as well as prohibitions. The mutation openssl-mut-mldsa65-keyusage-key-encipherment-cert exercises both the positive requirement that at least one signing-related bit be present and the negative requirement that encipherment/agreement semantics be absent. The mutation der-mut-mldsa65-cert-key usage-empty isolates the positive side by presenting an empty keyUsage extension. The local artifact blocks both cases. The baseline, by contrast, recovers only the negative encipherment/agreement semantics and leaves the positive requirement incomplete. Operationally, this means that an empty or signing-less keyUsage extension is still unacceptable even if it contains no forbidden encryption bit. The registry model lets the paper encode “must include a signing semantic” as a first-class requirement. ML-KEM keyUsage semantics The ML-KEM certificate rule has the same structural lesson. RFC 9935 says that if keyUsage is present, keyEncipherment must be the only active bit [7]. The local artifact therefore treats the mutations openssl-mut-mlkem768-keyusage-digital-signature-cert and der-mut-mlkem768-cert-key usage-empty as two faces of the same profile rule. The baseline catches the explicit prohibited-bit case and misses the empty case. ML-KEM encode/decode identity as deployable warning The only exercised mode split in the current artifact occurs on MLKEM-SPKI-ENCODE-DECODE-IDENTITY. The mutation der-mut-mlkem768-spki-unreduced-byteencode12-pub preserves the outer SPKI shape and payload length while injecting a coefficient value that decodes but does not round-trip

canonically under the ML-KEM encode/decode relation [6, 7]. In strict the artifact blocks the case. In deployable it warns. The expected detection remains met in both modes. General pattern: from clause to gate Table 9 and Figure 10 summarize the more general pattern. The reusable contribution lies in the method that turns final standards text into registry rows, mutation families, expected detections, and operator actions. Table 9: Policy-closure case studies. The rows illustrate the same reusable pattern: a normative clause is translated into a requirement, exercised by a named mutation, and surfaced as an operator-visible gate decision. Source clause

Requirement

Exercising mutation(s)

strict

deployable

What the case shows

RFC 9881 HashML-DSA exclusion for the covered certificate profile

MLDSA-PKIX-HASHML-FOR BIDDEN

der-mut-mldsa44-cert-s ignature-hashmldsa44

block

RFC 9881 signing-semantics requirement for ML-DSA certificates

MLDSA-CERT-KU-AT-LEAST -ONE-SIGNING-BIT

openssl-mut-mldsa65-key usage-key-enciphermen t-cert; der-mut-mldsa65 -cert-keyusage-empty

block

RFC 9935 keyEnciphermentonly rule for ML-KEM certificates

MLKEM-CERT-KU-KEYENCI PHERMENT-ONLY

openssl-mut-mlkem768-k eyusage-digital-signatu re-cert; der-mut-mlkem76 8-cert-keyusage-empty

block

FIPS 203 / RFC 9935 canonicality at the ML-KEM SPKI boundary

MLKEM-SPKI-ENCODE-DEC ODE-IDENTITY

der-mut-mlkem768-spki-u nreduced-byteencode12-p ub

block

warn

Final-policy closure becomes an executable certificate gate; the baseline leaves the case uncovered Positive semantics matter; “no forbidden bit” is not enough for a valid signing profile Profile correctness requires both the right bit and the absence of the wrong ones The mode split is evidence-preserving: the same defect is detected in both modes, but operator action changes

Normative clause FIPS / RFC text

Registry row ID, owner, stage, detector kind, mode action

Mutation family named artifact exercising the clause

Evaluation record expected detection met, first useful hit

Operator gate block / warn / pass

Figure 10: From standards clause to operator gate. The case studies in Table 9 are instances of the same reproducible translation pattern.

Part IV Significance

Operator Workflow and Deployment Guidance

What the CA must run The controlled results in Section 9 are useful only if they can be turned into a stable operating recipe for the people who issue or import artifacts. In the current pkix-core release line, the certification authority owns two active pre-issuance gates: ca-certificate-profile and ca-spki-public-key. Together, they cover the full CA-side requirement inventory of 10 active requirements: 5 at the certificate/profile surface and 5 at the SPKI/public-key surface. In deployable, the operator runs ./experiments/run_extended.sh --mode deployable and ./experiments/run_coverage.sh --mode deployable. In strict, the same path is replayed with --mode strict. The same artifact can therefore support two operational postures: a low-noise issuance posture and a maximal-assurance audit posture. The outputs inspected by the CA are equally important. For the certificate/profile surface, the decisive outputs are results/extended_registry_summary_deployable.json, results/policy_summary _deployable.json, results/certificate_spki_coverage_deployable.json, and results/oper ator_readiness_summary.json, with the strict analogues used for audit replay. For the SPKI/publickey surface, the same summary and policy artifacts apply, with results/operator_gate_matrix.json added when the operator needs a direct gate-pack view. The CA therefore runs a named gate, in a named mode, with named outputs that support an issuance decision. What the artifact importer must run The importer owns the import-private-key gate and, in the current profile, all 7 private-key-container/import requirements. This path is a separate assurance frontier whose inputs, detector kinds, and failure semantics differ materially from the CA side. The importer recipe therefore includes one step that the CA recipe does not: building the narrow import-validation bridge with ./experiments/build_libcrux_import_check.sh. After that, the importer runs the same registry-driven evaluator in either deployable or strict, followed by ./experiments/run_private_key_coverage.sh --mode <mode>. The outputs of interest are results/private_key_coverage.json or results/private_key_coverage_deployable.json, together with the shared policy summaries and gate matrices. The operator then decides whether a private-key container can be admitted to import, must be rejected outright, or should be escalated for deeper audit. The distinction between importer and CA prevents the manuscript from treating all PKIX assurance as if it were reducible to certificate parsing. The importer needs a stable answer to a narrower question: “Can this container be imported into the covered implementation substrate under the declared profile?” Default deployable mode and strict audit mode 31

The two-mode policy model reflects distinct operational postures. Some checks must always block. Others are better treated as evidence-preserving warnings in a deployable issuance context while remaining blocking in a strict conformance context. In the current release line, deployable is the default CA-facing posture. It keeps the same detection surface as strict for the controlled corpus, but downgrades exactly one exercised requirement, MLKEM-SPKI-ENCODE-DECODE-IDENTITY, from block to warn. All other active requirements remain blocking. The practical effect is a different operator consequence for a single canonicality condition at the ML-KEM SPKI boundary. By contrast, strict remains the reference assurance posture. It should be used for pre-release audits, claims reproduction, corpus-extension work, and any situation where the operator wants the artifact to present the hardest possible line. The same evidence model is used for both postures. Incoming artifacts certificate / SPKI / private-key container

Shared registry and policy layer owner, stage, gate pack, mode action

CA pre-issuance

Artifact importer

Run ca-certificate-profile and ca-spki-public-key

Build import bridge build_libcrux_ import_check.sh

Default: deployable Audit replay: strict

Run import-private-key in deployable or strict

Inspect extended_registry_ summary*, policy_summary_*, certificate_spki_coverage*, operator_gate_matrix.json

Inspect private_key_coverage*, policy_summary_*, operator_gate_matrix.json

issue / hold / block

import / reject / escalate

Strict audit replay

Figure 11: Operator execution workflow in the current pkix-core release line.

Outputs to inspect and decisions to make The workflow becomes tangible through outputs. Some are shared across the artifact regardless of stage, such as results/policy_matrix.csv, results/stage_owner_summary.json, and 32

results/reference_workflow.json. Others are mode-specific and stage-aware summaries that tell the operator which requirements block, which warn, and which surfaces were exercised without findings. Table 10 compresses the operator-facing view. This is the paper’s answer to the “what do I actually run?” question. Table 10: Operator execution matrix. The table gives the shortest faithful recipe for each active gate pack, including the commands to run, the outputs to inspect, and the decision supported by those outputs. Gate pack

Owner

Default mode

ca-certificateprofile

deployable

ca-spki-public-key

import-private-key

Commands

run_extended.sh --mode deployable; run_coverage.sh --mode deployable audit replay: same commands with --mode strict CA deployable run_extended.sh --mode deployable; run_coverage.sh --mode deployable audit replay: same commands with --mode strict Importer deployable build_libcrux_import or strict _check.sh; run_extended.sh --mode <mode>; run_private_key_cove rage.sh --mode <mode>

Outputs to inspect

Operator decision

extended_registry_su mmary_*, policy_summary_*, certificate_spki_cov erage*, operator_rea diness_summary.json

Issue, hold, or block on certificate-profile semantics before issuance

extended_registry_su mmary_*, policy_summary_*, certificate_spki_cov erage*, operator_gat e_matrix.json

Issue, hold, or block on SPKI structure, parameters, and key-material conditions before issuance

private_key_coverage *, extended_registry_ summary_*, policy_summary_*, operator_gate_matrix .json

Import, reject, or escalate based on container form, length, and consistency checks before use

Supporting External Evidence

Table 11 summarizes the support layer. Table 11: Supporting external evidence layers. Evidence layer

Count

Surface

Coverage highlights

What it supports

What it does not support

Controlled corpus

certificate, SPKI, private-key

Main performance claims, operator workflow claims, requirement-level closure

Bounded public appendix

certificate, private-key

21 valid, 27 invalid; all 17 active requirements exercised; strict and deployable views 2 providers; 8 certificates; 18 private-key containers; all 6 parameter sets

Cross-tool behavior matrix

certificate, private-key

4 tool rows; 31 controlled artifacts and 26 appendix artifacts

Parse-versus-policy divergence and baseline/runtime fragility patterns

Internet-scale prevalence, universal toolchain claims Census claims, invalid-coverage generalization, ecosystem-rate inference Proof that any given external tool is policyconformant or normatively complete

Bounded external-validity support for valid certificate and private-key handling

Appendix behavior against baseline The appendix certificate slice contains 8 valid certificates, all of which the local artifact accepts without findings. The frozen baseline, by contrast, fatally rejects 4 of those 8 valid certificates, all of them in 33

the ML-KEM family. In this appendix slice there are no invalid certificates, so the comparison is about whether externally sourced but in-scope valid certificates survive contact with the baseline. Cross-tool behavior and parse-versus-policy divergence In the current frozen run, it covers 57 artifacts in total, including 25 certificates and 32 private-key containers, drawn from both the controlled corpus and the public appendix. Four tool rows are recorded: the local extended artifact, the frozen JZLint baseline, the OpenSSL CLI path, and pkilint in its available-or-insufficient state. The local artifact exhibits structured policy behavior across the full matrix, with 40 acceptances, 8 semantic rejections, and 9 structural rejections. The baseline is certificate-only, and is therefore not applicable to all 32 private-key-container artifacts; on the applicable certificate slice it still exhibits 9 runtime failures. The OpenSSL path accepts 50 artifacts and rejects 7 structurally. Finally, pkilint appears as unavailable-or-insufficient.

extended-local jzlint-baseline openssl-cli pkilint 0

artifact count accepted

rejected-semantic

rejected-structural

runtime-failure

not-applicable

Figure 12: Cross-tool behavior is evidence of divergence. Parse acceptance and policy conformance separate materially across the current tool rows.

Limitations and Threats to Validity

Table 12 condenses all five threat classes to validity. Table 12: Threats-to-validity matrix. Each threat is paired with the concrete mitigation already built into the artifact or the manuscript framing. Threat class

Limiting fact

Mitigation in this paper

Claims protected by the mitigation

Construct validity

Only pkix-core and 17 active requirements are executable; runtime-consumer remains out of scope Baseline comparison is certificate-only and baseline runtime fragility appears on the frozen host Public appendix is small, curated, and valid-heavy

State owner/stage boundaries explicitly and refuse runtime claims that the artifact does not execute

Workflow-centric assurance claim remains narrow and defensible

Frame baseline evidence as certificate-level insufficiency rather than universal head-to-head superiority Use appendix as bounded support only; exclude prevalence or ecosystem-rate rhetoric Interpret the matrix behaviorally and distinguish acceptance from conformance Anchor claims to the current final normative floor and the current profile version

Comparative claims remain fair and stage-bounded

Comparison validity

External validity

Toolchain validity

Normative drift

External rows mix policy-aware evaluation, parse-only signals, and unavailable paths Future profile documents or errata may alter the best registry encoding

External-support claim remains modest and honest Cross-tool discussion supports divergence claims without overreach Final-standards framing remains temporally explicit rather than timelessly asserted

Conclusion

Final standards settle the normative floor for ML-KEM and ML-DSA in X.509/PKIX, but they do not by themselves yield operational assurance. The central result of this paper is that post-quantum assurance becomes actionable only when final normative clauses are translated into owner-assigned, stage-specific, and mode-aware workflow decisions. In the narrow but executable pkix-core profile, that translation is realized as a registry-driven assurance artifact spanning certificate/profile, SPKI/public-key, and private-key-container/import surfaces, organized into operator-facing gate packs for CA pre-issuance and artifact import. Within that profile, the paper shows that a reproducible assurance workflow can be built and evaluated with disciplined scope. The current artifact reifies 17 active requirements from the final standards corpus, assigns them by owner and stage, and exercises them against a frozen mutation-based corpus containing 48 artifacts across valid and invalid cases. On that primary evidence layer, the artifact meets all expected invalid detections, produces no false positives on the valid set, and preserves the same underlying detection coverage across strict and deployable modes, with a single explicit warning downgrade on an ML-KEM SPKI canonicality condition. Just as importantly, the importer-owned private-key boundary is treated as a first-class assurance surface rather than as an afterthought of certificate linting, and all 7 active importer requirements are covered in the present release line. The comparative and supporting evidence sharpen the operational meaning of these results. On the fair certificate-only slice, the frozen baseline misses expected invalid cases and exhibits fatal fragility on some valid ML-KEM certificates, whereas the local artifact closes the same slice without fatal valid rejections. The public appendix and the cross-tool matrix further show that parse acceptance, structural validity, profile conformance, and import readiness are materially different judgments. That distinction is precisely why post-quantum X.509 assurance cannot be reduced to parser success, certificate-only linting, or isolated algorithm-aware checks. The broader contribution of the paper is therefore methodological as much as empirical. It offers a reproducible pattern for turning standards prose into executable assurance: extract a requirement, normalize it into a checkable clause, assign it to an owner and stage, bind it to mutation-backed evidence, and expose the result through an operator-facing policy surface. In that sense, the paper extends prior PQ public-key linting work from detector catalogs toward accountable operational workflow. The point is to make assurance decisions reviewable, replayable, and attributable before issuance and before import. The work does not claim runtime-consumer coverage, ecosystem prevalence, universal tool behavior, or full PQ-family breadth beyond ML-KEM and ML-DSA. The next steps are clear: extend the registry discipline to runtime-consumer boundaries, widen artifact-family coverage where executable evidence can be maintained, broaden bounded external support without collapsing into prevalence rhetoric, and continue refining mode-aware policy for deployment-facing use. The present result establishes that once final post-quantum standards exist, the essential assurance task is no longer to ask only whether an artifact parses, but whether the right owner can justify the right decision at the right boundary with replayable evidence.

References [1] cryspen. libcrux Frozen Snapshot. Project-local frozen import-validation substrate; internal snapshot commit 6b9eca5a7b507e1d8423f85e5711572b4a661e8d. 2026. [2] Evangelos Karatsiolis et al. “Public Key Linting for ML-KEM and ML-DSA”. In: Applied Cryptography and Network Security Workshops. Ed. by Mark Manulis. Vol. 15654. Lecture Notes in Computer Science. Cham: Springer, 2026, pp. 337–362. doi: 10.1007/978-3-032-01806-9_18. [3] Jake Massimo et al. Internet X.509 Public Key Infrastructure – Algorithm Identifiers for the ModuleLattice-Based Digital Signature Algorithm (ML-DSA). RFC 9881. Oct. 2025. doi: 10.17487/RFC9881. [4] MTG AG. JZLint Frozen Snapshot. Project-local frozen certificate-level baseline; internal snapshot commit d6fdf02ad31f085e88d252b368f50e9da87debfd. 2026. [5] National Institute of Standards and Technology. Module-Lattice-Based Digital Signature Standard. Federal Information Processing Standards Publication 204. Aug. 2024. doi: 10.6028/NIST.FIPS. 204. [6] National Institute of Standards and Technology. Module-Lattice-Based Key-Encapsulation Mechanism Standard. Federal Information Processing Standards Publication 203. Aug. 2024. doi: 10. 6028/NIST.FIPS.203. [7] Sean Turner et al. Internet X.509 Public Key Infrastructure - Algorithm Identifiers for the ModuleLattice-Based Key-Encapsulation Mechanism (ML-KEM). RFC 9935. Mar. 2026. doi: 10.17487/ RFC9935.

Full Requirement Catalogue

The body text presents the registry as an operational object. This appendix makes the registry inspectable row by row. The catalogue is extracted from the final normative floor given by FIPS 203, FIPS 204, RFC 9881, and RFC 9935 [6, 5, 3, 7], then frozen into a machine-readable schema whose records can be audited, mutated, replayed, and cited without rewriting the paper each time a result table is rebuilt. Requirement schema The executable registry keeps more structure than a flat list of lint names. Each record carries provenance, operational ownership, fault-family alignment, detector expectation, and per-mode action. Table 13 summarizes the fields that matter most for review and replay. Table 13: Registry schema fields used by the executable requirement catalogue. Field

Role in the executable registry

Stable requirement identifier used by the registry, policy summaries, coverage reports, and expected-detection labels. Covered algorithm family, either ML-KEM or ML-DSA. Concrete artifact surface: certificate, spki, or private-key-container. Operational stage at which the check is owned and executed. Responsible workflow owner, namely CA pre-issuance or artifact importer. Operator-facing gate grouping exposed by the workflow. Fault class exercised by the mutation catalogue and used for coverage accounting. Natural-language executable clause distilled from the normative sources. Detector or validator expected to fire when the requirement is exercised. Structural, policy, or import-crypto detector category. Normative level as recorded from the source text, currently must or should. Position of the frozen baseline relative to this requirement: covered, partial, incomplete, gap, or external-lint only. Whether the project can construct and exercise the requirement in the frozen corpus. Per-mode operator consequence, recorded separately for strict and deployable. Normative source anchors used to justify the clause and audit the extraction.

algorithm artifact_type stage owner gate_pack fault_family requirement expected_detector detector_kind normative_strength baseline_status constructibility mode_action source / source_locators

ML-KEM requirements The current pkix-core profile contains eight active ML-KEM requirements: two at the certificate and SPKI issuance boundary and four at the importer boundary, plus the exercised encode/decode identity rule that becomes the only deployable warning. Table 14: ML-KEM requirement catalogue in the current pkix-core registry. The S and D columns denote strict and deployable actions. ID

Surface / owner Executable clause

Detector

Base

MLKEM-SPKI-AID-PAR AMS-ABSENT

SPKI / CA

structural

block

partial

MLKEM-CERT-KU-KEYEN CIPHERMENT-ONLY MLKEM-SPKI-PUBLIC-K EY-LENGTH MLKEM-SPKI-ENCODE-D ECODE-IDENTITY

cert/profile / CA SPKI / CA

policy

block

incomplete

structural

block

structural

block

warn

covered-forencoded-key covered-byexternal-lintpath

SPKI / CA

SPKI AlgorithmIdentifier uses the correct ML-KEM OID and absent parameters. if keyUsage is present, only keyEncipherment may be active. SPKI public-key payload length matches the parameter set. ML-KEM decode/re-encode is identity on the encapsulation key.

Continued on next page

Table 14: ML-KEM requirement catalogue in the current pkix-core registry. The S and D columns denote strict and deployable actions. (continued) ID

Surface / owner Executable clause

MLKEM-PRIVATE-SEE D-LENGTH MLKEM-PRIVATE-EXPAN DED-LENGTH MLKEM-PRIVATE-BOT H-CONSISTENCY MLKEM-PRIVATE-EXPAN DED-HASH-CHECK

priv/import / importer priv/import / importer priv/import / importer priv/import / importer

Detector

Base

seed-form private key length is 64 bytes. structural

block

gap

expanded-form private key length matches the parameter set. both-form ML-KEM import rejects seed/expanded inconsistency. expanded-form ML-KEM import performs the hash check before acceptance.

structural

block

gap

importcrypto importcrypto

block

gap

block

gap

ML-DSA requirements The current pkix-core profile contains nine active ML-DSA requirements: four at the certificate boundary, two at the SPKI boundary, and three at the importer boundary. The distinguishing policy closure point is that positive certificate-profile semantics are encoded as first-class requirements alongside prohibited-bit checking. Table 15: ML-DSA requirement catalogue in the current pkix-core registry. The S and D columns denote strict and deployable actions. ID

Surface / owner Executable clause

Detector

Base

MLDSA-SPKI-AID-PAR AMS-ABSENT

SPKI / CA

structural

block

partial

MLDSA-CERT-SIGNATU RE-AID-PARAMS-ABSEN T MLDSA-CERT-KU-AT-L EAST-ONE-SIGNING-B IT MLDSA-CERT-KU-NO-E NCIPHERMENT-OR-AGR EEMENT MLDSA-SPKI-PUBLIC-K EY-LENGTH MLDSA-PKIX-HASHML-F ORBIDDEN MLDSA-PRIVATE-SEE D-LENGTH MLDSA-PRIVATE-EXPAN DED-LENGTH MLDSA-PRIVATE-BOT H-CONSISTENCY

cert/profile / CA

SPKI AlgorithmIdentifier uses the correct ML-DSA OID and absent parameters. certificate signatureAlgorithm uses an ML-DSA OID with absent parameters.

structural

block

partial

cert/profile / CA

if keyUsage is present, at least one signing bit must be active.

policy

block

incomplete

cert/profile / CA

keyUsage forbids encipherment and agreement bits for ML-DSA.

policy

block

SPKI / CA

SPKI public-key payload length matches structural the parameter set. HashML-DSA is forbidden in the policy covered PKIX certificate profile. seed-form private key length is 32 bytes. structural

block

covered-forprohibitedbits gap-orunverified gap

block

gap

structural

block

gap

importcrypto

block

gap

cert/profile / CA priv/import / importer priv/import / importer priv/import / importer

expanded-form private key length matches the parameter set. both-form ML-DSA import rejects seed/expanded inconsistency.

Gate-pack index The requirement rows above are operator-facing only when bundled into named gate packs. Table 16 gives the compact index used by the CA and importer workflows.

Table 16: Operator gate-pack index for the frozen release line. Gate pack

Surface / owner

Title

Requirement IDs

Mode note

Strict commands

ca-certifica te-profile

cert/profile / CA

CA certificate/profile gate

MLDSA-CERT-KU-AT-LEAST-ONE-S IGNING-BIT, MLDSA-CERT-KU-NO-E NCIPHERMENT-OR-AGREEMENT, MLDSA-CERT-SIGNATURE-AID-PARAM S-ABSENT, MLDSA-PKIX-HASHML-FORBIDDEN, MLKEM-CERT-KU-KEYENCIPHERMENT -ONLY MLDSA-SPKI-AID-PARAMS-ABSENT, MLDSA-SPKI-PUBLIC-KEY-LENGTH, MLKEM-SPKI-AID-PARAMS-ABSENT, MLKEM-SPKI-ENCODE-DECODE-IDENT ITY, MLKEM-SPKI-PUBLIC-KEY-LENGTH MLDSA-PRIVATE-BOTH-CONSISTEN CY, MLDSA-PRIVATE-EXPANDED-LENGTH, MLDSA-PRIVATE-SEED-LENGTH, MLKE M-PRIVATE-BOTH-CONSISTENCY, MLKEM-PRIVATE-EXPANDED-HASH-C HECK, MLKEM-PRIVATE-EXPANDED-LENGTH, MLKEM-PRIVATE-SEED-LENGTH

strict 5 block / deployable 5 block, 0 warn

experiments/run_exte nded.sh--modestrict, experiments/run_cove rage.sh--modestrict

strict 5 block / deployable 4 block, 1 warn

experiments/run_exte nded.sh--modestrict, experiments/run_cove rage.sh--modestrict

strict 7 block / deployable 7 block, 0 warn

experiments/build_li bcrux_import_check.sh, experiments/run_exte nded.sh--modestrict, experiments/run_priv ate_key_coverage.s h--modestrict

ca-spki-publi SPKI / CA c-key

import-priva te-key

CA SPKI/public-key gate

priv/import / importer

Importer private-key gate

Controlled Corpus Inventory and Mutation Catalogue

The controlled corpus is the main evidence bed of the paper. It is intentionally small enough to be auditable and large enough to exercise every active requirement on both the valid and mutated sides. All artifact identifiers below appear in the frozen manifest and can be replayed exactly from the packaged artifact. Valid artifacts The valid side of the controlled corpus contains 21 locally generated artifacts: 7 certificates, 7 SPKI/publickey artifacts, and 7 private-key containers. The This stage symmetry ensures that every active assurance frontier is exercised on a non-trivial valid set before invalid mutations are considered. Table 17: Valid artifacts in the frozen controlled corpus. Artifact ID

Parameter set

Surface

Path

openssl-mldsa44-ee-pub spki

ML-DSA-44

SPKI

openssl-mldsa65-ca-pub spki

ML-DSA-65

SPKI

openssl-mldsa65-ee-pub spki

ML-DSA-65

SPKI

openssl-mldsa87-ee-pub spki

ML-DSA-87

SPKI

spki

ML-KEM-1024

SPKI

spki

ML-KEM-512

SPKI

spki

ML-KEM-768

SPKI

certificate

ML-DSA-44

cert/profile

certificate

ML-DSA-65

cert/profile

corpus/valid/openssl/openssl_mldsa 44_ee_pub.pem corpus/valid/openssl/openssl_mldsa 65_ca_pub.pem corpus/valid/openssl/openssl_mldsa 65_ee_pub.pem corpus/valid/openssl/openssl_mldsa 87_ee_pub.pem corpus/valid/openssl/openssl_mlkem 1024_ee_pub.pem corpus/valid/openssl/openssl_mlkem 512_ee_pub.pem corpus/valid/openssl/openssl_mlkem 768_ee_pub.pem corpus/valid/openssl/openssl_mldsa 44_ee_cert.pem corpus/valid/openssl/openssl_mldsa 65_ca_cert.pem

openssl-mlkem1024-ee-p ub openssl-mlkem512-ee-p ub openssl-mlkem768-ee-p ub openssl-mldsa44-ee-cer t openssl-mldsa65-ca-cer t

Type

Continued on next page

Table 17: Valid artifacts in the frozen controlled corpus. (continued) Artifact ID

Type

Parameter set

Surface

Path

openssl-mldsa65-ee-cer t openssl-mldsa87-ee-cer t openssl-mlkem1024-ee-c ert openssl-mlkem512-ee-c ert openssl-mlkem768-ee-c ert openssl-mldsa44-ee-key

certificate

ML-DSA-65

cert/profile

certificate

ML-DSA-87

cert/profile

certificate

ML-KEM-1024

cert/profile

certificate

ML-KEM-512

cert/profile

certificate

ML-KEM-768

cert/profile

private-keycontainer private-keycontainer private-keycontainer private-keycontainer private-keycontainer private-keycontainer private-keycontainer

ML-DSA-44

priv/import

ML-DSA-65

priv/import

ML-DSA-65

priv/import

ML-DSA-87

priv/import

ML-KEM-1024

priv/import

ML-KEM-512

priv/import

ML-KEM-768

priv/import

corpus/valid/openssl/openssl_mldsa 65_ee_cert.pem corpus/valid/openssl/openssl_mldsa 87_ee_cert.pem corpus/valid/openssl/openssl_mlkem 1024_ee_cert.pem corpus/valid/openssl/openssl_mlkem 512_ee_cert.pem corpus/valid/openssl/openssl_mlkem 768_ee_cert.pem corpus/valid/openssl/openssl_mldsa 44_ee_key.pem corpus/valid/openssl/openssl_mldsa 65_ca_key.pem corpus/valid/openssl/openssl_mldsa 65_ee_key.pem corpus/valid/openssl/openssl_mldsa 87_ee_key.pem corpus/valid/openssl/openssl_mlkem 1024_ee_key.pem corpus/valid/openssl/openssl_mlkem 512_ee_key.pem corpus/valid/openssl/openssl_mlkem 768_ee_key.pem

openssl-mldsa65-ca-key openssl-mldsa65-ee-key openssl-mldsa87-ee-key openssl-mlkem1024-ee-k ey openssl-mlkem512-ee-k ey openssl-mlkem768-ee-k ey

Invalid mutation families The invalid side of the corpus is organized first by fault family and then by artifact-level mutation. Table 18: Mutation families exercised by the 27 invalid controlled artifacts. Fault family

Invalid artifacts

Representative mutation tokens

encoding/container

size/shape

aid-parameters-null, aid-p 3 arameters-present-non-null, signature-aid-parameters-n ull 6 spki-public-key-truncate, private-key-seed-length-s hort, private-key-expanded-lengt h-short

inter-fieldconsistency

profile/usage-policy

field-domain

algorithm-policy

import-validation

spki-oid-length-mismatch, private-key-both-seed-exp anded-mismatch, aid-oid-family-swap keyusage-empty, keyusage-mis sing-key-encipherment, keyusage-extra-prohibite d-bit mlkem-unreduced-byteencod e12-value hashml-dsa-signature-oid-i n-pkix-cert, hashml-dsa-pkix-context mlkem-expanded-key-hash-m ismatch

Expected-detection map

Covered requirements

Requirement IDs

MLKEM-SPKI-AID-PARAMS-ABSENT, MLDSA-SPKI-AID-PARAMS-ABSENT, MLDSA-CERT-SIGNATURE-AID-PARAMS-ABSENT MLKEM-SPKI-PUBLIC-KEY-LENGTH, MLKEM-PRIVATE-SEED-LENGTH, MLKEM-PRIVATE-EXPANDED-LENGTH, MLDSA-SPKI-PUBLIC-KEY-LENGTH, MLDSA-PRIVATE-SEED-LENGTH, MLDSA-PRIVATE-EXPANDED-LENGTH MLKEM-PRIVATE-BOTH-CONSISTENCY, MLDSA-PRIVATE-BOTH-CONSISTENCY

MLKEM-CERT-KU-KEYENCIPHERMENT-ONLY, MLDSA-CERT-KU-AT-LEAST-ONE-SIGNING-BIT, MLDSA-CERT-KU-NO-ENCIPHERMENT-OR-AGREEMENT

MLKEM-SPKI-ENCODE-DECODE-IDENTITY

MLDSA-PKIX-HASHML-FORBIDDEN

MLKEM-PRIVATE-EXPANDED-HASH-CHECK

Each invalid artifact has a declared expected-detection set in the manifest before the evaluator is run. The map below therefore records both what failed and what the artifact was expected to fail for. The only strict/deployable action split in the current corpus is the unreduced ML-KEM ByteEncode12 mutation, which remains detected in both modes while becoming a warning in deployable. Table 19: Expected-detection ledger for all invalid controlled artifacts. Artifact ID

Surface

Mutation token(s)

der-mut-mldsa44-spk i-oid-swapped-to-mld sa65-pub der-mut-mldsa65-spk i-aid-null-pub der-mut-mldsa65-spk i-aid-octet-params-p ub der-mut-mldsa87-spk i-payload-2602-pub

SPKI

der-mut-mldsa65-spk i-oid-swapped-to-mlk em768-pub der-mut-mlkem512-spk i-oid-swapped-to-mlk em768-pub der-mut-mlkem768-cer t-spki-aid-null der-mut-mlkem768-cer t-spki-aid-octet-par ams der-mut-mlkem768-cer t-spki-payload-trunc ated der-mut-mlkem768-spk i-aid-null-pub der-mut-mlkem768-spk i-aid-octet-params-p ub der-mut-mlkem768-spk i-payload-truncated-p ub der-mut-mlkem768-spk i-unreduced-byteencod e12-pub der-mut-mldsa44-cer t-signature-aid-null der-mut-mldsa44-cer t-signature-aid-octet -params der-mut-mldsa44-cer t-signature-hashmldsa 44 der-mut-mldsa65-cer t-keyusage-empty openssl-mut-mldsa65-k eyusage-key-encipherm ent-cert

SPKI

Strict

Deployable

spki-oid-length-mismatch MLDSA-SPKI-PUBLIC-KEY -LENGTH

block

SPKI

aid-parameters-null

block

SPKI

aid-parameters-presentnon-null

MLDSA-SPKI-AID-PARAM S-ABSENT MLDSA-SPKI-AID-PARAM S-ABSENT

block

SPKI

spki-public-key-extend, MLDSA-SPKI-PUBLIC-KEY rfc9881-appendix-size-LENGTH transcription-2602 aid-oid-family-swap, MLKEM-SPKI-PUBLIC-KEY spki-oid-length-mismatch -LENGTH

block

SPKI

spki-oid-length-mismatch MLKEM-SPKI-PUBLIC-KEY -LENGTH

block

SPKI

aid-parameters-null

block

SPKI

aid-parameters-presentnon-null

MLKEM-SPKI-AID-PARAM S-ABSENT MLKEM-SPKI-AID-PARAM S-ABSENT

block

SPKI

spki-public-key-truncate

MLKEM-SPKI-PUBLIC-KEY -LENGTH

block

SPKI

aid-parameters-null

block

SPKI

aid-parameters-presentnon-null

MLKEM-SPKI-AID-PARAM S-ABSENT MLKEM-SPKI-AID-PARAM S-ABSENT

block

SPKI

spki-public-key-truncate

MLKEM-SPKI-PUBLIC-KEY -LENGTH

block

SPKI

mlkem-unreducedbyteencode12-value

MLKEM-SPKI-ENCODE-DEC ODE-IDENTITY

block

warn

cert/profile

signature-aid-parameters- MLDSA-CERT-SIGNATURE-A null ID-PARAMS-ABSENT signature-aid-parameters- MLDSA-CERT-SIGNATURE-A present-non-null ID-PARAMS-ABSENT

block

der-mut-mlkem768-cer t-keyusage-empty openssl-mut-mlkem76 8-keyusage-digital-s ignature-cert

cert/profile

cert/profile cert/profile

cert/profile

der-mut-mldsa44-key-b priv/import oth-mismatch der-mut-mldsa44-key-e priv/import xpanded-short

Expected requirement(s)

hashml-dsa-signature-oid- MLDSA-PKIX-HASHML-FOR block block in-pkix-cert, BIDDEN hashml-dsa-pkix-context keyusage-empty MLDSA-CERT-KU-AT-LEAST block block -ONE-SIGNING-BIT keyusage-missingMLDSA-CERT-KU-AT-LEAST-ONE-SIGNING-BIT, block block signature-bit, MLDSA-CERT-KU-NO-ENCIPHERMENT-OR-AGREEMENT keyusage-keyencipherment keyusage-empty MLKEM-CERT-KU-KEYENCI block block PHERMENT-ONLY keyusage-missing-keyMLKEM-CERT-KU-KEYENCI block block encipherment, PHERMENT-ONLY keyusage-extraprohibited-bit private-key-both-seedMLDSA-PRIVATE-BOTH-CON block block expanded-mismatch SISTENCY private-key-expandedMLDSA-PRIVATE-EXPANDE block block length-short D-LENGTH Continued on next page

Table 19: Expected-detection ledger for all invalid controlled artifacts. (continued) Artifact ID

Surface

Mutation token(s)

Expected requirement(s)

der-mut-mldsa44-key-s eed-short der-mut-mlkem512-key -both-mismatch der-mut-mlkem512-key -expanded-short der-mut-mlkem512-key -hash-mismatch der-mut-mlkem512-key -seed-short

priv/import

private-key-seed-lengthshort private-key-both-seedexpanded-mismatch private-key-expandedlength-short mlkem-expanded-keyhash-mismatch private-key-seed-lengthshort

MLDSA-PRIVATE-SEED-LEN block block GTH MLKEM-PRIVATE-BOTH-CON block block SISTENCY MLKEM-PRIVATE-EXPANDE block block D-LENGTH MLKEM-PRIVATE-EXPANDED-HASH-CHECK, block block MLKEM-PRIVATE-BOTH-CONSISTENCY MLKEM-PRIVATE-SEED-LEN block block GTH

priv/import priv/import priv/import priv/import

Strict

Deployable

Detailed Baseline Comparison Tables

The baseline comparison is certificate-only because the frozen JZLint CLI baseline does not natively cover raw SPKI artifacts or private-key containers. Within that fair slice, the baseline remains useful as it catches some defects, misses others, and exhibits fatal fragility on some otherwise valid ML-KEM certificates [4]. Per-artifact outcomes Table 20: Per-artifact certificate-level comparison between the frozen baseline and the local extended artifact. Artifact ID

Validity

Expected requirement

Baseline

Extended Comparison class

invalid

error

same-detection

error

same-detection

pass

error

extended-recovers-baseline-miss

pass

error

extended-recovers-baseline-miss

error

extended-recovers-baseline-miss

der-mut-mlkem768-cert-key usage-empty der-mut-mlkem768-cert-spk i-aid-null der-mut-mlkem768-cert-spk i-aid-octet-params der-mut-mlkem768-cert-spk i-payload-truncated openssl-mut-mlkem768-keyus age-digital-signature-cert openssl-mldsa44-ee-cert openssl-mldsa65-ca-cert openssl-mldsa65-ee-cert openssl-mldsa87-ee-cert openssl-mlkem1024-ee-cert openssl-mlkem512-ee-cert openssl-mlkem768-ee-cert

invalid

MLDSA-CERT-SIGNATURE -AID-PARAMS-ABSENT MLDSA-CERT-SIGNATURE -AID-PARAMS-ABSENT MLDSA-PKIX-HASHML-FOR BIDDEN MLDSA-CERT-KU-AT-LEA ST-ONE-SIGNING-BIT MLDSA-CERT-KU-AT-LEA ST-ONE-SIGNING-BIT | MLDSA-CERT-KU-NO-ENC IPHERMENT-OR-AGREEME NT MLKEM-CERT-KU-KEYENCI PHERMENT-ONLY MLKEM-SPKI-AID-PARAM S-ABSENT MLKEM-SPKI-AID-PARAM S-ABSENT MLKEM-SPKI-PUBLIC-KEY -LENGTH MLKEM-CERT-KU-KEYENCI PHERMENT-ONLY – – – – – – –

fatal

error

fatal

error

pass pass pass pass fatal fatal fatal

pass pass pass pass pass pass pass

extended-recovers-baseline-mis s-and-runtime-fragility extended-matches-detection-witho ut-baseline-runtime-fragility extended-matches-detection-witho ut-baseline-runtime-fragility extended-recovers-baseline-mis s-and-runtime-fragility extended-matches-detection-witho ut-baseline-runtime-fragility same-pass same-pass same-pass same-pass baseline-runtime-fragile baseline-runtime-fragile baseline-runtime-fragile

invalid invalid invalid invalid

invalid invalid invalid invalid valid valid valid valid valid valid valid

Requirement-level comparison

The requirement-level view is often more revealing than the artifact-level view because it separates “baseline missed the expected defect” from “baseline never had a fair path to the covered artifact type.” Only the ten certificate requirements relevant to the baseline slice appear here. Table 21: Requirement-level comparison for the certificate-only baseline slice. Requirement ID

Stage

Expected

Baseline met

Blocked by fatal

Baseline status

Extended met

MLDSA-CERT-KU-AT-LEAST-ONE-SIG NING-BIT MLDSA-CERT-KU-NO-ENCIPHERMENT-O R-AGREEMENT MLDSA-CERT-SIGNATURE-AID-PARAM S-ABSENT MLDSA-PKIX-HASHML-FORBIDDEN MLDSA-SPKI-AID-PARAMS-ABSENT MLDSA-SPKI-PUBLIC-KEY-LENGTH MLKEM-CERT-KU-KEYENCIPHERMENT-O NLY MLKEM-SPKI-AID-PARAMS-ABSENT MLKEM-SPKI-ENCODE-DECODE-IDENT ITY MLKEM-SPKI-PUBLIC-KEY-LENGTH

cert/profile

incomplete

cert/profile

covered-forprohibited-bits partial

cert/profile SPKI SPKI cert/profile

1 0 0 2

0 0 0 1

0 0 0 0

gap partial gap-or-unverified incomplete

1 0 0 2

SPKI SPKI

2 0

0 0

2 0

SPKI

partial covered-by-externallint-path covered-forencoded-key

Runtime fragility notes Fatal baseline behavior matters even when the baseline eventually “rejects” an invalid artifact, because the rejection can happen for the wrong reason and can also spill onto valid artifacts. The table below records the fatal cases inside the controlled certificate slice. Table 22: Fatal baseline cases in the controlled certificate comparison. Artifact ID

Validity

Fatal baseline lints

Comparison class

der-mut-mlkem768-cert-key usage-empty

invalid

der-mut-mlkem768-cert-spk i-payload-truncated

invalid

openssl-mlkem1024-ee-cert

valid

openssl-mlkem512-ee-cert

valid

openssl-mlkem768-ee-cert

valid

e_ml_kem_ek_encodi ng; e_ml_kem_ek_length e_ml_kem_ek_encodi ng; e_ml_kem_ek_length e_ml_kem_ek_encodi ng; e_ml_kem_ek_length e_ml_kem_ek_encodi ng; e_ml_kem_ek_length e_ml_kem_ek_encodi ng; e_ml_kem_ek_length

extended-recovers-basel invalid certificate blocked by fatal ine-miss-and-runtime-f baseline behavior before the expected ragility requirement could be credited extended-recovers-basel invalid certificate blocked by fatal ine-miss-and-runtime-f baseline behavior before the expected ragility requirement could be credited baseline-runtime-fragi valid certificate rejected by baseline le with fatal ML-KEM encoded-key/runtime lints baseline-runtime-fragi valid certificate rejected by baseline le with fatal ML-KEM encoded-key/runtime lints baseline-runtime-fragi valid certificate rejected by baseline le with fatal ML-KEM encoded-key/runtime lints

Why the case matters

Public Appendix Ledger

The public appendix spans 26 valid public artifacts across two providers, a certificate slice, and privatekey containers covering all six ML-KEM/ML-DSA parameter sets. Provider inventories

certificate

private-key container

ossl35 0

10 12 artifact count

Figure 13: Public appendix coverage by provider and artifact type. Table 23: Provider inventory for the bounded public appendix. Provider

Artifacts

Certificates

Private-key containers

Algorithms

Parameter sets

bc ossl35

8 18

2 6

6 12

ML-DSA, ML-KEM ML-DSA, ML-KEM

ML-DSA-65, ML-KEM-768 ML-DSA-44, ML-DSA-65, ML-DSA-87, ML-KEM-1024, ML-KEM-512, ML-KEM-768

Parameter-set coverage Table 24: Parameter-set coverage. Parameter set

Certificate providers

Private-key providers

Covered stages

ML-DSA-44 ML-DSA-65 ML-DSA-87 ML-KEM-1024 ML-KEM-512 ML-KEM-768

ossl35 bc, ossl35 ossl35 ossl35 ossl35 bc, ossl35

ossl35 bc ossl35 ossl35 ossl35 bc

cert/profile, priv/import cert/profile, priv/import cert/profile, priv/import cert/profile, priv/import cert/profile, priv/import cert/profile, priv/import

For the certificate subset of the public appendix, the frozen baseline still fatally rejects four valid ML-KEM certificates while the local artifact passes all eight appendix certificates without findings. Certificate slice Table 25: Certificate slice of the bounded public appendix. Artifact ID

Provider

Parameter set

Surface

Selection rationale

appendix-bc-mldsa65-ta-cert

ML-DSA-65

cert/profile

appendix-bc-mlkem768-ee-cert

ML-KEM-768

cert/profile

appendix-ossl35-mldsa44-ta-c ert appendix-ossl35-mldsa65-ta-c ert

ossl35

ML-DSA-44

cert/profile

ossl35

ML-DSA-65

cert/profile

cross-provider pure ML-DSA certificate matching the private-key container variants selected for import-validation cross-provider pure ML-KEM certificate matching the private-key container variants selected for import-validation final-R5 pure ML-DSA trust anchor from a widely used public implementation final-R5 pure ML-DSA trust anchor from a widely used public implementation Continued on next page

Table 25: Certificate slice of the bounded public appendix. (continued) Artifact ID

Provider

Parameter set

Surface

Selection rationale

appendix-ossl35-mldsa87-ta-c ert appendix-ossl35-mlkem1024-e e-cert appendix-ossl35-mlkem512-e e-cert appendix-ossl35-mlkem768-e e-cert

ossl35

ML-DSA-87

cert/profile

ossl35

ML-KEM-1024

cert/profile

ossl35

ML-KEM-512

cert/profile

ossl35

ML-KEM-768

cert/profile

final-R5 pure ML-DSA trust anchor from a widely used public implementation final-R5 pure ML-KEM end-entity certificate covering the highest NIST parameter set final-R5 pure ML-KEM end-entity certificate covering the lowest NIST parameter set final-R5 pure ML-KEM end-entity certificate covering the practical default security level

Private-key slice Table 26: Private-key-container slice. Artifact ID

Provider

Parameter set

Surface

Selection rationale

appendix-bc-mldsa65-both-k ey appendix-bc-mldsa65-expande d-key appendix-bc-mldsa65-seed-k ey appendix-bc-mlkem768-both-k ey

ML-DSA-65

priv/import

ML-DSA-65

priv/import

ML-DSA-65

priv/import

ML-KEM-768

priv/import

appendix-bc-mlkem768-expan ded-key

ML-KEM-768

priv/import

appendix-bc-mlkem768-seed-k ey appendix-ossl35-mldsa44-bot h-key

ML-KEM-768

priv/import

ossl35

ML-DSA-44

priv/import

appendix-ossl35-mldsa44-exp anded-key

ossl35

ML-DSA-44

priv/import

appendix-ossl35-mldsa44-see d-key

ossl35

ML-DSA-44

priv/import

appendix-ossl35-mldsa87-bot h-key

ossl35

ML-DSA-87

priv/import

appendix-ossl35-mldsa87-exp anded-key

ossl35

ML-DSA-87

priv/import

appendix-ossl35-mldsa87-see d-key

ossl35

ML-DSA-87

priv/import

appendix-ossl35-mlkem1024-b oth-key

ossl35

ML-KEM-1024

priv/import

appendix-ossl35-mlkem1024-e xpanded-key

ossl35

ML-KEM-1024

priv/import

appendix-ossl35-mlkem1024-s eed-key

ossl35

ML-KEM-1024

priv/import

appendix-ossl35-mlkem512-b oth-key

ossl35

ML-KEM-512

priv/import

appendix-ossl35-mlkem512-e xpanded-key

ossl35

ML-KEM-512

priv/import

appendix-ossl35-mlkem512-s eed-key

ossl35

ML-KEM-512

priv/import

cross-provider both-form ML-DSA private key exercising seed-expanded consistency parsing cross-provider expanded-key ML-DSA private key for import-format external validity cross-provider seed-only ML-DSA private key for import-format external validity cross-provider both-form ML-KEM private key exercising seed-expanded consistency and hash-check parsing cross-provider expanded-key ML-KEM private key exercising hash-check parsing on non-OpenSSL material cross-provider seed-only ML-KEM private key for import-format external validity low-parameter pure ML-DSA both-form private key from ossl35 to cover seed-expanded consistency parsing low-parameter pure ML-DSA expanded-key private key from ossl35 to complement seed-only import coverage low-parameter pure ML-DSA seed-only private key from ossl35 to cover importer behavior at the low end high-parameter pure ML-DSA both-form private key from ossl35 to pair consistency checks with the highest parameter set high-parameter pure ML-DSA expanded-key private key from ossl35 to close representation coverage at the high end high-parameter pure ML-DSA seed-only private key from ossl35 to show importer coverage at the high end high-parameter pure ML-KEM both-form private key from ossl35 to combine consistency and hash-check coverage at the high end high-parameter pure ML-KEM expanded-key private key from ossl35 to extend hash-check and sizing coverage to the high end high-parameter pure ML-KEM seed-only private key from ossl35 to complete parameter-set coverage for importer behavior low-parameter pure ML-KEM both-form private key from ossl35 to cover seed-expanded consistency at the low end low-parameter pure ML-KEM expanded-key private key from ossl35 to exercise hash-check parsing outside the default set low-parameter pure ML-KEM seed-only private key from ossl35 to widen importer coverage beyond the mid-level parameter set

Cross-Tool Full Matrix

The cross-tool layer shows a practical separation that matters to operators: parse acceptance is not the same thing as policy conformance. The matrix below keeps that evidence visible: Behavior taxonomy Table 27: Behavior codes used in the cross-tool matrix. Code

Meaning

A RS RP RF NA

artifact accepted by the named tool in the exercised path artifact rejected for a structural or encoding reason artifact rejected for a profile or semantic-policy reason tool failed or raised a fatal runtime condition on the artifact tool path not applicable for the artifact type or unsupported in the frozen scope

Controlled set The controlled set contains 31 artifacts in the cross-tool layer: 17 certificates and 14 private-key containers. Raw SPKI artifacts are omitted from this appendix matrix because the external tools exercised here do not offer a fairly comparable frozen path for them. Table 28: Cross-tool behavior matrix for the controlled set. Artifact ID

Surface

Validity

Local

JZLint

OpenSSL

pkilint

der-mut-mldsa44-cert-signature-aid-null der-mut-mldsa44-cert-signature-aid-octet -params der-mut-mldsa44-cert-signature-hashmldsa 44 der-mut-mldsa65-cert-keyusage-empty der-mut-mlkem768-cert-keyusage-empty der-mut-mlkem768-cert-spki-aid-null der-mut-mlkem768-cert-spki-aid-octet-p arams der-mut-mlkem768-cert-spki-payload-trunc ated openssl-mldsa44-ee-cert openssl-mldsa65-ca-cert openssl-mldsa65-ee-cert openssl-mldsa87-ee-cert openssl-mlkem1024-ee-cert openssl-mlkem512-ee-cert openssl-mlkem768-ee-cert openssl-mut-mldsa65-keyusage-key-enciphe rment-cert openssl-mut-mlkem768-keyusage-digital-s ignature-cert der-mut-mldsa44-key-both-mismatch der-mut-mldsa44-key-expanded-short der-mut-mldsa44-key-seed-short der-mut-mlkem512-key-both-mismatch der-mut-mlkem512-key-expanded-short der-mut-mlkem512-key-hash-mismatch der-mut-mlkem512-key-seed-short openssl-mldsa44-ee-key openssl-mldsa65-ca-key openssl-mldsa65-ee-key openssl-mldsa87-ee-key openssl-mlkem1024-ee-key openssl-mlkem512-ee-key openssl-mlkem768-ee-key

cert/profile cert/profile

invalid invalid

RS RS

A A

RF RF

cert/profile

invalid

cert/profile cert/profile SPKI SPKI

invalid invalid invalid invalid

RP RP RS RS

A RF RS RS

A A A A

RF RF RF RF

SPKI

invalid

cert/profile cert/profile cert/profile cert/profile cert/profile cert/profile cert/profile cert/profile

valid valid valid valid valid valid valid invalid

A A A A A A A RP

A A A A RF RF RF RP

A A A A A A A A

RF RF RF RF RF RF RF RF

cert/profile

invalid

priv/import priv/import priv/import priv/import priv/import priv/import priv/import priv/import priv/import priv/import priv/import priv/import priv/import priv/import

invalid invalid invalid invalid invalid invalid invalid valid valid valid valid valid valid valid

RP RS RS RP RS RP RS A A A A A A A

NA NA NA NA NA NA NA NA NA NA NA NA NA NA

RS RS RS RS RS RS RS A A A A A A A

NA NA NA NA NA NA NA NA NA NA NA NA NA NA

Appendix set The appendix set contains 26 valid public artifacts. It is particularly useful for exposing baseline runtime fragility on otherwise valid ML-KEM certificates and for showing that parse-only acceptance by OpenSSL does not, by itself, establish profile conformance. Table 29: Cross-tool behavior matrix for the bounded public appendix. Artifact ID

Surface

Validity

Local

JZLint

OpenSSL

pkilint

appendix-bc-mldsa65-ta-cert appendix-bc-mlkem768-ee-cert appendix-ossl35-mldsa44-ta-cert appendix-ossl35-mldsa65-ta-cert appendix-ossl35-mldsa87-ta-cert appendix-ossl35-mlkem1024-ee-cert appendix-ossl35-mlkem512-ee-cert appendix-ossl35-mlkem768-ee-cert appendix-bc-mldsa65-both-key appendix-bc-mldsa65-expanded-key appendix-bc-mldsa65-seed-key appendix-bc-mlkem768-both-key appendix-bc-mlkem768-expanded-key appendix-bc-mlkem768-seed-key appendix-ossl35-mldsa44-both-key appendix-ossl35-mldsa44-expanded-key appendix-ossl35-mldsa44-seed-key appendix-ossl35-mldsa87-both-key appendix-ossl35-mldsa87-expanded-key appendix-ossl35-mldsa87-seed-key appendix-ossl35-mlkem1024-both-key appendix-ossl35-mlkem1024-expanded-key appendix-ossl35-mlkem1024-seed-key appendix-ossl35-mlkem512-both-key appendix-ossl35-mlkem512-expanded-key appendix-ossl35-mlkem512-seed-key

cert/profile cert/profile cert/profile cert/profile cert/profile cert/profile cert/profile cert/profile priv/import priv/import priv/import priv/import priv/import priv/import priv/import priv/import priv/import priv/import priv/import priv/import priv/import priv/import priv/import priv/import priv/import priv/import

valid valid valid valid valid valid valid valid valid valid valid valid valid valid valid valid valid valid valid valid valid valid valid valid valid valid

A A A A A A A A A A A A A A A A A A A A A A A A A A

A RF A A A RF RF RF NA NA NA NA NA NA NA NA NA NA NA NA NA NA NA NA NA NA

A A A A A A A A A A A A A A A A A A A A A A A A A A

RF RF RF RF RF RF RF RF NA NA NA NA NA NA NA NA NA NA NA NA NA NA NA NA NA NA

Reproduction and Release Manifest

The artifact is designed to be rerun. This appendix records the canonical replay path, the frozen toolchain summary, the reference hashes, the release tiers, and the reviewer-first reading order. The underlying import substrate and baseline remain frozen local snapshots [4, 1]. Canonical replay log Table 30: Canonical replay sequence distilled from experiments/replay_freeze.sh. Step

Command or script

Purpose

STEP-01 STEP-02 STEP-03

./experiments/check_environment.sh ./experiments/prepare_third_party.sh ./experiments/build_libcrux_import_che ck.sh ./experiments/generate_corpus_openssl. sh ./experiments/generate_mutations_opens sl.sh ./experiments/generate_der_mutations.s h ./experiments/run_extended.sh--modestr ict ./experiments/run_extended.sh--modedep loyable ./experiments/run_coverage.sh--modestr ict/deployable

capture toolchain state and write environment.txt prepare frozen third-party snapshots needed for baseline replay build narrow import-validation bridge used by the importer slice

STEP-04 STEP-05 STEP-06 STEP-07 STEP-08 STEP-09

regenerate valid local corpus artifacts regenerate OpenSSL-driven certificate mutations regenerate DER-level mutations for SPKI and private keys produce strict registry results produce deployable registry results produce certificate and SPKI coverage summaries in both modes Continued on next page

Table 30: Canonical replay sequence distilled from experiments/replay_freeze.sh. (continued) Step

Command or script

Purpose

STEP-10

./experiments/run_private_key_coverage .sh--modestrict/deployable ./experiments/run_baseline.sh

produce importer/private-key coverage summaries in both modes

STEP-11 STEP-12 STEP-13 STEP-14

STEP-15 STEP-16

STEP-17

./experiments/run_baseline_compare.sh ./experiments/run_real_world_appendix. sh ./experiments/run_reference_workflow.s h, ./experiments/run_operator_gate_pack s.sh ./experiments/run_cross_tool_behavior. sh ./experiments/run_claim_lock.sh, ./experiments/run_visual_plan.sh, ./experiments/run_positioning_lock.sh ./experiments/run_artifact_packaging.s h, ./experiments/run_upgrade_decision.sh, ./experiments/run_smoke_tests.sh

replay certificate-level JZLint baseline; baseline_exit_code=1 is frozen as expected upstream fragility materialize certificate-level baseline-versus-extended comparison materialize the bounded public appendix and its summary outputs materialize owner/stage workflow and gate-pack outputs

materialize the secondary parse-vs-policy behavior matrix lock claim, visual, and positioning scaffolding

package the artifact, freeze the upgrade decision, and run smoke tests

Environment and hashes Table 31: Toolchain summary captured in results/environment.txt. Component

Frozen value

Java Maven Rust Python OpenSSL Environment status

openjdk version "17.0.18" 2026-01-20 Apache Maven 3.9.14 (996c630dbc656c76214ce58821dcc58be960875b) rustc 1.82.0 (f6e511eec 2024-10-15); cargo 1.82.0 (8f40fc59f 2024-08-21) Python 3.14.3 OpenSSL 3.6.1 27 Jan 2026 (Library: OpenSSL 3.6.1 27 Jan 2026) ok

Table 32: Frozen reference artifacts. Hash prefix

Reference path

Note

a4852298eebc. . . fe1f12f32a7e. . . 57239b9f84c0. . . 4b586ec732b2. . . 977e6fb42ecd. . . 4206e03ad6ff. . .

../reference/2025-1241.pdf ../reference/NIST.FIPS.203.pdf ../reference/NIST.FIPS.204.pdf ../reference/rfc9881.pdf ../reference/rfc9935.pdf ../reference/github/jzlint-main.zip

764f83e3bd00. . .

../reference/github/libcrux-main.zip

Public Key Linting for ML-KEM and ML-DSA FIPS 203 FIPS 204 RFC 9881 RFC 9935 JZLint snapshot, internal commit d6fdf02ad31f085e88d252b368f50e9da87debfd libcrux snapshot, internal commit 6b9eca5a7b507e1d8423f85e5711572b4a661e8d

Record · ID 120448 · SHA-256 813e799bb4fba677
Retrieved via Conceptio — every document is proof-bundled with source, license, and retrieval metadata.