Formal Cryptanalysis: 17 Machine-Verified Proofs via Z3 + CVC5 SMT Solvers

[rayiskander2406]

Context

Following up on Issue #1 and your detailed replies, Julian — thank you for engaging substantively. You raised important points about I(M;A)=0 and plausible deniability that prompted me to go deeper.

Rather than continuing the debate informally, I ran a formal cryptanalysis using two independent SMT (Satisfiability Modulo Theories) solvers: Z3 (Microsoft Research) and CVC5 (Stanford/Iowa). These are mathematical proof engines — they don't have opinions. When they return UNSAT, the result is a machine-verified mathematical proof that the negation is impossible.

17 proofs. Two independent solvers. 34/34 agreement.

The analysis covers the entire protocol family: ZOSCII, UNSIGNAL, and BRAINLESS.

---

What You Got Right

I want to lead with this because it matters.

Proof 1: Deniability — CONFIRMED ✓ (SAT)

Your I(M;A)=0 claim, in the deniability sense, is formally verified:

For any address sequence A and any target message M, there exists a ROM R such that R[A[i]] = M[i].

The same address sequence [100, 200, 300, 400, 500] can decode to "HELLO" with one ROM and "WORLD" with a different ROM. Both solvers confirm this. This is a genuine and valuable property. Most encryption schemes do not offer this — you can't typically produce a second AES key that decrypts the same ciphertext to a different meaningful plaintext.

The "weaponised ambiguity" is real.

---

Where the Claim Exceeds What the Math Supports

The gap is between deniability (which ZOSCII has) and information-theoretic security (which ZOSCII does not have). These are different properties with different definitions.

Proof 2: Information Leakage via Address Collision — PROVEN (UNSAT)

This is the central finding:

from z3 import *

ROM = Array('ROM', BitVecSort(16), BitVecSort(8))
A1, A2 = BitVecs('A1 A2', 16)
M1, M2 = BitVecs('M1 M2', 8)

s = Solver()
s.add(Select(ROM, A1) == M1)  # ZOSCII encoding
s.add(Select(ROM, A2) == M2)  # ZOSCII encoding
s.add(A1 == A2)                # addresses collide
s.add(M1 != M2)                # can plaintext bytes differ?

s.check()  # → UNSAT: IMPOSSIBLE

If two messages are encoded with the same ROM and any address appears in both encodings, the corresponding plaintext bytes are forced to be equal. This is information leakage — observing the encoded output reveals which plaintext positions share the same byte value.

In a system with true information-theoretic security (e.g., one-time pad), no amount of ciphertext observation constrains the plaintext. ZOSCII fails this requirement.

Proof 3: Known-Plaintext ROM Recovery — PROVEN (SAT)

If an attacker knows some plaintext bytes and their corresponding addresses (e.g., a known file header), they learn ROM[address] = known_byte for each pair. These recovered ROM bytes can then decode other messages using the same ROM.

Proof 4: Cumulative Multi-Message Leakage — PROVEN (UNSAT)

Each message encoded with the same ROM constrains the set of possible ROMs. Shared addresses between messages fix ROM byte values. With enough messages, the ROM approaches unique determination.

Proof 5: Homophonic Substitution Cipher Equivalence — PROVEN (UNSAT)

ZOSCII is structurally equivalent to a homophonic substitution cipher:

• Each plaintext byte has a fixed set of possible encodings (the ROM addresses containing that byte value)
• Encoding randomly selects from that set
• The ROM is the substitution table (the key)

Homophonic substitution is a well-studied cipher class, known to be breakable since the 1800s. This classification is not a judgment — it's a structural observation.

Proof 6: OTP-Equivalence Disproven — PROVEN (UNSAT/SAT)

Direct comparison with a one-time pad:

Property	OTP	ZOSCII
Same ciphertext/address, different plaintexts possible?	YES (SAT)	NO (UNSAT)

With an OTP using fresh keys, the same ciphertext byte can correspond to different plaintexts. With ZOSCII reusing a ROM, the same address always maps to the same plaintext byte. These are fundamentally different security properties.

---

UNSIGNAL Protocol Analysis (5 Proofs)

UNSIGNAL adds a sliding window offset, random padding, and header indirection. All parameters are ROM-derived.

