We’ve just submitted what I’ve been referring to as “the japanese paper”!
Written together with professor Naoki Kabayashi and his student Yunde Sun this was my first time working with Japanese people. It didn’t make a huge difference. I installed a Dashboard widget to easily show what time it was in Japan (8 hours ahead), and that was more or less it. Naoki was very polite and fair, and the whole experience has left me thinking that spending some time in Japan might not be a bad idea.
For the more technical stuff, the paper deals with how to enable a computer to automatically analyse security protocols for errors. The motivation behind this is that human designers of these protocols are notorious for missing critical details that years later allow some bad guy to do some nasty stuff. Giving these designers computer tools to verify the details is the essence of our work. The formal abstract is as follows:
Gordon and Jeffrey developed a type system for verification of asymmetric and symmetric cryptographic protocols. We propose a modified version of Gordon and Jeffrey’s type system and develop a type inference algorithm for it, so that protocols can be verified automatically as they are, without any type annotations or explicit type casts. We have implemented a protocol verifier based on the algorithm, and confirmed its effectiveness. We also formally investigate the relationship between Gordon and Jeffrey’s type system and ours.
We have submitted the paper to the Computer Security Foundations 2011 Symposium (CSF ’11) and will know whether it is accepted or not by the end of March.
Today also marks the end of a rather busy period! It’s been too much. At the level you can only keep for a short time and where physical symptoms start to show (in this case chest pains). Three sweet sweet weeks of vacation awaits me now :).