Automated security protocol verification tool for eCK model I want a tool that (runs on Win7 and) can perform automated verification of a protocol in the eCK security model as described in Microsoft Research's paper "Stronger Security of Authenticated Key Exchange". 

Does anyone know such a tool?
Just wrapping my comment into an answer as it seems to be what you're looking for…

CryptoVerif can be used for verification of security against polynomial time adversaries in the computational model. It's available via http://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/cryptoverifbin.html

Related to your "it doesn't work on my computer", here's an example how to test if it works (which it will on Win7 - which you previously wrote you're using):


create c:\cv\ and decompress the contents of the downloaded package in there.
Open a command-line prompt and go to c:\cv\ where the cryptoverif.exe resides.
Run cryptoverif.exe c:\cv\examples\fdh.cv


As for your question about TEX output, it would go like this:

cryptoverif.exe -tex somefilename.tex c:\cv\examples\fdh.cv


The manual, which is included in the download package, will provide you with the rest of the commandline parameters and a detailed description on how to use it.

Here's a screenshot of the --help parameter:



EDIT

A bit late, but The Scyther Tool may come handy too.