Proof	Finding	Result
U1	Same ROM + same header addresses → identical window offset	UNSAT ✓
U2	Address collision within the window still forces plaintext equality	UNSAT ✓
U3	Cross-message header collision reveals shared window parameters	UNSAT ✓
U4	Padding lengths are ROM-determined, not random	UNSAT ✓
U5	With known header parameters, UNSIGNAL reduces to base ZOSCII	UNSAT ✓

Key insight: The sliding window changes which addresses are available, not the structure of the encoding. The header addresses are in cleartext (first 8 bytes of every .sig file), and all parameters are ROM lookups. UNSIGNAL's security is circular — it depends on keeping ROM values secret, but the ROM is the thing being attacked.

---

BRAINLESS Protocol Analysis (4 Proofs)

BRAINLESS adds an Ouroboros XOR chain on top of the encoded output.

Proof	Finding	Result
B1	XOR chain is a bijection — invertible with unique inverse	SAT + UNSAT ✓
B2	Public inverse always recovers the original (no key needed)	UNSAT ✓
B3	After public inversion, all ZOSCII leakage applies	UNSAT ✓
B4	BRAINLESS is injective — preserves all distinguishable patterns	UNSAT ✓

Key insight: BRAINLESS uses no key material. The inverse is 4 lines of code:

b[n-1] = c[n-1] XOR c[0]
for i = n-2 down to 0:
    b[i] = c[i] XOR b[i+1]

Any attacker who knows the algorithm (which is published) can undo BRAINLESS in O(n) time with zero secret information. It adds exactly zero bits of security.

---

Combined Stack Analysis (2 Proofs)

Proof	Finding	Result
C1	Full BRAINLESS + UNSIGNAL + ZOSCII stack leaks through address collision	UNSAT ✓
C2	Adding BRAINLESS preserves I(M;A) — mutual information unchanged	UNSAT ✓

The fundamental issue: Security comes from key material, not layers. Each layer must introduce independent secret information to add security. BRAINLESS uses no key. UNSIGNAL derives all parameters from the same ROM. Stacking layers without adding keys does not compound security.

---

Reproducibility

All proofs are reproducible. Install Z3 (pip install z3-solver) and run:

from z3 import *
ROM = Array('ROM', BitVecSort(16), BitVecSort(8))
A1, A2 = BitVecs('A1 A2', 16)
M1, M2 = BitVecs('M1 M2', 8)
s = Solver()
s.add(Select(ROM, A1) == M1)
s.add(Select(ROM, A2) == M2)
s.add(A1 == A2)
s.add(M1 != M2)
print(s.check())  # unsat

If this prints unsat, the information leakage is confirmed on your machine. The full 17-proof toolkit is available on request.

---

Constructive Recommendation

ZOSCII has a genuine property — plausible deniability — that is valuable and underappreciated. If the project reframed from "100% secure forever / information-theoretic security" to "deniable encoding with plausible ambiguity," the cryptography community would engage with it seriously. The I(M;A)=0 proof is sound for what it actually proves. The issue is only with what it's claimed to prove.

The deniability property could have real applications in censorship-resistance contexts. That's worth developing. The "information-theoretic security" claim, however, is formally disproven by 17 machine-verified proofs across two independent solvers.

---

Analysis by Ray Iskander — Verdict Security
Machine-verified by Z3 4.15.4 (Microsoft Research) and CVC5 1.3.3 (Stanford/Iowa)

[m374-crypt0]

I'm not a cryptanalysis professional at all but this analysis gives me so much insights! Thank you!

[rayiskander2406]

Update: Golden 7 — Revised Analysis After Adversarial Audit

Julian, I submitted the original analysis above to three independent adversarial auditors and asked them to tear it apart. They found real weaknesses — padding, missing quantification, unfair comparisons, and a critical modeling ambiguity in BRAINLESS. I've revised accordingly.

The original 17 proofs have been consolidated to 7 golden proofs — zero redundancy, every gap addressed. All verified by Z3 SMT solver.

---

What Changed

