code wiki / (root) / nx_connect_seal_gate.nx

nx_connect_seal_gate.nx source

↩ module page · 94 lines · 5420 B

1// nx_connect_seal_gate.nx -- proves CONNECT message sealing is REAL AEAD, not the additive stand-in. 2// The load-bearing teeth are the ones the old stand-in FAILED: tamper-rejection and no-keystream-reuse. 3// license_tier: ORIGINAL expect_exit: 0 4import "nx_syscalls.nx" 5import "nx_connect_seal.nx" 6 7func w(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 } 8func wn(v: i64) -> i64 { let t: *u8=sys_mmap(28); var m: i64=v; var k: i64=0; if m==0{t[0]=48 as u8;k=1} while m>0{t[k]=(48+(m%10)) as u8;m=m/10;k=k+1} let b: *u8=sys_mmap(28); var i: i64=0; while i<k{b[i]=t[k-1-i];i=i+1} sys_write(1,b,k); return 0 } 9func ck(pass: i64, label: *u8, fails: *i64) -> i64 { 10 w(" " as *u8); w(label); w(": " as *u8) 11 if pass==1 { w("PASS\n" as *u8) } else { w("FAIL\n" as *u8); fails[0]=fails[0]+1 } 12 return 0 13} 14func eqbytes(a: *u8, b: *u8, n: i64) -> i64 { var i: i64=0; while i<n { if (a[i]&0xff)!=(b[i]&0xff) { return 0 } i=i+1 } return 1 } 15 16// NEG-CONTROL: a model of the old stand-in -- XOR with a fixed keystream byte, NO authentication. 17// "decrypt" always "succeeds" and returns bytes, even for a tampered ciphertext -> the danger. 18func xor_seal(pt: *u8, n: i64, ct: *u8) -> i64 { var i: i64=0; while i<n { ct[i]=(pt[i]^0x5a) as u8; i=i+1 } return 0 } 19func xor_open(ct: *u8, n: i64, pt: *u8) -> i64 { var i: i64=0; while i<n { pt[i]=(ct[i]^0x5a) as u8; i=i+1 } return 1 } // always "ok" 20 21func main() -> i64 { 22 let fails: *i64 = sys_mmap(16) as *i64 23 fails[0]=0 24 w("=== nx_connect_seal_gate -- CONNECT messages on REAL RFC-8439 ChaCha20-Poly1305 AEAD ===\n" as *u8) 25 26 let key: *u8 = sys_mmap(32) 27 var i: i64=0 28 while i<32 { key[i]=(0x40+i) as u8; i=i+1 } // a fixed test conversation key 29 let pt: *u8 = "meet me at the library saturday, bring the book" as *u8 30 var plen: i64=0 31 while pt[plen]!=(0 as u8) { plen=plen+1 } 32 let ct: *u8 = sys_mmap(256) 33 let tag: *u8 = sys_mmap(32) 34 let out: *u8 = sys_mmap(256) 35 36 // T1: round-trip -- seal at seq 7, open at seq 7 restores the plaintext exactly 37 let s1: i64 = cseal_seal(key, 7, pt, plen, ct, tag) 38 let o1: i64 = cseal_open(key, 7, ct, plen, tag, out) 39 var t1: i64=0 40 if s1==CSEAL_OK { if o1==CSEAL_OK { if eqbytes(pt, out, plen)==1 { t1=1 } } } 41 ck(t1, "T1 round-trip: seal then open restores the message byte-exact" as *u8, fails) 42 43 // T2: content-blind -- ciphertext differs from plaintext (server sees noise), and the WRONG key cannot open 44 var t2: i64=1 45 if eqbytes(pt, ct, plen)==1 { t2=0 } // ct must not equal pt 46 let badkey: *u8 = sys_mmap(32) 47 i=0; while i<32 { badkey[i]=(0x40+i) as u8; i=i+1 } 48 badkey[0]=0x00 as u8 // one byte different 49 let obad: i64 = cseal_open(badkey, 7, ct, plen, tag, out) 50 if obad!=CSEAL_REJECT { t2=0 } // server / attacker without the real key cannot read 51 ck(t2, "T2 content-blind: ciphertext != plaintext AND a wrong key is REJECTED (no plaintext leak)" as *u8, fails) 52 53 // T3: TAMPER rejection (ciphertext) -- the property the additive stand-in NEVER had 54 let ct2: *u8 = sys_mmap(256) 55 i=0; while i<plen { ct2[i]=ct[i]; i=i+1 } 56 ct2[3] = (ct2[3] ^ 0x01) as u8 // flip one bit 57 let ot: i64 = cseal_open(key, 7, ct2, plen, tag, out) 58 var t3: i64=0; if ot==CSEAL_REJECT { t3=1 } 59 ck(t3, "T3 tamper rejection: a 1-bit ciphertext flip is REJECTED (authenticated)" as *u8, fails) 60 61 // T4: TAMPER rejection (tag) -- forging the tag fails 62 let tag2: *u8 = sys_mmap(32) 63 i=0; while i<16 { tag2[i]=tag[i]; i=i+1 } 64 tag2[0] = (tag2[0] ^ 0x80) as u8 65 let ot2: i64 = cseal_open(key, 7, ct, plen, tag2, out) 66 var t4: i64=0; if ot2==CSEAL_REJECT { t4=1 } 67 ck(t4, "T4 tag forgery rejection: a flipped auth tag is REJECTED" as *u8, fails) 68 69 // T5: no keystream reuse -- the SAME plaintext at seq 7 vs seq 8 yields DIFFERENT ciphertext (distinct nonce) 70 let ct8: *u8 = sys_mmap(256) 71 let tag8: *u8 = sys_mmap(32) 72 cseal_seal(key, 8, pt, plen, ct8, tag8) 73 var t5: i64=0; if eqbytes(ct, ct8, plen)==0 { t5=1 } 74 ck(t5, "T5 nonce discipline: identical plaintext at seq 7 vs 8 -> different ciphertext (no keystream reuse)" as *u8, fails) 75 76 // T6: replay/reorder detection -- a message sealed at seq 7 fails to open when presented as seq 8 77 let o6: i64 = cseal_open(key, 8, ct, plen, tag, out) 78 var t6: i64=0; if o6==CSEAL_REJECT { t6=1 } 79 ck(t6, "T6 replay/reorder: seq-7 message rejected when opened as seq 8 (sequence bound into the tag)" as *u8, fails) 80 81 // T7: NEG-CONTROL -- the additive/XOR stand-in ACCEPTS a tampered message silently; AEAD rejected it (T3) 82 let xct: *u8 = sys_mmap(256) 83 xor_seal(pt, plen, xct) 84 xct[3] = (xct[3] ^ 0x01) as u8 // same tamper as T3 85 let xr: i64 = xor_open(xct, plen, out) // returns 1 ("ok") -- NO authentication 86 var t7: i64=0; if xr==1 { if ot==CSEAL_REJECT { t7=1 } } 87 ck(t7, "T7 NEG-CONTROL: the additive stand-in ACCEPTS the tamper AEAD rejects (auth is load-bearing)" as *u8, fails) 88 89 w(" fails=" as *u8); wn(fails[0]); w("\n" as *u8) 90 if fails[0]==0 { w("VERDICT: verdict=GREEN (CONNECT messages sealed with real RFC-8439 AEAD: authenticated, nonce-safe, content-blind)\n" as *u8); sys_exit(0) } 91 w("VERDICT: verdict=RED\n" as *u8) 92 sys_exit(1) 93 return 1 94}