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 _______________________________________________ Secure Coding mailing list (SC-L) SC-L@securecoding.org List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l List charter available at - http://www.securecoding.org/list/charter.php