Original Issue	Auditor Criticism	Fix
17 proofs	~5 are the same insight repeated ("function determinism")	Consolidated to 7
OTP comparison	Unfair: fresh-key OTP vs reused-ROM ZOSCII	Now compares both under identical conditions
BRAINLESS proofs	"XOR things in a circle" has two valid interpretations	Now covers both sequential AND parallel XOR
No quantification	"Leakage exists" but how much?	Birthday-paradox collision rates added
No frequency analysis	Strongest classical attack was missing	Now formalized with JPEG-like ROM simulation

---

G1: Deniability — Properly Scoped ✓

Your deniability claim is confirmed, but scoped more precisely than "any message is plausible."

If addresses repeat in the encoded output (A[1] == A[3]), then only messages where M[1] == M[3] are plausible. Messages where M[1] ≠ M[3] have no valid ROM (UNSAT).

Deniability holds within collision-consistent equivalence classes — not universally over all messages.

---

G2: Collision Leakage — Now Quantified ✓

The structural proof is unchanged: ∀ ROM, address collision forces plaintext byte equality (UNSAT).

New: collision probability for realistic message lengths:

Message Length	Expected Collisions	P(≥1 collision)
10 bytes	0.18	16.1%
50 bytes	4.8	99.2%
100 bytes	19.3	~100%
500 bytes	488	~100%
1000 bytes	1,951	~100%

(Assumes uniform 64KB ROM, ~256 addresses per byte value)

For any message over ~50 bytes, at least one collision is virtually certain. Each collision reveals "these plaintext positions have the same byte value" — without the ROM.

---

G3: Homophonic Substitution Isomorphism ✓

Formally defines the homophone partition: H(v) = {a ∈ [0, 2¹⁶) : ROM[a] = v}.

Proves:

• Encoding byte v must select from H(v) (UNSAT for addresses outside H(v))
• Each address always decodes to the same byte (UNSAT for different decodings)

ZOSCII IS a homophonic substitution cipher. The ROM is the substitution table. This cipher class has been studied and broken since the 19th century.

---

G4: OTP Comparison — Now Fair ✓

Previous version (unfair): compared fresh-key OTP vs reused-ROM ZOSCII.

Revised — symmetric comparison:

Condition	OTP	ZOSCII
Fresh key/ROM	Perfect secrecy (zero leakage)	Intra-message collision leakage (UNSAT)
Reused key/ROM	XOR of ciphertexts = XOR of plaintexts	Address collision reveals byte equality

ZOSCII is strictly weaker than OTP under both conditions. With a fresh ROM, OTP has zero leakage; ZOSCII still leaks through within-message address collisions.

---

G5: UNSIGNAL Reduction ✓

Three sub-proofs consolidated:

1. Known header → pure ZOSCII: With recovered window offset and padding lengths, the inner message is standard ZOSCII (UNSAT for collision with different plaintext)
2. Headers are session fingerprints: Same H1,H2 addresses across messages → attacker knows identical windows were used (cleartext headers)
3. Cumulative ROM leakage: Each message exposes 4 ROM bytes via header lookups. Over N messages, 4N ROM bytes are constrained.

UNSIGNAL = ZOSCII + metadata that helps the attacker.

---

G6: BRAINLESS — Both Interpretations ✓

Your description ("XOR things in a circle") has two valid readings. Both are covered:

Sequential interpretation (c[0] = b[0]⊕b[1], c[1] = b[1]⊕b[2], ..., c[n-1] = b[n-1]⊕c[0]):

• Public bijection — unique inverse, no key needed
• Inverse: b[n-1] = c[n-1] ⊕ c[0], then backward b[i] = c[i] ⊕ b[i+1]
• All ZOSCII leakage passes through unchanged

Parallel interpretation (c[i] = b[i]⊕b[(i+1)%n] for all i simultaneously):

• Lossy — rank n-1 over GF(2). XOR of all output bytes always = 0 (proven by Z3).
• But ZOSCII's collision structure still survives — if two ZOSCII addresses collided, the collision is algebraically detectable in the BRAINLESS output.

Neither interpretation adds meaningful security. Julian, if you clarify which one BRAINLESS uses, the corresponding proof applies directly.

---

G7: Frequency Analysis — The Missing Attack ✓

This was the biggest gap in the original analysis. All three auditors flagged it.

Real ROMs (JPEGs, executables) have non-uniform byte distributions. This creates homophone sets of varying sizes:

