《基於Scyther的祕鑰創建協議設計》-------摘抄整理

本篇論文額主要創新點：   利用Scyther軟件，經過對一個不安全的祕鑰創建協議逐步添加並驗證安全屬性，最終創建一個安全的祕鑰創建協議。

      經過形式化分析軟件設計祕鑰創建協議課能夠提升協議設計效率，減小設計者在設計過程當中的認爲錯誤，此外，該方法將協議的設計過程和協議的分析過程合成一塊兒，協議設計的終止條件取決於自動化分析工具的分析結果。所以來講，該方法設計的協議其安全性，能同時獲得形式化分析工具的驗證。

      這篇論文是比較基礎的講解Scyther工具的原理的 ----- 可是在協議形式化描述上沒有系統的講，

       那麼以前屢次重複的概念我這裏就省略不寫。

     Scyther能夠 進行多協議的並行分析，能夠分析與時序相關的協議（這一點暫時我仍是沒有碰見）、能夠進行多祕鑰設施（PKIs）模式化、能夠尋找協議的多種攻擊，

     Scyther軟件使用 SPDL語言的三種使用方法：    驗證給定的安全聲明（聲明參量的機密性或者主體的認證機密性）、自動生成安全聲明（存活性、非單射一致性、非單射同步以及數據機密性）、經過完整的特徵描述分析協議，即描述每個協議主體特徵，描述全部主體執行協議的跡，經過跡類發現潛在的危險。

      Scyther軟件圍繞的安全屬性：  機密性和 認證性。