はじめに ProVerifとは、INRIAが開発したセキュリティプロトコルを形式検証するツールである。この記事ではProVerifによるプロトコルの形式検証のやり方の基礎を解説する。なお、この記事では2015年10月時点での最新版であるProVerif 1.91について解説する。 この文章を読んで何か気がついたことがあったら、コメントなどで気軽に指摘して欲しい。 インストールと入手 次のようにインストールできる。また、現在はEmacs用のモードが提供されているので、Emacsも併せてインストールするといいかもしれない1。 OS X
![セキュリティプロトコルの形式検証ツール“ProVerif” - Qiita](https://cdn-ak-scissors.b.st-hatena.com/image/square/34884cd83fc948b6313c28c663f843718970192f/height=288;version=1;width=512/https%3A%2F%2Fqiita-user-contents.imgix.net%2Fhttps%253A%252F%252Fcdn.qiita.com%252Fassets%252Fpublic%252Farticle-ogp-background-9f5428127621718a910c8b63951390ad.png%3Fixlib%3Drb-4.0.0%26w%3D1200%26mark64%3DaHR0cHM6Ly9xaWl0YS11c2VyLWNvbnRlbnRzLmltZ2l4Lm5ldC9-dGV4dD9peGxpYj1yYi00LjAuMCZ3PTkxNiZoPTMzNiZ0eHQ9JUUzJTgyJUJCJUUzJTgyJUFEJUUzJTgzJUE1JUUzJTgzJUFBJUUzJTgzJTg2JUUzJTgyJUEzJUUzJTgzJTk3JUUzJTgzJUFEJUUzJTgzJTg4JUUzJTgyJUIzJUUzJTgzJUFCJUUzJTgxJUFFJUU1JUJEJUEyJUU1JUJDJThGJUU2JUE0JTlDJUU4JUE4JUJDJUUzJTgzJTg0JUUzJTgzJUJDJUUzJTgzJUFCJUUyJTgwJTlDUHJvVmVyaWYlRTIlODAlOUQmdHh0LWNvbG9yPSUyMzIxMjEyMSZ0eHQtZm9udD1IaXJhZ2lubyUyMFNhbnMlMjBXNiZ0eHQtc2l6ZT01NiZ0eHQtY2xpcD1lbGxpcHNpcyZ0eHQtYWxpZ249bGVmdCUyQ3RvcCZzPTBlOWM2YmU4NTlkNGQ1YjBhY2ZhZDgxYmRmM2JmZTNl%26mark-x%3D142%26mark-y%3D112%26blend64%3DaHR0cHM6Ly9xaWl0YS11c2VyLWNvbnRlbnRzLmltZ2l4Lm5ldC9-dGV4dD9peGxpYj1yYi00LjAuMCZ3PTYxNiZ0eHQ9JTQweXl1JnR4dC1jb2xvcj0lMjMyMTIxMjEmdHh0LWZvbnQ9SGlyYWdpbm8lMjBTYW5zJTIwVzYmdHh0LXNpemU9MzYmdHh0LWFsaWduPWxlZnQlMkN0b3Amcz1hM2FjOWY1MzAzNzlkN2Q3NjYxNjRkNjdkNmFlMjljZA%26blend-x%3D142%26blend-y%3D491%26blend-mode%3Dnormal%26s%3Df062e0b680941f4458ca8f29de04f6d9)