Apple introduced PQ3 quantum-resistant encryption in 2024 #437829, and they're now releasing it to the public on the corecrypto repo.
For corecrypto, we use mathematical proofs to show that our algorithm implementations are correct to a significantly greater degree of assurance than conventional software testing allows. Put simply: if we can prove that the mathematical formula of our implementation is equivalent to that of its specification, then we know that our implementation will produce the correct output. In theory, this gives us strong assurance that our implementation will work correctly every time. Such a high degree of assurance generally cannot be obtained through conventional testing.
Before releasing it to the public, Apple built a formal verification method that is capable of verifying the entire algorithm implementation and able to demonstrate that each subroutine individually produces the correct output, and that the full sequence of subroutines together computes the correct final result.
Apple - A blueprint for formal verification of Apple corecrypto
corecrypto can be found here: https://github.com/apple/corecrypto
This got me interested in the algorithm itself. It would be great to hear about it from a cryptographer, but from what I gather it uses ML-KEM (a.k.a. kyber) to replace the traditional ECDH key exchange. ML-KEM is lattice based encryption, which uses a learning with errors (LWE) algorithm, which sounds cool, but is still very young in the encryption world.
So because this hasn't stood the test of time, they're using a hybrid approach. They generate a symmetric key via ML-KEM, which is then used to privately exchange traditional AES keys and encrypted data. Basically, the public key is never available to an adversary that could collect the traffic and one day have a CRQC to break it.
It doesn't seem like serious applications are ready to jump to lattice-based encryption wholesale yet. The devil you know is better than the devil you don't?
No serious implementation will optimize away 32 bytes (ecdh) on a kilobyte signature (kyber) to get half the security guarantee today. Even post q-day, it still protects against anyone that doesn't have a vacuum, absolute zero chamber the size of a small city.
Yes it seems so. Equivalent to Signals PQXDH: encapsule the conventional crypto in a hybrid setting instead of replacing it whole with the new algorithms
Only key-encryption and signatures? No hash function?
Yeah I mean thay are always late to the party, but end up stealing the show. Bert tactical and impactful. Let’s go!
Apples can make things their fruits
Respect to Apple for making the code public instead of keeping everything locked away. More eyes on crypto implementations is always good.
Curious how it holds up in real-world use outside the lab assumptions.
Apple is stoopid