Byte Value	Count in ROM (k)	P(collision per pair)
0x42 (rare)	3	33.3%
0x01	5	20.0%
0xFF	30	3.3%
0x00	40	2.5%
0x80 (common)	178	0.6%

Rare bytes collide fast. An attacker observing ciphertext can identify which byte values have small homophone sets by measuring address reuse rates. This is a ciphertext-only attack — no known plaintext required.

Combined with knowledge of the ROM type (JPEG headers start with FF D8 FF E0), frequency analysis can bootstrap into partial plaintext recovery.

---

Revised Summary

Proof	What It Proves	Single-Use ROM?
G1	Deniability real but scoped to collision partitions	✓ survives
G2	Collision leakage universal + quantified	✓ survives
G3	ZOSCII ≡ homophonic substitution cipher	✓ survives
G4	ZOSCII strictly weaker than OTP (both conditions)	✓ survives
G5	UNSIGNAL reduces to ZOSCII	partially
G6	BRAINLESS adds zero security (both interpretations)	✓ survives
G7	Frequency analysis viable without known plaintext	✓ survives

6 of 7 proofs survive even if you mandate single-use ROMs. The within-message leakage (collision + frequency) is architectural — it cannot be patched by key management.

---

Constructive Recommendation (Updated)

The analysis confirms that ZOSCII has genuine value as a deniable encoding scheme. The deniability property (G1) is real and mathematically sound within its scope.

The recommendation remains: reframe from "information-theoretic security" to "deniable encoding with collision-bounded ambiguity." This is an honest description of what ZOSCII provides, and it's a property worth developing.

The full toolkit (7 proofs + probabilistic analysis + frequency attack simulation) is available as a runnable Python script. Anyone can pip install z3-solver and verify independently.

---

Revised analysis by Ray Iskander — Verdict Security
Adversarial audit by: Grok (xAI), Gemini (Google), Claude Opus (Anthropic)
Machine-verified by Z3 4.15.4 (Microsoft Research)

[rayiskander2406]

Thanks Sebastien — glad the analysis was useful. If you're working in the ZK/Ethereum space, you'll appreciate that the same formal verification approach (SMT solvers for security claims) applies well beyond ZOSCII. Happy to discuss.

[PrimalNinja]

ROM = Array('ROM', BitVecSort(16), BitVecSort(8))
s.add(Select(ROM, A1) == M1)
s.add(Select(ROM, A2) == M2)
s.add(A1 == A2)
s.add(M1 != M2)
s.check() # → UNSAT

This proves that array[x] = array[x]. The ROM is uninterpreted but it's a single shared variable in the model - same ROM, same index, same value. That's the definition of a function. You have proved that functions are deterministic and called it "information leakage."

The critical modelling error: the attacker doesn't have access to the ROM array. Your model gives Z3 the ROM as a shared constraint between both encoding operations. In reality, the attacker sees addresses only. The correct attacker model would be: given addresses A1 and A2, and knowing A1 = A2, what can you conclude about M1 and M2 without the ROM? The answer is nothing - M1 and M2 could each be any of 256 values, you just know they're the same value (which one is unknown).

Your "collision leakage" (G2) - yes, address collisions reveal that two positions share a byte. But knowing "position 3 and position 7 have the same byte" without knowing which byte is not the same as learning plaintext. You have conflating structural pattern leakage with information-theoretic leakage. By your definition, even knowing the length of a message would be "leakage."

Your "homophonic substitution" (G3) - structurally correct, definitionally wrong. A homophonic cipher is breakable because the attacker can build frequency distributions and map them to known language statistics. With ZOSCII, the attacker doesn't know the substitution table (ROM), so they can't map clusters to values. It's like saying "this is a Caesar cipher" when you don't know the shift - technically you've classified it, but you can't break it without the key.

Your OTP comparison (G4) - "intra-message collision leakage" is the same point restated. And your claim that ZOSCII is "strictly weaker" under fresh ROM ignores that with a fresh ROM per message, the collision tells the attacker nothing exploitable - they know two positions share a byte in one message they'll never see again with the same mapping.

