At the heart of modern cyber security is mathematics, and mathematics is a subject where formal proofs matter. Many aspects of cyber security are asserted and find their way into common usage, but often formal proofs follow a long way behind, or are never actually produced. Now, a formal proof of some security scheme does not guarantee that it is secure, but it does go along way towards doing so.
One area in which I am particularly interested is anonymity based systems. Most people think of Tor when the subject is raised. However, anonymity is vital in a number of schemes. One example is electronic voting where your vote must be cast in secret but, ideally, be verifiable. A classic example is the Pret A Voter system.
Tor uses a method called “decryption mixes”, since layers of cipher text are shed as the onion makes its way to the receiver - just like a Russian Doll.. These (and how they apply to e-voting systems) have been studied a lot in recent years. However, there is another form called "re-encryption mixes" which has been incorporated in various systems but is less well studied.
I'd not seen a formal analysis of re-encryption mixes until this week. The paper I read was entitled "Semantically Secure Anonymity: Foundations of Re-encryption".
The paper starts by demonstrating that, to date, these schemes have not had a satisfactory definition of security, despite its use in various important applications. The researchers then analyse the ElGamal-based universal cryptosystem and show that it has not been proven to be anonymous under Decisional Diffie–Hellman (DDH) assumption. More surprising the researchers cryptanalyse the security foundation of the ElGamal-based incomparable public key cryptosystem and appear to show that it is not proven to be secure (this has long been one of the bases for "proving" the security of ElGamal ie if the decisional Diffie–Hellman assumption (DDH) holds in G then ElGamal achieves semantic security.)
Now, showing that something is not proven to be secure is not the same as saying it is insecure, but it does ring a few alarm bells. None of this is what we had all previously thought, proving that even long held assumption at the heart of some security schemes can be overturned by formal analysis.
The paper goes on to not just highlight the problem(s) but also to suggest a provable secure universal re-encryption algorithm. They also suggest a modification to the DDH proof technique used by many to date, which allows them to show the security of ElGamal, and which they then use to prove their own new forward-anonymous scheme.
This paper was a timely reminder that assumptions need to be challenged, and when you do so through formal mathematical proofs you often uncover inconsistencies in systems where those assumptions have become taken as proven fact. Security is a discipline where the devil is in the detail, and that detail requires a lot of study if the devil is not to pop up at the most unexpected moments.
