{"id":"58570f30-2ad6-4988-917b-ce1288984a92","arxiv_id":"2505.14162","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"VMuckle adapts the Muckle+ hybrid authenticated key exchange so a single run can use PSK, post-quantum signatures, or both, and uses this to give MACsec a quantum-safe root key.","lead":"This paper proposes a new hybrid key exchange protocol called VMuckle that combines classical, post-quantum, and quantum key material, and can authenticate with either pre-shared keys or post-quantum signatures. It slots this protocol into MACsec, the Ethernet layer-2 security standard, as a drop-in replacement for 802.1X authentication to protect LAN links against quantum computers.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The load-bearing reduction is delegated: VMuckle's modified key schedule changes the very games that Appendix C says follow from Muckle+, and the empty-PSK mode violates Theorem 1's uniform-PSK premise.","rationale":"The reader identified the same two fragile premises: the delegated proof cases and the uniform-PSK assumption. I agree that the delegated cases are the single load-bearing concern. VMuckle's modifications are not cosmetic; they change the key schedule by introducing k1 = F(kc, ℓ3||k0) and k2 = F(kq, ℓ4||k1). In the original Muckle+ flow, the classical and post-quantum shares are independent until combined later, whereas here the classical and QKD keys are interdependent with the post-quantum share. The reduction must handle adversaries who know some components while others remain secret, and the paper does not show those hybrids. This is a proof-writing gap, not evidence of a broken protocol; the construction is plausible and the high-level proof structure matches [18]. But the submitted artifact does not establish the central theorem. The empty-PSK issue is real but secondary: the protocol explicitly permits psk = '', and cleanVM's conditions 4 and 5 do not force psk to be non-empty or uniformly random, so the theorem's hypotheses do not cover the protocol's advertised mode. Since the missing proof work is substantial but the construction is plausible, I maintain CONDITIONAL, matching the reader's verdict. The condition is that a complete, self-contained case analysis and an explicit treatment of the empty/known-PSK mode be supplied.","tokens_in":23237,"tokens_out":3184,"duration_ms":65371,"concrete_test":"Complete the proof of Theorem 1 without citing [18]: (a) In Subcase 3.1, write the explicit sequence of hybrids replacing kpq, k0, k1, k2, k3, and M_S by independent random values, and verify each transition while the adversary may observe kc, kq, SecState, and both KEM ciphertexts; in particular, state which PRF justifies replacing k1 = F(kc, ℓ3||k0) when kc is known. (b) In Subcase 3.2, write the hybrids for k2 = F(kq, ℓ4||k1) when k1 is known to the adversary, confirming that the dual-PRF assumption is applied with kq as key and ℓ4||k1 as input. (c) Re-run the key-indistinguishability game with psk set to the empty string and DSS authentication enabled; check whether cleanVM still holds and whether the Case 1.1 PRF hop for fC/fS remains valid when psk is fixed and known.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"Theorem 1 is the central claim, and its proof is not self-contained at the critical points. Case 1.2 and Subcases 3.1-3.4 in Appendix C say 'the proof follows the proof of case X in [18]' without presenting the hybrids. But VMuckle is not Muckle+: the boxed modifications in Fig. 2 insert a classical KEM share kc, chain it through k1 = F(kc, ℓ3||k0), then chain QKD share kq through k2 = F(kq, ℓ4||k1), and finally add a PSK-MAC authentication track. Each insertion is a place where a game hop must be re-derived: e.g., when kpq is unknown but kc, kq, SecState, and all long-term keys may be known, the reduction must prove that k0 still hides the tested master secret; when kq is unknown and k1 is known, it must prove that k2 = F(kq, ℓ4||k1) is independent of k1 via a properly ordered dual-PRF argument. The paper also uses a modified cleanness predicate relative to [18], explicitly footnoting a different bound, making the delegation even less safe. Separately, the protocol text states psk may be empty or known, while Theorem 1 requires psk to be uniformly random; cleanVM conditions 4 and 5 do not exclude empty or known PSK from the no-CorruptSK branch, so an implementation allowing empty PSK would satisfy the predicate while falling outside the theorem's hypotheses.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes VMuckle, a hybrid authenticated key exchange (HAKE) protocol that combines a classical KEM, a post-quantum KEM, a QKD-supplied key, and authentication via either post-quantum digital signatures or a pre-shared key (or both). The protocol is designed as a drop-in replacement for the 802.1X authentication step in MACsec, feeding its output as the Master Session Key into the MKA key hierarchy without modifying the 802.1AE or 802.1X standards. The authors claim post-quantum HAKE security under a new cleanness predicate cleanVM (Theorem 1, Appendix C), with the proof largely delegated to the Muckle+ proof from [18] at several critical subcases. The paper also reports a Python/liboqs prototype and benchmarks comparing many KEM/signature combinations in terms of CPU cycles and bandwidth, and it compares VMuckle's handshake size with EAP-TLS.","tokens_in":23529,"tokens_out":5363,"duration_ms":58439,"significance":"If the security claim is established, VMuckle would be a valuable contribution: it is the first HAKE protocol to allow both PSK-based and signature-based authentication to be chosen flexibly while preserving a single proof framework, and the proposed MACsec integration is concrete and standards-compatible. The paper has several concrete strengths: the key schedule is explicitly specified with labeled PRF calls and a dual-PRF assumption; the protocol is instantiated with standardized NIST PQC algorithms; the prototype and benchmark tables provide useful engineering evidence; and the cleanness predicate is stated precisely enough to expose exactly which compromises are tolerated. The main unresolved issue is that the central proof, Theorem 1, is not self-contained at exactly the points where VMuckle deviates from Muckle+, and the protocol text permits an empty or known PSK mode that falls outside the theorem's uniform-random-PSK hypothesis.","major_comments":[{"comment":"The proof of Theorem 1 delegates the core reductions to [18] without presenting the game transitions, but VMuckle is not Muckle+. The boxed modifications in Fig. 2 insert a classical KEM share kc, chain it through k1 = F(kc, ℓ3||k0), then chain the QKD share kq through k2 = F(kq, ℓ4||k1), and add a PSK-MAC authentication track. Each of these insertions changes which keys are known in the adversary's view and therefore requires a re-derived hybrid argument. For example, in Subcase 3.2 (only the QKD key kq uncompromised), the adversary may know kc, k0, SecState, and all long-term keys; the reduction must prove that k2 = F(kq, ℓ4||k1) still hides the tested master secret even when k1 is known, which requires a carefully ordered dual-PRF argument that is not supplied. Likewise, Theorem 1 makes no security assumption on KEMc, so the proof must explicitly handle an adversarially known kc. Footnote 2 further states that a different cleanness predicate than [18] is used and that this gives a 'slightly tighter bound', yet no derivation is provided. Please present the missing hybrids or a formal reduction theorem with an explicit game sequence; a citation to [18] is not sufficient at these load-bearing points.","section":"Appendix C, Subcases 1.2 and 3.1–3.4"},{"comment":"The protocol specification explicitly permits an empty or known pre-shared key: Section III states 'psk may be an empty string' and 'If psk is an empty or known string, key confirmation can still be achieved via f kS'. Theorem 1, however, assumes 'psk ∈ S be a uniformly random pre-shared key'. The cleanness predicate cleanVM (Definition 11) does not exclude the empty-PSK case: condition 4 only requires that either no CorruptQK(i) or no CorruptSK(i) query was issued, and an empty PSK remains 'uncorrupted' in the sense that no CorruptSK was issued. In Subcase 1.1 (Appendix C), Game 4 replaces fC = F(psk, f kC) and fS = F(psk, f kS) with uniformly random values using a PRF challenger, justified by 'no CorruptSK queries have been issued'. If psk is empty, this replacement is invalid because F(empty, ·) is a deterministic function that the adversary can evaluate. Thus the theorem does not cover a mode that the protocol text explicitly supports. Please either restrict the proven configuration to a secret, randomly chosen PSK and state this restriction in the protocol specification, or extend the security analysis to the empty/known-PSK case by relying on the other authentication mechanism.","section":"Section III and Theorem 1"}],"minor_comments":[{"comment":"The subcase is titled 'No CorruptQK has been issued' but the text then says 'we assume that the signing key skI is not corrupted'. Please clarify explicitly that the post-quantum long-term key used for signatures is the key covered by CorruptQK, or introduce a separate corruption identifier for the signing key, to avoid ambiguity.","section":"Appendix C, Subcase 1.2"},{"comment":"The text 'the proof of case 3.3 in [18] 2' contains a stray superscript '2' that appears to be a leftover footnote marker; please remove it or attach the footnote text clearly.","section":"Appendix C, Subcase 3.3"},{"comment":"The table headers and footnotes are inconsistent: Table III uses '(1)' and '(2)' footnotes that are not all defined, 'Cycles (G)' is ambiguous (it is later referred to as giga cycles), and the table would benefit from stating which variants include the classical ECDH contribution and which include QKD-256 explicitly for every row group.","section":"Tables III and IV"},{"comment":"Definition 10 first states HAKE security for 'any PPT adversary A' and then defines post-quantum security by requiring the same for QPT adversaries; the text should be consistent about whether the base definition also allows QPT adversaries or whether the QPT version is the only one used in Theorem 1. Also, the final advantage bound sums subcases that use different reductions with the same symbol A; please make the standard composition argument explicit, since the per-subcase adversaries and their running times are not identical.","section":"Definition 10 and Appendix C final derivation"}],"recommendation":"major_revision","confidential_remarks":"The central design is promising and the application to MACsec is well motivated, but the proof as written delegates the exact parts where the protocol differs from Muckle+. Before this is publishable as a security claim, the authors should provide a complete proof or an explicit reduction with all game hops, and they should align the protocol's permitted PSK modes with the theorem's hypotheses. The benchmark and integration material is a strength and should be preserved. I would encourage the editor to request a revised version with the full proof or a clearly marked extended-full-proof appendix."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The paper is worth reading and refereeing, but the main theorem is not self-contained where it matters. What's genuinely new: a single HAKE run can authenticate with a PSK, a post-quantum signature, or both, and an optional classical KEM is added to the key schedule. The MACsec integration uses VMuckle to produce the MKA root key without changing 802.1AE or 802.1X. That is a real practical contribution for LAN infrastructure, and the protocol description plus the benchmark tables are solid.\n\nThe soft spot is the proof. Appendix C delegates Subcase 1.2 and Subcases 3.1-3.4 to Muckle+ without presenting the game hops. That delegation is too quick, because VMuckle's modifications - the classical KEM share kc, the k1/k2 chain, the PSK-MAC track - are precisely the places where a game hop must be re-derived. The paper also changes the cleanness predicate and even footnotes a different bound, which makes the delegation less safe. A referee should ask for a full proof or at least a precise lemma showing why each modified game transition preserves the Muckle+ argument.\n\nThere is also a mismatch between the protocol spec and Theorem 1. The text says psk may be empty or known; the theorem requires psk uniformly random. The cleanness predicate cleanVM does not rule out the empty-PSK branch, so an implementation could satisfy the predicate while falling outside the theorem's hypotheses. That should be fixed by either forbidding the empty-PSK mode in the protocol or expanding the theorem.\n\nThe prototype and benchmarks are fine, but no code is released and the measurement methodology is thin. That is minor compared with the proof gaps. The citation pattern is honest; the dependency on [18] is explicit, and the overlap in authorship does not by itself create a problem since [18] is peer-reviewed.\n\nWho is this for: anybody working on quantum-safe key exchange for layer 2, and anyone wanting a concrete example of HAKE-to-MACsec mapping. The central idea is sound and the application is sensible. I'd send it to peer review rather than desk reject, but with a clear request: complete the delegated proof cases, and reconcile the PSK assumption with the protocol text.","headline":"VMuckle is a genuinely useful HAKE variant and MACsec integration, but the security proof delegates the cases that the protocol actually changes, and the empty-PSK mode is outside Theorem 1.","tokens_in":24100,"tokens_out":3949,"would_cite":true,"duration_ms":33173,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":null,"created_at":"2026-08-07T15:40:17.970810+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":null,"supporting_citations":[],"review_version":1}