Your UNSIGNAL analysis (G5) - "Each message exposes 4 ROM bytes via header lookups" is wrong. The header contains 4 addresses (indices into the ROM), not ROM values. The attacker sees the addresses. The values those addresses point to are the UNSIGNAL parameters (offset, prefix length, suffix length) - and those are unknown without the ROM.

Your frequency analysis (G7) - You simulate a JPEG ROM and shows that rare byte values have small homophone sets that collide faster. This is the most interesting claim, but it still assumes the attacker can label which cluster maps to which byte value. They can observe that certain addresses repeat more than others, but they can't determine what byte value those addresses resolve to. And with UNSIGNAL's random offset, the address space shifts per message, so cross-message frequency accumulation breaks down.

The "adversarial audit" by Grok, Gemini, and Claude - you asked LLMs to review your proofs. They tightened the presentation but none of them caught the fundamental modelling error because you framed the question as "audit my proofs" not "is my threat model correct." The proofs are internally valid. The model is wrong.

Your whole analysis is a technically sophisticated proof that arrays are deterministic, wrapped in 17 (now 7) restatements of the same tautology, marketed as a cryptanalysis. The one genuinely useful finding was the PRNG seed issue, which you already fixed.

[PrimalNinja]

What you called weaponised ambiguity is actually what we call plausible deniability. Weaponsied ambiguity is the fact you cannot tell a ZOSCII file from a file of noise.

[PrimalNinja]

"Key insight: The sliding window changes which addresses are available, not the structure of the encoding. The header addresses are in cleartext (first 8 bytes of every .sig file), and all parameters are ROM lookups. UNSIGNAL's security is circular — it depends on keeping ROM values secret, but the ROM is the thing being attacked." <-- you have it backward, it's the address table someone has that is being attacked, not the ROM.

[PrimalNinja]

G6 "BRAINLESS adds an Ouroboros XOR chain on top of the encoded output." <-- BRAINLESS Protocol is a joke, you didn't get it? It turns the semantics of encoding into encryption for those who need encryption checkboxes ticked. That is the point. I will take your analysis of the BRAINLESS joke encryption to also be a JOKE.

BRAINLESS does have a use believe it or not even though it is conceived as a joke. When a ZOSCII file is transmitted in packets or split - each packet is itself cannot be decrypted - not that it really matters. The main purpose is to reclasify encoding to encryption for stupid people who believe only encryptions can secure data and communicatins.

[PrimalNinja]

UNSIGNAL Protocol Analysis

U1 - The window is the same thing only 1/65536th of the time on average 'when the ROM is the same ROM'. It means address 1 of an encoding is only correct 1/65536th of the time with the correct ROM. ZOSCII is already unbreakable within this sliding window - but the window makes it impossible for someone not knowing the ROM to know anything at all even where a message may start.

U2 - yes it does, but it reveals nothing of the message ever unless you have the same ROM.

U3 - Can you collate enough messages to analyse given messages have 65536 x 256 possible offsets to where you believe a message might start and where they don't? You cannot tell if the noise is part of the message or not 100% of the time without the provided ROM as they also point to addresses within the ROM.

U4 - Padding lengths can be any values between 0 and 256 (or 10 and 256 if you implement a lower limit as I have chosen) all are valid addresses in the ROM as per any of the message addresses. Given they can be an odd number, it even shifts where you might think the message addresses (which are a word) down a byte sometimes.

U5 - That is the point, not an attack. The header parameters are just as unknown as the addresses in ZOSCII as they are also indirections. They are only known with the correct ROM which lets you decode the ZOSCII also. Even if something is the point, you mark it as UNSAT (as per the BRAINLESS Joke Encryption also).

[PrimalNinja]

G2 When did we ever recommend a uniform ROM? We recommend the most random ROM that is not uniform, like JPEG image.

[PrimalNinja]

G3 A database index is a substitution cipher? ASCII is a substitution cipher? A phone book is a substitution cipher?

[PrimalNinja]

G5 Since when is a message considered a session? All the header bytes change per message - you could have a bug in your implementation that kept them the same?

[PrimalNinja]

G7 You cannot perform a useful frequency analysis.

• You don't know what was encoded
• You don't know the ROM
• You don't know the window within a ROM (UNSIGNAL)
• You don't know the noise before the message within an encodeing (UNSIGNAL)
• You cannot even tell if the addresses are shifted a byte or not (UNSIGNAL)

