> The state of the art is represented by: > - ProVerif (represent protocols by Horn clauses and analyzes them > doing over-approximation) > http://prosecco.gforge.inria.fr/personal/bblanche/proverif/ > - Scyther (symbolic backwards search) > http://people.inf.ethz.ch/cremersc/scyther/index.html > - Avispa (here protocols are modeled in a common language called HLPSL > and fed into four different back-end tools, each with unique > features...) http://www.avispa-project.org/ > - Casper/FDR (translate protocol models in process algebra CSP and > uses FDR model checker to provide an analysis of the translated > protocols) http://www.cs.ox.ac.uk/gavin.lowe/Security/Casper/installation.html > > So far, I've been having positive experiences with Scyther and Avispa.
I second that. In particular, I have found Avispa to be very useful. There used to be one difference between Scyther and Avispa in terms of the authentication definition, with Scyther's using a stronger one. But I think Cas mentioned he's implemented Avispa's definition now, too. Both are very good model checkers. Avispa might give you some more difficulty, I think, because it's only available as a binary for certain platforms (ia32 linux, I think). Ralph _______________________________________________ cryptography mailing list [email protected] http://lists.randombit.net/mailman/listinfo/cryptography
