(this post merges several previous ones.)

I attended an Informatics postgraduate course, Formal Analysis of Cryptographic Protocols during the second semester of 2006/07. The full notes from lecturer Sibylle Fröschle can be found here, but I also tried to make some more accessible summaries of my own, which subsequently found their way to E2.

I actually wrote a piece on Massey-Omura encryption before the course started, but it’s of a similar theme. The presentation is mostly in lay terms (featuring the usual cast of Alice, Bob, Eve and Mallory posting boxes to each other), but the mathematics of the three-pass system is covered towards the end. Specifically, I outline how factorisation isn’t a suitable technique but (assuming it’s as hard as everyone suspects) the discrete logarithm problem is.

My interest in this course came from a number of modules in formal logic I pursued as an undergraduate, and I’m often fascinated by ideas in this field. There are natural connections between cryptographic protocol analysis and string rewriting, and with enough freedom one can emulate general models of computation such as Turing machines by protocols. One particularly neat side effect of this is that it allows an elegant proof of the undecidability of the secrecy problem: namely, given a protocol and a secret message, is there a decision procedure to establish whether an intruder can learn the secret? By reducing to Post’s Correspondence Problem, it can be shown that the answer is no! Of course, this raises issues of intruder strength and ‘honest’ protocols; here’s the article.

Next up were a few protocols and attacks against them: Authentication sets notation and discusses one-way identity verification such as central locking for cars. The challenge-response protocol and the replay attack are included. Mutual authentication demonstrates the reflection attack on running challenge-response in both directions; three-pass mutual authentication is introduced to resolve this (at the price of some extra complexity).

Finally, I covered the type flaw attack; a particularly devious vulnerability that is invisible to many formal analytic techniques.