Trees, hashes and Lean

Most of the week went into researching VCVio's[1] capabilities and what exactly I'd need to do on the security-analysis part of my project.

Lean 4[2] is quite a no-brainer for getting a machine-verifiable proof of logic correctness, which is similar to invariant testing when we're making an assumption based on what the logic does not do, and what the proven boundaries are.

In earlier posts I described the separation of cryptographic primitives across the DKSAP implementation, but in short it would be: key exchange (which is settled as FIPS 203[3] and Kyber ML-KEM) and signatures, which are both FIPS 204[4] and FIPS 205[5] (Dilithium and SPHINCS+).

For the key exchange we'd be looking to prove the boundaries and identity correctness. Spending stays outside of this project proposal and is considered an implementation detail.

When reading Ethereum's point of view on the PQ roadmap[7], it made sense to me to also consider different mechanisms for the key exchange, which were mentioned in the original paper[6] but were not that efficient — they could serve the useful purpose of having alternatives if an attack vector were discovered on Kyber/ML-KEM.

Also, recently I saw a dev update from the EF's PQ team, and it seems like the Poseidon competition[8] has been there for a while and it's time to settle what to do with it.

While thinking about alternative ways to do a key exchange, I can't stop thinking of using some sort of tree for authentication and note discovery. Especially considering the fact that Dr. Merkle did a PhD at Stanford under Martin Hellman, and the Diffie-Hellman key exchange could've been the Diffie-Hellman-Merkle key exchange.

Not that NIST approval says a lot, but Merkle constructions over SHA-3 are considered PQ-secure. Grover halves the 256-bit preimage security, keeping roughly 128-bit preimage resistance.

Next week I'll tinker around and see if there is anything useful for us. While 5564[9] may remain unchanged and is designed to be very future-proof, the Stealth Meta-Address Registry[10] would need to be reconsidered, because the contract includes an ECDSA recovery right inside of it.

So hypothetically, if we changed the registry implementation to something abstract, like storing a root somewhere, we could play around with indexing speed, and it might be a greater fit for EIP-8304[11] to also make the discovery process trustless and persistent as long as the state exists on Ethereum.

I did a small detour and worked on exploring Merklized Poseidon leaves with significantly cheaper registry writes

upd 15.8: this one didn't age well — Poseidon is not considered anymore in favor of SHA-2/BLAKE-family hashes

Next week for me is fully dedicated to research on VCVio and Lean 4.