0. 源代码地址
代码的GitHub链接
https://github.com/cascremers/scyther
这个项目的README.md里有部分安装教程，还有一个Scyther的安装使用文档链接，但是这里有一个坑点，这两个安装说明之间存在冲突。
Scyther安装使用文档链接
https://people.cispa.io/cas.cremers/scyther/
原页面都是英文，截图的时候我用了页面翻译，所以有的地方不是特别准确
问题就出在Python版本上，做为两个方法都折腾过的人，表示Python3真的不行。
1. 环境安装
我的环境使用的是Ubuntu16，使用的是安装使用文档中的安装方式，但是并不能像安装文档说的，一条指令结束就可以运行，还需要再装一些别的插件。
sudo apt-get install graphviz python-wxgtk3.0
2. 代码下载解压
代码下载这个版本的，注意这个版本和GitHub上下载的版本略有差异
两个版本一个是Python3，一个是Python2，而Ubuntu自带的Python版本是2.7（顺便说一句，centos7的自带版本也是2.7）
解压（别在下载路径里直接解压了，给它挪个地方）
tar zxvf scyther-linux-v1.1.3.tgz
如果按照安装教程，这个时候就可以运行了，尝试运行一下会出现如下报错
仔细看这里的报错都指向wx，这是Python的一个库，也就是需求里的wxPython库，这个需要单独安装。
打开页面里的那个链接
https://www.wxpython.org/pages/downloads/
执行安装指令
pip install -U \
-f https://extras.wxpython.org/wxPython4/extras/linux/gtk3/ubuntu-16.04 \
wxPython
出现报错pip未安装，我是找了一个比较新的虚拟机从新截图记录安装步骤的，所以很多东西都没有。
3. pip安装
首先尝试按照提示安装
sudo apt install python-pip
然后再重复安装wxPython，下着下着就会超时中止，并提示pip版本低。
按照它的提示来
sudo pip install --upgrade pip
会出现新的错误
没关系还有救
wget https://bootstrap.pypa.io/pip/2.7/get-pip.py
如果因为网络问题这次下载提前中断，记得去本地把下载失败的文件删除，不然就会像这样，它并不覆盖原路径，而是在后边加一个.1，再正常执行指令的时候就会报错。
sudo python get-pip.py
这时候查看pip的版本会发现直接查不到了，明明前面已经显示successfully的，因为系统是从默认路径找的，但是pip现在不在默认路径下。
which pip
type pip
hash -r
pip --version
然后再执行wxPython的安装指令，它又报错了……
可以看到是gtk找不到了，安装gtk
4. gtk安装
sudo apt-get install libgtk2.0-dev
sudo apt-get install libgtk-3-dev
5. wxPython安装
现在终于可以安装wxPython了。
pip install -U \
-f https://extras.wxpython.org/wxPython4/extras/linux/gtk3/ubuntu-16.04 \
wxPython
到这里wxPython安装好了，但是如果现在试图运行会发现又出现了报错
仔细看提示，还是出在wx的使用上。
在wxpython4中，SplashScreen小部件不再位于wx.SplashScreen中。它在wx.adv.SplashScreen
6. 修改代码
在scyther-gui.py的140行加上
from wx import adv
把141行的wx改为adv
修改前：
修改后：
7. 运行
./scyther-gui.py
就会出来这个欢迎界面
关掉后是使用界面——的半成品
和官方文档中的图片一比就知道，它少了一行菜单栏，没有这行菜单栏图形界面实际上是完全无法使用的，因为运行就是要点菜单栏的“Verify”。
我之前试图克服这个问题，然后勉强测出来还是wx的问题，可能还是因为版本更新，有的函数不兼容了。由于毕竟使用的时候还是通过命令行执行，而且我的Python学的就跟压根不会一样，我选择及时放弃。
8. 命令行执行
Scyther的使用方法，和spdl的语言规范官方文档里有，我自己也上传了一份，省的以后再去找了
Scyther使用文档
https://download.csdn.net/download/mandiheyanyu/85660198
在Scyther路径下有个scyther-linux
调出帮助文档
./scyther-linux --help
Usage:
scyther [switches] [FILE]
Switches:
-d, --dot-output show patterns in dot format
-x, --xml-output show patterns in XML format
--filter=<protocol>[,<label>] check only certain claims
-a, --auto-claims ignore any existing claims and automatically generate claims
Switches that affect the state space:
-r, --max-runs=<int> maximum number of runs in patterns [5]
--unbounded Do not bound the number of runs in patterns
-A, --all-attacks generate all attacks within the state space instead of just one
Misc. switches:
--license show license
-h, --help show short help
--long-help show long help
-o, --output=<FILE> output file [stdout]
--append-output=<FILE> append output file [stdout]
FILE input file ('-' for stdin)
There are two environment variables that influence the behaviour of the Scyther command-line tool.
SCYTHERFLAGS Put any default command-line options here, syntax as on the command line.
SCYTHERDIR Colon-separated path of directories to search for input files if a file
is not found in the current directory. Note: use '$HOME' instead of '~'.
代码就有个ns3.spdl，可以拿来测试。
./Scyther/scyther-linux --dot-output --output=ns3-attacks.dot ns3.spdl
会产生这么一个新文件。
渲染输出文件。
dot -Tpdf -O ns3-attacks.dot
有几个Fail就会生成几个pdf。
随便打开一个看看，大约是这个样子的。
一些高级参数请比照scyther-linux --help出来的那个帮助文档，我就不写了。
相关链接
Scyther形式化验证工具简单教程
https://blog.csdn.net/qq_42450533/article/details/117512538
Scyther tool 入门
https://www.cnblogs.com/xinxianquan/p/11398445.html