Scyther 形式化分析工具資料整理（三）

一、做者Cas Cremers在作TLS1.3的時候我麼發現並無使用Scyther 形式化豐分析工具對其進行分析，而是使用了 The Tamarin 。做者創建了TLS.13的模型。 那麼個人目標是 使用Scyther工具對TLS1.2協議的握手協議和TLS1.3版本的握手協議分別進行形式化的分析。經過對比TLS1.3較以前的TLS1.2版本上的改進以後是否還存在攻擊圖輸出。或者改變TLS1.3版本協議中的消息發送的時序或者其餘工業網絡中相關的問題，在檢查是否TLS1.3版本的協議存在漏洞。

   做者對TLS1.3協議版本的形式化分析發表的相關論文：Automated Analysis and Verification of TLS 1.3: 0-RTT, Resumption and Delayed Authentication

 做者公開發表的全部文章的列表：（這裏我只挑選關於Scyther 形式化分析工具的論文資料）

 PublicationsBooks/Book chapters

1. Operational Semantics and Verification of Security Protocols 
   With S. Mauw. Information Security and Cryptography series, Springer, 2012.
2. Book chapter: Model Checking Security Protocols
   With D. Basin and C. Meadows.
   In: Handbook of Model Checking, Springer.
   [bibtex]

Conference and workshop papers

1. Abstractions for security protocol verification
   With Thanh Binh Nguyen and Christoph Sprenger.
   Journal of Computer Security, 2018. 
   
2. A Comprehensive Symbolic Analysis of TLS 1.3
   With M. Horvat, J. Hoyland, S. Scott, and T. van der Merwe.
   ACM CCS 2017: Proceedings of the 24th ACM Conference on Computer and Communications Security, Dallas, USA, 2017. 
   
3. A Formal Security Analysis of the Signal Messaging Protocol 
   With K. Cohn-Gordon, B. Dowling, L. Garratt, and D. Stebila
   IEEE EuroS&P 2017. 
   [full version (eprint)
4. On Post-Compromise Security 
   With K. Cohn-Gordon and L. Garratt.
   CSF 2016, Proc. of the 29th IEEE Computer Security Foundations Symposium, 2016. 
   [Long version] [bibtex]
5. Automated Analysis of TLS 1.3: 0-RTT, Resumption and Delayed Authentication 
   With M. Horvat, S. Scott, and T. van der Merwe.
   IEEE Symposium on Security and Privacy (Oakland), San Jose, CA, May 2016.
   [PDF] [further information and sources] [bibtex
6. 1. Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties
      With B. Schmidt, S. Meier, and D. Basin.
      CSF 2012, Proc. of the 25th IEEE Computer Security Foundations Symposium, Harvard, 2012.
      [pdf] [bibtex] [Extended version]
      Tool support: Tamarin Prover
   2. 1. Comparing State Spaces in Automatic Security Protocol Analysis
         With P. Lafourcade and P. Nadeau.
         Formal to Practical Security (LNCS 5458/2009), Springer. 
         [pdf] [bibtex] 
         Test reproduction archive containing all scripts, the used test data, and protocol description generators: [gzipped tar file]
      2. 1. Comparing State Spaces in Automatic Security Protocol Analysis
            With P. Lafourcade and P. Nadeau.
            Formal to Practical Security (LNCS 5458/2009), Springer. 
            [pdf] [bibtex] 
            Test reproduction archive containing all scripts, the used test data, and protocol description generators: [gzipped tar file]
         2. 1. Feasibility of multi-protocol attacks
               ARES 2006, Proc. of the first international conference on availability, reliability and security, Vienna, Austria, April 2006, IEEE. 
               [pdf] [bibtex]
            2. 1. Operational semantics of security protocols
                  With S. Mauw.
                  Scenarios: models, transformations and tools: revised selected papers. Dagstuhl castle, Germany, September 7-12, 2003, LNCS, Vol. 3466, 2005, Springer. 
                  [pdf] [bibtex]
               2. 以及後面的55-60。

 

二、形式化分析工具的功能差別性比較

     並非說 全部的形式都適合使用某一種形式化分析工具來作，而是每一種協議都有本身適合的分析工具進行分析。 我如今以爲仍是沒有看懂Scyther的手冊還有形式化描述的語言。Scyther是一種自動驗證協議的安全工具，

   scyther的主要特色是： 可使用無限次數的會話和隨機數來驗證協議；   能夠表徵協議，產生全部可能的協議行爲的有限表示。

   做者使用 scyther工具已經分析的協議有：

   做者一共開發了三種形式化分析的工具，分別是 Scyther  、Scyther-proof  、Tamarin

   做者說道：  對於各類對手模型的標準分析或者瞭解安全協議，可使用 Scyther 工具

                    須要機器檢查的證據使用  Scyther-proof

                    對於高級分析和尖端功能使用 Tamarin   

 貌似以前的Scyther關於安裝的 實例已經說過，此處再也不贅述。

 二、看看做者是如何在PPT中解說本身的 Operation  Semantics  這本書的概要

  爲了評估不安全的系統 ，須要定義兩個偏偏是下面的：

          安全協議：  一種鏈接方式將鏈條鏈接到自行車並鎖定的方法。

         入侵者模型：   自行車盜竊

什麼是安全 ：   安全協議的安全性要求在模型中精確的定義。

     舉個列子： 自行車完整的樣子、自行車架不能被盜竊、自行車車座不能被盜竊

從第四章開始從數學的模型開始，開發了Scyther工具  ，如何使用： 這幅圖基本上描述了

將幾個安全的協議混合在一塊兒可能獲得的不是安全的協議。