code wiki / _hdl_build / nx_quic_handshake_sm_test.nx
`nx_quic_handshake_sm_test.nx` source

1// nx_quic_handshake_sm_test.nx -- RUNG 6d gate: TLS 1.3 / QUIC handshake state machine (RFC 8446 App A)
2// + Finished-MAC (RFC 8446 sec 4.4.4). Drives the valid client flight, rejects out-of-order messages, and
3// proves the Finished MAC binds the transcript (different transcript -> different verify_data). Native,
4// sovereign, on our own HKDF+HMAC. license_tier: ORIGINAL
5import "nx_quic_handshake_sm.nx"
6import "nx_g_pn_lite_lib.nx"
7import "nx_g_check_lib.nx"
8import "nx_g_puts_lib.nx"
9
10func main() -> i64 {
11    g_puts("nx_quic_handshake_sm gate -- TLS 1.3 handshake state machine + Finished MAC (RFC 8446)\n" as *u8)
12    var pass: i64=0; var total: i64=0
13
14    // ---- valid client flight: WAIT_SH ->SH-> EE -> Cert -> CertVerify -> Finished -> CONNECTED ----
15    var s: i64 = HS_WAIT_SH
16    s = quic_hs_sm_step(s, 2)    // server_hello
17    s = quic_hs_sm_step(s, 8)    // encrypted_extensions
18    s = quic_hs_sm_step(s, 11)   // certificate
19    s = quic_hs_sm_step(s, 15)   // certificate_verify
20    s = quic_hs_sm_step(s, 20)   // finished
21    pass = pass + g_check("valid flight SH->EE->Cert->CV->Fin reaches HS_CONNECTED" as *u8, (s == HS_CONNECTED) as i64); total=total+1
22
23    // ---- out-of-order rejected ----
24    var bad1: i64 = quic_hs_sm_step(HS_WAIT_SH, 11)   // cert before server_hello
25    var bad2: i64 = quic_hs_sm_step(HS_WAIT_EE, 20)   // finished before cert chain
26    var bad_ok: i64=1
27    if bad1 != HS_ERROR { bad_ok=0 }
28    if bad2 != HS_ERROR { bad_ok=0 }
29    pass = pass + g_check("out-of-order handshake messages -> HS_ERROR (2 cases)" as *u8, bad_ok); total=total+1
30
31    // ---- Finished MAC: deterministic + binds the transcript ----
32    let base_key: *u8 = sys_mmap(32)
33    var i: i64=0; while i<32 { base_key[i]=((i*13+5)&255) as u8; i=i+1 }
34    let th1: *u8 = sys_mmap(32); i=0; while i<32 { th1[i]=((i*7+1)&255) as u8; i=i+1 }
35    let th2: *u8 = sys_mmap(32); i=0; while i<32 { th2[i]=((i*7+1)&255) as u8; i=i+1 } th2[0]=(th2[0] as i64 ^ 1) as u8  // 1 bit different
36    let vd1: *u8 = sys_mmap(32); quic_hs_finished_verify(base_key, th1, vd1)
37    let vd1b: *u8 = sys_mmap(32); quic_hs_finished_verify(base_key, th1, vd1b)
38    let vd2: *u8 = sys_mmap(32); quic_hs_finished_verify(base_key, th2, vd2)
39    pass = pass + g_check("Finished verify_data deterministic (same inputs -> identical)" as *u8, quic_hs_verify_eq(vd1, vd1b)); total=total+1
40    pass = pass + g_check("Finished MAC binds transcript (1-bit transcript change -> different verify_data)" as *u8, (quic_hs_verify_eq(vd1, vd2) == 0) as i64); total=total+1
41
42    // ---- finished_key derivation is deterministic + distinct from the base key ----
43    let fk1: *u8 = sys_mmap(32); quic_hs_finished_key(base_key, fk1)
44    let fk2: *u8 = sys_mmap(32); quic_hs_finished_key(base_key, fk2)
45    var fk_ok: i64=0
46    if quic_hs_verify_eq(fk1, fk2)==1 { if quic_hs_verify_eq(fk1, base_key)==0 { fk_ok=1 } }
47    pass = pass + g_check("finished_key = Expand-Label(base,'finished') deterministic + != base" as *u8, fk_ok); total=total+1
48
49    g_puts("---- quic_handshake_sm gate: passed " as *u8); g_pn(pass); g_puts(" / " as *u8); g_pn(total); g_puts(" ----\n" as *u8)
50    if pass == total { g_puts("VERDICT: GREEN (TLS 1.3 handshake state machine + Finished MAC, RFC 8446, sovereign)\n" as *u8); return 0 }
51    g_puts("VERDICT: RED\n" as *u8)
52    return 1
53}
nx_quic_handshake_sm_test.nx source

`nx_quic_handshake_sm_test.nx` source