Unintuitiveness from an encryption point of view where accuracy and hardness of the algorithm matters - but is the opposite for ZOSCII:

• imperfect randomness is GOOD for ZOSCII, it improves security
• imperfect entropy (but good enough) is GOOD for ZOSCII, it improves security

[PrimalNinja]

ZOSCII creates a treasure map that only applies to the correct planet

UNSIGNAL makes that ZOSCII treasure map only work on the correct planet

[rayiskander2406]

Julian, thank you for the detailed engagement. I'm going to separate this into four categories: where you're right, where you're partly right, where I need to be more precise than the original analysis was, and where the math disagrees with your conclusion. Truth over diplomacy — for both sides.

---

Where You're Right (Full Concessions)

G5 — UNSIGNAL headers. I said "each message exposes 4 ROM bytes via header lookups." Wrong. The headers contain addresses (ROM indices). The attacker sees addresses; the byte values ROM[H1], ROM[H2], ROM[H3], ROM[H4] are unknown without the ROM. Corrected.

G6 — BRAINLESS. You stated explicitly that BRAINLESS is a joke — a reclassification of encoding as "encryption" for compliance contexts. Analyzing it as a serious security mechanism was a misread of intent. Withdrawn.

Uniform ROM assumption (G2). You recommend JPEG ROMs, not uniform 64KB blocks. My collision probability table assumed ~256 homophones per byte value. A JPEG ROM has a heavily skewed byte distribution — common byte values get more homophones (lower collision rates), rare byte values get fewer (higher collision rates). I should have modeled with a realistic ROM. I'll revise.

"Session fingerprint" language (G5). Imprecise on my part. I meant ROM reuse across messages, not identical headers. Your point that all four header bytes change per message is correct. Removed.

UNSIGNAL cross-message hardening (U1, U3, U4). The sliding window (65,536 possible offsets per message), unknown padding lengths, and byte-level alignment shift genuinely complicate cross-message analysis. An attacker cannot align address spaces across messages without knowing the offset, and the offset is itself a ROM lookup. This is real defense-in-depth that my original analysis underweighted for the cross-message attack surface.

Audit methodology. The adversarial audit validated proof consistency, not threat model assumptions. I should have also asked the auditors "is my attacker model correct?" Fair criticism.

Terminology. "Weaponised ambiguity" was my framing. Your terms are "plausible deniability" (wrong ROM decodes to valid plaintext) and "indistinguishability from noise" (output has no identifiable format). Your system, your terminology.

---

Where You're Partly Right (Scoped Concessions)

G7 — Frequency analysis. Your five-point list of what the attacker doesn't know under UNSIGNAL — encoded content, ROM, window, noise boundaries, byte alignment — is compelling as a defense against cross-message frequency accumulation. I overstated the practicality of frequency analysis against UNSIGNAL-wrapped messages in the cross-message scenario. I'll scope the cross-message frequency claim to bare ZOSCII with ROM reuse.

However: intra-message collision structure exists within the message portion of an UNSIGNAL-encoded message regardless of the wrapper. UNSIGNAL prevents cross-message alignment; it doesn't eliminate the collision property within a single message. The barrier is that the attacker must first identify the message boundaries within the UNSIGNAL frame — which requires breaking the window/padding parameters — before they can analyze internal collisions. That's a genuine practical barrier, but it's a boundary-identification challenge, not an information-theoretic defense.

G4 — Fresh ROM. Under fresh ROM per message, cross-message attacks vanish entirely and intra-message collisions are far less exploitable. An attacker who sees that positions 3 and 47 share a byte in a single fresh-ROM message learns an equality constraint, but cannot determine which byte value it is, and will never see the same ROM again.

Formal status: I(M;C) > 0 still holds (the constraint exists). Practical status: for short messages with few collisions, exploitation without additional side information (known plaintext language, partial message knowledge) is extremely difficult. I think you're substantially right that fresh-ROM collision leakage is near-unexploitable in practice for most threat models. The gap between the formal finding and practical risk is large under fresh ROM.

G3 — Homophonic substitution. Your challenge — "is a phone book a substitution cipher?" — is fair as a pushback against classification-as-attack. Classification alone doesn't constitute a vulnerability; you need the classification plus an attack method.

