eCK模型的自動化安全協議驗證工具

我想要一個工具（在 Win7 上執行並且）可以在 eCK 安全模型中執行協議的自動驗證，如 Microsoft Research 的論文“Authenticated Key Exchange 的更強安全性”中所述。

有人知道這樣的工具嗎？

只需將我的評論包裝成答案，因為它似乎是您正在尋找的……

CryptoVerif可用於針對計算模型中的多項式時間對手驗證安全性。可通過http://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/cryptoverifbin.html獲得

與您的“它在我的電腦上不起作用”相關，這是一個如何測試它是否有效的範例（它將在 Win7 上執行 - 您之前寫過您正在使用）：

1. 在那裡創建c:\cv\並解壓縮下載包的內容。
2. 打開命令行提示符並轉到駐留c:\cv\位置。cryptoverif.exe
3. 跑cryptoverif.exe c:\cv\examples\fdh.cv

至於你關於 TEX output 的問題，它會是這樣的：

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

該手冊包含在下載包中，將為您提供其餘的命令行參數以及如何使用它的詳細說明。

這是--help參數的螢幕截圖：

編輯

有點晚了，但Scyther Tool也可能派上用場。

引用自：https://crypto.stackexchange.com/questions/10231