Proving the security properties of transaction protocols - 10 years on

[dcrocker at eschertech.com (David Crocker)]

Members of this list might be interested in an article in this month's IEEE
Computer Journal about the use of automatic and semi-automatic theorem proving
to prove the security of a transaction protocol. The article - which is called
First Steps in the Verified Software Grand Challenge - concerns the transaction
protocol that was used by the Mondex electronic purse, which was developed and
formally verified (by hand) around ten years ago. Several teams have recently
attempted to apply modern tools to the problem. In the process, several of the
teams working on the project found that the original hand-developed proof was
incomplete, but could be patched.

More details can be found at
http://csdl2.computer.org/persagen/DLAbsToc.jsp?resourcePath=/dl/mags/co/&toc=co
mp/mags/co/2006/10/rxtoc.xml&DOI=10.1109/MC.2006.340#abstract . Non-subscribers
can download the article for $19.

My own company provided one of the teams working on this problem, and we found
it is quite a challenge to prove the protocol correct by fully-automatic means.
Proofs that software is free from buffer overflows for all possible inputs are
almost trivial by comparison.

Regards

David Crocker, Escher Technologies Ltd.
Consultancy, contracting and tools for dependable software development
www.eschertech.com