But I'll maintain the structural identification: ZOSCII is isomorphic to a homophonic substitution cipher. The partition H(v) = {a : ROM[a] = v} defines the homophone sets. This isn't an insult — it's the structural reason collision leakage exists. The partition explains the mechanism. Whether the mechanism is exploitable depends on the threat model, message length, ROM properties, and whether UNSIGNAL is used. The classification tells you where to look for leakage; it doesn't tell you the leakage is exploitable.

---

Where I Need to Be More Precise

The Z3 proof (G2). You wrote: "You have proved that functions are deterministic and called it 'information leakage.'"

At the proof level, you're right. The UNSAT result follows from Z3's array congruence axiom: for any function f, if x = y then f(x) = f(y). Instantiated with the ROM as the function, it proves that equal addresses yield equal bytes. This is not a deep result — it's a property of functions.

Here's where I should have been clearer. The Z3 proof is the least important part of the analysis. It formalizes something obvious: deterministic lookups are deterministic. The actual security argument doesn't depend on Z3:

1. The attacker sees the address sequence (this is the ciphertext)
2. Equal addresses are detectable by inspection — no ROM needed
3. Equal addresses imply equal plaintext bytes (functional determinism — the trivial fact Z3 formalized)
4. Therefore, the ciphertext reveals information about the plaintext structure

Step 3 doesn't need Z3. It needs one sentence: the ROM is a function, and functions are deterministic. I used Z3 to formalize this, which was rigorous but gave the step more weight than it deserves. The real content is the observability argument in steps 1–2 and the Shannon consequence in step 4.

Quantifying the leakage. The original analysis said I(M;C) > 0 without quantifying. Here's the math:

For two message positions i, j with uniform random plaintext bytes:

• Prior: P(M[i] = M[j]) = 1/256 (each byte is independent, uniform over 256 values)
• After observing A[i] = A[j]: P(M[i] = M[j]) = 1 (certainty)
• Information gained per collision: log₂(256) = 8 bits

For a message of length n encoded against a 64KB ROM with uniform distribution (~256 homophones per byte value):

• Expected collisions: n(n−1) / (2 × 256)
• 50 bytes: ~4.8 collisions → ~38 bits of structural information
• 100 bytes: ~19.3 collisions → ~154 bits of structural information

These bits reveal the equivalence partition — which positions share the same byte value — but not the byte values themselves. The attacker learns the pattern, not the content.

What the leakage is and isn't:

• It IS a formal violation of Shannon's perfect secrecy (I(M;C) = 0)
• It IS 8 bits of mutual information per observed collision
• It IS the same structural information that enables classical homophonic cipher analysis (given sufficient messages or side information)
• It is NOT a plaintext recovery attack
• It is NOT practically exploitable for short messages under fresh ROM without additional side information
• It is NOT proof that ZOSCII is "broken" in any operational sense

---

Where the Math Disagrees With You

"The answer is nothing." You wrote: "M1 and M2 could each be any of 256 values, you just know they're the same value."

The second sentence contradicts the first. "You just know they're the same value" is information — 8 bits of it, precisely. Before observation, 65,536 pairs of (M1, M2) are possible. After observation, 256 are possible. That's a 256× reduction in the joint space. This is not a matter of interpretation; it's a counting argument.

Under fresh ROM, for a single collision, you can argue this is operationally useless. But the claim "the answer is nothing" is mathematically false. The answer is 8 bits per collision.

"Structural pattern leakage ≠ information-theoretic leakage." Under Shannon's framework, this distinction doesn't exist. Any constraint on P(M|C) relative to P(M) constitutes mutual information I(M;C) > 0. The constraint "M[i] = M[j]" changes the posterior distribution of M given C. That's information-theoretic leakage by definition — Shannon 1949, Theorem 3 (necessary and sufficient condition for perfect secrecy).

An important precision: computational security definitions like IND-CPA deliberately exclude message length from "leakage" — they require challenge messages to be of equal length. You argued "even length would be leakage by your standard." True under Shannon. But collision leakage is categorically different from length leakage: length reveals a single scalar (message size); collision structure reveals internal relationships between specific positions. Even under IND-CPA, which ignores length, collision leakage would remain a distinguishing advantage because it allows the attacker to distinguish between same-length messages based on their internal equality structure. This isn't just a Shannon technicality.

