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.
