The Secrecy Problem

May 3rd, 2007

I took a number of interesting modules in formal logic 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; I’ve written up some of these ideas (along with the proof and an outline of PCP) over on e2.

Leave a Reply