Analysis of Origin and Destination Authentication The analysis of origin and destination authentication is implemented in Standard ML of New Jersey (ML) and uses the Succinct Solver as a solving back end.

Software Analysis of Origin and Destination Authentication (version 1.1). February 10, 2004. Copyright. Changes.

Documents D19: Static Analysers (version 1.1). February 10, 2004 Documentation of the ML implementation. Implementing Control Flow Analysis for Security Protocols. Draft of October 1, 2003. Describes the technical development behind the implementation including an appendix on asymmetric cryptography. Note that current version is a first draft.

Comments are much welcomed and should be send to Mikael Buchholtz.

Last updated February 18, 2004 by Mikael Buchholtz