1、Scyther 適合分析什么樣的協議
首先協議分析工具並不是可以分析所有的協議，每種協議都有其自己適合的分析方法，並不都是可以使用形式化方法來分析。
目前協議分析方法： 模態邏輯分析（BAN邏輯，Bieber邏輯等）、定理證明分析（耗費資源）、模型檢測分析。
Scyther適合分析協議的特征：
- 參與協議的對象較少（列如：客戶端，服務端，認證端）
- 協議自身沒有使用加密、認證、過程協商。而是依托第三方加密協議
- 不支持及雙線性對和的協議分析
下圖是比較 形式化分析的工具性能的截圖（基本上可以對自己要分析的協議有一個基本的判斷之后，就可以選擇使用什么樣的工具來分析協議）
2、Scyther 如何分析一個協議
下面我簡單舉例一個單純使用加密的的簡單協議（A----->B之間的消息發送消息c，發送之前對消息單純的使用hash函數加密 ）
首先我么按照上面的描述形式化這個簡單的列子（並申明收發雙方之間可以接受到消息）------結果證明 我們形式化過程沒有問題，接受者b 和發送者 a 可以實現消息的傳遞（雙方認可）
下面我們對協議進行驗證是否存在敵手攻擊，即就是協議消息被敵手獲取的漏洞，結果證明，即便是發送的時候使用了加密函數對消息加密，敵手仍然可以獲取信息
（如圖DY模型下輸出兩個攻擊圖）
3、Scytehr 的敵手模型
Dolev-Yao模型的概念（參考資料-----《A Structured Operational Modelling of the Dolev-Yao Treat Model》）
強安全模型：敵手模型的攻擊參數可以添加 隨機數泄露、狀態空間泄露、會話秘鑰泄露等
Scyther 工具的一個好處就是 強安全模型的參數等都可以通過手動的設置選項來添加。
4、Scyther 的改進
對 Scyther的改進我們主要從兩個方面入手，
一是：界面的漢化 分析界面中所有的涉及到按鈕的標識的地方的代碼全部使用 "#coding=utf-8" 或者“ #-*- coding:utf-8 -*-” 來編譯 （具體的漢化過程不寫了，下圖是我調整了部分代碼 還沒有全部替換完 ），（看見國內一個博士漢化了 Scytehr-linux, Scyther-linux-Compromise其實漢化方法也是一樣的）
二是：添加協議分析計時器的功能
（目前還沒做完）
5、Scyther 輸出的攻擊軌跡圖分析
Scyther輸出的軌跡圖包括兩大類，一是協議分析的實例軌跡圖，另一類是在敵手模型下輸出的安全隱患的攻擊軌跡圖
先分析上面舉的例子： 圖片放小一點來看 ， 首先 我們在協議中聲明了兩個角色（分別表示客戶端A--a和 服務端B---b）,聲明了常量 函數 hash 和 unhash 並且標明了 互為反函數
為了簡單 我們只讓 a 發送一個 使用 hash() 加密的 消息 c 給 b ,並且我們在安全屬性聲明 b可以獲得 消息 c 承認接受到 。
下圖是 一個運行實例的軌跡圖 首先Run 1 中 假設 Bob 是 a 的角色代理 , b 中 Alice是 角色代理 我們 發送Bob的公鑰加密發送 消息 ，{hash(c#1)} ，顯示結果為 Alice承認 Bob發送給自己 信息。
這樣就將運行實例1 （Run1 ）d的軌跡圖描述了出來。
下面我們 看攻擊軌跡輸出的圖
6、Scyther 內部算法 Athena 的介紹
Athena算法支持多協議的並行分析、 時序相關的協議、多秘鑰設施（PKIs）模式化、多協議的多種攻擊
具體的算法分析的參考資料:Cremers C J F , Mauw S . Operational Semantics of Security Protocols[C]// International Conference on Scenarios: Models. Springer-Verlag, 2005.
scyther 使用 該算法對協議進行分析，如果在輸入協議，划分成多個主題規格，調用該算法，如果能不能搭建出安全聲明的反例，則輸出OK 反之輸出Fail
7、Scyther 形式化描述語言的SPDL的書寫規范
規范部分參見之前的博客
8、Scytehr 工具為什么最好在Linux下使用
之前在Windows下配置使用 Scyther 結果不是理想，（Wind下的首先下載對應的版本，我是在 PY上加載的文件，配置好插件之后還是會提示問題，）
要安裝支持的插件截圖見下面： 報錯的這個 包 目前無法安裝 感覺應該是版本之前不兼容問題
大家如果要使用可以將wxpython離線之后 安裝在試一試。
9、Scyther 版本 Scyther-linux 和 Scyther-linux-Compromise之間的差別在哪
兩個版本之間的差別 ： Compromise是之前的升級版，添加 了敵手的攻擊模型---->強安全模型。
10、實現加密認證的協議本身分析為什么比較難，需要攻克什么樣的問題
TLS協議時很多協議依賴的加密認證協議，整個協議的認證過程和秘鑰建立過程復雜，即便是分析清楚也要花費大量的時間。還有中間牽扯的算法要全部進行指定
13、拋開乙方加密協議我們如何快速分析甲方的協議
可以參考 《OAuth2.0 協議的安全形式化分析》
14、Scyther工具的官方網站資料
https://people.cispa.io/cas.cremers/scyther/
15、 國內工業協議形式化分析存在的問題是什么