nx_tls13_schedule.nx source

1// nx_tls13_schedule.nx -- TLS 1.3 key schedule cascade (RFC 8446 §7.1). 2// 3// Phase 0b §D of the Nishi TLS 1.3 stack per 4// docs/NISHI_TLS13_GAP_AUDIT.md. Composes the just-landed 5// nx_hkdf + nx_tls13_kdf into the named 5-stage cascade that 6// produces every secret a TLS 1.3 session needs. 7// 8// The cascade (no-PSK case, which is the 99%-common one): 9// 10// 0 11// | 12// v 13// HKDF-Extract(salt=0^Hash, IKM=0^Hash) = early_secret 14// | 15// v 16// Derive-Secret(., "derived", "") = derived_1 (salt for next HKDF-Extract) 17// | 18// v ECDHE shared 19// HKDF-Extract(salt=derived_1, IKM=ECDHE) = handshake_secret 20// | 21// +--> Derive-Secret(., "c hs traffic", H1) = client_hs_traffic_secret 22// +--> Derive-Secret(., "s hs traffic", H1) = server_hs_traffic_secret 23// v 24// Derive-Secret(., "derived", "") = derived_2 (salt for next HKDF-Extract) 25// | 26// v 27// HKDF-Extract(salt=derived_2, IKM=0^Hash) = master_secret 28// | 29// +--> Derive-Secret(., "c ap traffic", H2) = client_app_traffic_secret_0 30// +--> Derive-Secret(., "s ap traffic", H2) = server_app_traffic_secret_0 31// +--> Derive-Secret(., "exp master", H2) = exporter_master_secret 32// +--> Derive-Secret(., "res master", H3) = resumption_master_secret 33// 34// Then per-traffic-secret AEAD key + IV derivation: 35// 36// key = HKDF-Expand-Label(traffic_secret, "key", "", key_length) 37// iv = HKDF-Expand-Label(traffic_secret, "iv", "", iv_length) 38// finished_key = HKDF-Expand-Label(traffic_secret, "finished", "", Hash.length) 39// 40// All transcript hashes (H1, H2, H3) are caller-supplied because 41// they depend on which handshake messages have been seen so far -- 42// Gap E (transcript hash) ships separately. 43// 44// What it does today: 45// - early_secret, derived_1, handshake_secret, derived_2, master_secret 46// -- the cascade BACKBONE (the secrets that flow from one 47// HKDF-Extract to the next; no transcript hash needed for these) 48// - tls13_traffic_secret -- convenience for the 6 transcript- 49// hash-dependent secrets (c/s hs/app traffic + exp/res master) 50// - tls13_traffic_key + tls13_traffic_iv + tls13_finished_key 51// 52// What it doesn't do yet: 53// - SHA-384 variant (composes against nx_hkdf_sha384; queued) 54// - PSK path early_secret = HKDF-Extract(0, PSK) where PSK != 0 55// (function signature already takes PSK so trivial; just need 56// the caller to wire it from session resumption -- Gap M) 57// - 0-RTT early secrets (queued with Gap M) 58// 59// KAT verified: 60// - RFC 8448 §3 handshake_secret w/ ECDHE = 8bd4054f...92d 61// -> 1dc826e9...eac 62// - RFC 8448 §3 master_secret -> 18df0684...919 63// 64// Composes with: 65// - nx_hkdf (extract) 66// - nx_tls13_kdf (Derive-Secret + HKDF-Expand-Label) 67// - nx_tls13_transcript (queued Gap E; produces H1/H2/H3) 68// 69// license_tier: INDEPENDENT_REDERIVE 70// genealogy_id: international-research-sources/ietf/rfc_8446 71// lineage_id: nishi_tls13_schedule_q10 72 73// nx_safety_envelope: 74// intended_use: AUTO_APPLIED -- primitive-specific tuning queued 75// sil_target: SIL1 76// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail] 77// verdict: NOT_YET_EVALUATED 78 79import "nx_syscalls.nx" 80import "nx_hkdf.nx" 81import "nx_tls13_kdf.nx" 82 83const TLS13_HASH_LEN_SHA256: i64 = 32 84 85// Sealed traffic-secret kind enum -- which label gets fed to 86// Derive-Secret for the four traffic + two master-secret-derived 87// secrets in the cascade. 88const NX_TLS13_LABEL_C_HS_TRAFFIC: i64 = 1 89const NX_TLS13_LABEL_S_HS_TRAFFIC: i64 = 2 90const NX_TLS13_LABEL_C_AP_TRAFFIC: i64 = 3 91const NX_TLS13_LABEL_S_AP_TRAFFIC: i64 = 4 92const NX_TLS13_LABEL_EXP_MASTER: i64 = 5 93const NX_TLS13_LABEL_RES_MASTER: i64 = 6 94 95// ---- Stage 1: early_secret = HKDF-Extract(0^HashLen, PSK) ---- 96// 97// For the no-PSK case, caller passes psk = pointer to zeros, psk_len 98// = HashLen. Writes 32-byte output. 99func tls13_early_secret(psk: *u8, psk_len: i64, out_32: *u8) -> i64 { 100 // RFC 8446 §7.1: salt is empty (HKDF will auto-fill with HashLen zeros). 101 return hkdf_extract(psk, 0, psk, psk_len, out_32) 102} 103 104// ---- Stage 2: derived = Derive-Secret(parent, "derived", "") ---- 105// 106// The cascade "salt for next HKDF-Extract" step. Uses the 107// empty-message SHA-256 hash (constant e3b0c442...) as the 108// Transcript-Hash for the empty-context case. 109// 110// empty_hash MUST be the 32-byte SHA-256 of the empty string; 111// caller's nx_sha256 produces this. We don't hardcode here so the 112// schedule remains hash-agnostic (SHA-384 variant just passes the 113// SHA-384 empty hash and length 48). 114func tls13_derived(parent_secret: *u8, empty_hash: *u8, hash_len: i64, out: *u8) -> i64 { 115 // "derived" = 7 bytes: 64 65 72 69 76 65 64 116 let label: *u8 = sys_mmap(8) 117 label[0]=0x64; label[1]=0x65; label[2]=0x72; label[3]=0x69 118 label[4]=0x76; label[5]=0x65; label[6]=0x64 119 return tls13_derive_secret(parent_secret, label, 7, empty_hash, hash_len, out) 120} 121 122// ---- Stage 3: handshake_secret = HKDF-Extract(derived_1, ECDHE_shared) ---- 123func tls13_handshake_secret( 124 derived_1: *u8, hash_len: i64, 125 ecdhe_shared: *u8, ecdhe_len: i64, 126 out_32: *u8 127) -> i64 { 128 return hkdf_extract(derived_1, hash_len, ecdhe_shared, ecdhe_len, out_32) 129} 130 131// ---- Stage 4: master_secret = HKDF-Extract(derived_2, 0^HashLen) ---- 132// 133// IKM is hash_len bytes of zero (sovereign caller may pass a fresh 134// zero buffer or reuse the early-secret psk buffer). 135func tls13_master_secret( 136 derived_2: *u8, hash_len: i64, 137 out_32: *u8 138) -> i64 { 139 let zeros: *u8 = sys_mmap(64) 140 return hkdf_extract(derived_2, hash_len, zeros, hash_len, out_32) 141} 142 143// ---- Stage 5: per-purpose traffic secrets via Derive-Secret. ---- 144// 145// label_kind picks one of the 6 NX_TLS13_LABEL_* constants. 146// transcript_hash is the SHA-256 (or SHA-384) of the relevant 147// handshake-messages prefix; caller computes it. 148func tls13_traffic_secret( 149 parent_secret: *u8, 150 label_kind: i64, 151 transcript_hash: *u8, hash_len: i64, 152 out: *u8 153) -> i64 { 154 let lbl: *u8 = sys_mmap(16) 155 var lbl_len: i64 = 0 156 if label_kind == NX_TLS13_LABEL_C_HS_TRAFFIC { 157 // "c hs traffic" = 12 bytes 158 lbl[0]=0x63; lbl[1]=0x20; lbl[2]=0x68; lbl[3]=0x73 159 lbl[4]=0x20; lbl[5]=0x74; lbl[6]=0x72; lbl[7]=0x61 160 lbl[8]=0x66; lbl[9]=0x66; lbl[10]=0x69; lbl[11]=0x63 161 lbl_len = 12 162 } else { 163 if label_kind == NX_TLS13_LABEL_S_HS_TRAFFIC { 164 // "s hs traffic" 165 lbl[0]=0x73; lbl[1]=0x20; lbl[2]=0x68; lbl[3]=0x73 166 lbl[4]=0x20; lbl[5]=0x74; lbl[6]=0x72; lbl[7]=0x61 167 lbl[8]=0x66; lbl[9]=0x66; lbl[10]=0x69; lbl[11]=0x63 168 lbl_len = 12 169 } else { 170 if label_kind == NX_TLS13_LABEL_C_AP_TRAFFIC { 171 // "c ap traffic" 172 lbl[0]=0x63; lbl[1]=0x20; lbl[2]=0x61; lbl[3]=0x70 173 lbl[4]=0x20; lbl[5]=0x74; lbl[6]=0x72; lbl[7]=0x61 174 lbl[8]=0x66; lbl[9]=0x66; lbl[10]=0x69; lbl[11]=0x63 175 lbl_len = 12 176 } else { 177 if label_kind == NX_TLS13_LABEL_S_AP_TRAFFIC { 178 // "s ap traffic" 179 lbl[0]=0x73; lbl[1]=0x20; lbl[2]=0x61; lbl[3]=0x70 180 lbl[4]=0x20; lbl[5]=0x74; lbl[6]=0x72; lbl[7]=0x61 181 lbl[8]=0x66; lbl[9]=0x66; lbl[10]=0x69; lbl[11]=0x63 182 lbl_len = 12 183 } else { 184 if label_kind == NX_TLS13_LABEL_EXP_MASTER { 185 // "exp master" = 10 bytes 186 lbl[0]=0x65; lbl[1]=0x78; lbl[2]=0x70; lbl[3]=0x20 187 lbl[4]=0x6d; lbl[5]=0x61; lbl[6]=0x73; lbl[7]=0x74 188 lbl[8]=0x65; lbl[9]=0x72 189 lbl_len = 10 190 } else { 191 if label_kind == NX_TLS13_LABEL_RES_MASTER { 192 // "res master" 193 lbl[0]=0x72; lbl[1]=0x65; lbl[2]=0x73; lbl[3]=0x20 194 lbl[4]=0x6d; lbl[5]=0x61; lbl[6]=0x73; lbl[7]=0x74 195 lbl[8]=0x65; lbl[9]=0x72 196 lbl_len = 10 197 } else { 198 return 0 - 1 // unknown label_kind 199 } 200 } 201 } 202 } 203 } 204 } 205 return tls13_derive_secret(parent_secret, lbl, lbl_len, transcript_hash, hash_len, out) 206} 207 208// ---- Per-traffic-secret AEAD key derivation. ---- 209// 210// key = HKDF-Expand-Label(traffic_secret, "key", "", key_length). 211// For ChaCha20-Poly1305: key_length = 32. For AES-128-GCM: 16. 212func tls13_traffic_key(traffic_secret: *u8, key_len: i64, out: *u8) -> i64 { 213 let lbl: *u8 = sys_mmap(8) 214 lbl[0]=0x6b; lbl[1]=0x65; lbl[2]=0x79 // "key" 215 let empty: *u8 = sys_mmap(8) 216 return tls13_hkdf_expand_label(traffic_secret, lbl, 3, empty, 0, key_len, out) 217} 218 219// iv = HKDF-Expand-Label(traffic_secret, "iv", "", iv_length). 220// For ChaCha20-Poly1305 and AES-GCM: iv_length = 12. 221func tls13_traffic_iv(traffic_secret: *u8, iv_len: i64, out: *u8) -> i64 { 222 let lbl: *u8 = sys_mmap(8) 223 lbl[0]=0x69; lbl[1]=0x76 // "iv" 224 let empty: *u8 = sys_mmap(8) 225 return tls13_hkdf_expand_label(traffic_secret, lbl, 2, empty, 0, iv_len, out) 226} 227 228// finished_key = HKDF-Expand-Label(base_key, "finished", "", Hash.length). 229// Used to compute the Finished MAC as HMAC(finished_key, transcript_hash). 230func tls13_finished_key(base_key: *u8, hash_len: i64, out: *u8) -> i64 { 231 let lbl: *u8 = sys_mmap(16) 232 lbl[0]=0x66; lbl[1]=0x69; lbl[2]=0x6e; lbl[3]=0x69 // "fini" 233 lbl[4]=0x73; lbl[5]=0x68; lbl[6]=0x65; lbl[7]=0x64 // "shed" 234 let empty: *u8 = sys_mmap(8) 235 return tls13_hkdf_expand_label(base_key, lbl, 8, empty, 0, hash_len, out) 236}