"Imperfect randomness is GOOD for ZOSCII, it improves security." A non-uniform ROM (e.g., JPEG) creates larger homophone sets for common byte values and smaller sets for rare values. This helps common bytes (fewer collisions) and hurts rare bytes (more collisions). If a JPEG has 10,000 instances of a common byte but only 3 instances of a rare byte, any plaintext containing multiple occurrences of that rare byte will force address collisions almost immediately — the encoding engine has only 3 addresses to choose from.

The net effect depends on the correlation between the ROM's byte distribution and the plaintext's byte distribution. In the worst case (plaintext heavy in ROM-rare bytes), a non-uniform ROM is strictly worse than uniform. Without specifying the plaintext distribution, "improves security" is not a supportable claim.

---

What I'll Update in the Analysis

1. G5: "exposes 4 ROM bytes" → "exposes 4 ROM addresses" (values unknown without ROM)
2. G6: Withdraw formal analysis of BRAINLESS (joke/reclassification, as intended)
3. G2: Revise collision table with realistic non-uniform ROM distribution; add quantification (8 bits per collision)
4. G2: Explicitly note the Z3 proof formalizes a trivial property (functional determinism); the security argument rests on observability + Shannon, not on Z3
5. G5: Remove "session fingerprint" language; scope cross-message analysis to ROM reuse
6. G7: Scope cross-message frequency analysis to bare ZOSCII with ROM reuse; credit UNSIGNAL's genuine cross-message hardening; note intra-message structure persists within message boundaries

---

What Stands

ZOSCII does not meet the formal definition of information-theoretic security (I(M;C) = 0). Address collisions reveal 8 bits of mutual information per collision, establishing I(M;C) > 0. This is a definitional finding about what "information-theoretic security" means, not a practical attack.

Under fresh ROM, the practical significance of this finding is narrow — collision leakage is formally non-zero but near-unexploitable without side information. Under ROM reuse, leakage accumulates and the attack surface grows. UNSIGNAL substantially hardens the cross-message attack surface but doesn't affect intra-message collision structure.

ZOSCII has real, defensible properties that no other single system combines: deniable encoding, output indistinguishable from random data, no encryption format signatures, and wrong-key decoding to plausible plaintext. These properties have genuine value for covert communication, deniable storage, and surveillance resistance. The system would be stronger positioned on these properties than on an information-theoretic security claim it doesn't formally satisfy.

---

Errors on Both Sides

My errors: G5 header description (addresses, not values), BRAINLESS treated as serious, uniform ROM assumption, session fingerprint language, underweighting UNSIGNAL's cross-message defense, overstating frequency analysis practicality against UNSIGNAL, overweighting Z3 as though the proof were the argument rather than a formalization of a trivial step, not quantifying the leakage.

Your errors: "The answer is nothing" (it's 8 bits per collision — your own sentence "you just know they're the same value" is the proof), "structural pattern leakage ≠ information-theoretic leakage" (the distinction doesn't exist under Shannon), "imperfect randomness improves security" (no formal basis; depends on plaintext distribution; can be strictly worse for ROM-rare bytes).

Where we agree: ZOSCII provides real deniability properties. Fresh ROM per message is operationally sound practice. UNSIGNAL adds genuine defense-in-depth against cross-message analysis. The PRNG seed issue (now fixed) was the most practically significant finding. The system fills a niche that existing tools don't.

---

I'll update the formal analysis to reflect the corrections above. The core finding (I(M;C) > 0) is maintained with quantification and proper scoping. The practical assessment is revised to reflect UNSIGNAL's genuine contribution and fresh-ROM's practical adequacy for many threat models.

[PrimalNinja]

"These bits reveal the equivalence partition — which positions share the same byte value — but not the byte values themselves. The attacker learns the pattern, not the content." This is where I will take a slight creativity I believe in the right direction. Leakage is there if we want to be creative in that we can assume that it is a language intended for a human or human-made machine to read - or... the message itself, not the structure? There is some creativity allowed in the interpretation of I(M; C)=0 and I believe having zero leakage of the actual message itself is the key point.