On Wed, May 1, 2013 at 6:50 PM, Florian Weimer <f...@deneb.enyo.de> wrote: > I'm wondering what's the state of the art here, and if there are any > formal methods for deciding if a particular protocol has certain > security properties. I know that there have been some advances in > this area, but it's sort of difficult to put together the current > overall picture.
There is no such thing as single winner among security protocols symbolic verifiers. As a matter of fact, not every tool provides support for the same set of security properties or adversary models. 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. ProVerif and Scyther are generally the fastest (see "Comparing State Spaces in Automatic Security Protocol Analysis" by Cremers C. et al). Cheers, alfonso _______________________________________________ cryptography mailing list cryptography@randombit.net http://lists.randombit.net/mailman/listinfo/cryptography
