CPNtools協議建模安全分析（一）

       本文根據最近整理的CPNtools論文和CPNtools官網上的說明，以及參照了烏克蘭敖德薩 ---國家電信研究院運輸和通訊部關於   電信系統協議仿真關於CPNtools的學生講義。基於此和和本身的理解整理的關於CPNtools在協議建模狀態空間分析以及其餘的一些特徵。具體的介紹基於對CPNtools的工具的實際操做來講明。

       由於CPNtools是丹麥奧爾胡斯大學（Aarhus University）大學團隊開發的軟件，因此在該學院的 Department of Computer Science 部門有不少相關使用該軟件作的工做。 學院官網地址：https://cs.au.dk/  能夠在搜索欄中檢索相關的CPNtools資料

      由於考慮了一下寫的內容可能比較多，因此大致上分紅幾個章節來寫。若是後續寫的太多，我會在每一個博客作超連接到其餘博客頁面。（這項工做我會分紅大概一週時間完成）

     由於CPNtools官網上的介紹沒有針對如何建模協議來說，並且手冊部分也很簡單對作協議分析內有什麼大的幫助。因此綜合了不少材料，對CPNtool如何來建模協議模型想具體的寫點東西。算是對本身論文的一個輔助材料，凡作事必須講究認真。嚴謹的邏輯，不可捕風捉影，協議的形式化分析也必須是合乎規定，任何協議的形式化建模以前必需要根據協議組織的規範文檔來作。

第一部分：界面的功能組件的介紹

 1.1 CPNtools的安裝

     Windows安裝：在官網上 http://cpntools.org/ 上下載界面下載 基於Windows版本的最近版本 ，下載以後安裝便可

     Linux 安裝：Linux安裝以後會出現調用公用庫的 libxml2.so.2  報錯的問題，提示報錯信息：: libxml2.so.2 cannot open shared object file: No such file or directory 解決問題的方法：使用   find 命令查詢是否存在該庫， 若是存在是不是對應軟件版本和系統版本的不匹配問題， 若是沒有下載安裝便可， 若是有可是關聯存在問題，使用 ln -sf 命令 對庫文件的地址執行關聯。 具體的執行步驟見圖

      

  若是按照上面的操做仍是提示不能讀取文件，提示下面的信息：

       ./cpntools: error while loading shared libraries:  libxml2.so.2: cannot open shared object file: No such file or directory

• 、首先打開/etc/ld.so.conf文件
• 、加入動態庫文件所在的目錄：執行vi /etc/ld.so.conf，在"include ld.so.conf.d/*.conf"下方增長"/usr/local/lib"。(具體的看本身的文件庫位置)
• 、保存後，在命令行終端執行：/sbin/ldconfig -v；其做用是將文件/etc/ld.so.conf列出的路徑下的庫文件緩存到/etc/ld.so.cache以供使用，所以當安裝完一些庫文件，或者修改/etc/ld.so.conf增長了庫的新搜索路徑，須要運行一下ldconfig，使全部的庫文件都被緩存到文件/etc/ld.so.cache中，若是沒作，可能會找不到剛安裝的庫。 通常狀況下能夠解決共享庫不能加載的問題，可是有時候用戶仍是提示不能加載庫，這個時候應該考慮是不是用戶本身添加的軟件或者本身生成的 .so動態庫沒有執行權限。

  安裝完成以後操做的主界面以下。

 1.1.1 咱們先舉一個簡單的登陸協議的模型

   setp 1 首先建立兩個庫所，分別表示  Send 和 Reciver ,在建立一個變遷表示 網絡 NET

     接下來聲明顏色集合變量的類型，建模的簡單模型結構件下圖：

    

 

  step2 這裏注意，顏色集綁定的數值標記定義好以後，在變遷NEt中會自動出現，變遷的綁定初始值，這個時候咱們須要點擊變遷的左下方的小三角，來選擇須要綁定的初始值，也就是將變遷使能。變遷使能綁定初始值見下圖，這裏我麼選擇綁定(n=1,p="one")

 

step3 在弧上寫上弧表達式， 咱們定義了 var n=INT   p=DATA ， 因此從 SEND---->Reciver  弧的表達式爲 （n,p）, 這裏 從變遷NET到 Reciver端咱們 使用函數 來判斷髮送的數據。

step4 ,如今咱們來模擬數據從Send 發送到Reciver端，條件不符合的時候輸出 fail  ,條件知足的時候輸出 sucess

 

 

 

這裏咱們要注意的是幾點容易出錯的問題：

•     顏色集申明的時候 不能和 默認的（Standard declarations）中的申明重複
•     在標記顏色集的數值的時候，注意 1`(1,"shijian")++   中的符號  `  不是英文的分隔符  ’  
•     變遷的初始值綁定是根據在於其輸出的庫所中的值決定的，可是須要本身手動來綁定

我本想這將主款工具界面操做部分漢化，可是官網上不發佈 CPNtools的源代碼版本，只支持對託管源代碼的Subversion存儲庫開放。

1.1.2 tools BOX 的介紹

      我從最經常使用的工具開始介紹：

   Creat： 建立工具。  （功能介紹部分我所有放在圖像上面，這樣方便你們閱讀。）

菱形表示建立一個變遷， 橢圓表示建立一個庫所，單箭頭表示建立弧

1.2 Petri網--CPNtools 層級網絡介紹

  CPNtools最近被Nokia 被用來模型驅動的新一代手機的開發， CPN建模工具提出了強大的Petri網建模工具，一個抽象對象可使用層級網絡建模分析，簡單的（）

 

 第二部分： 原理的介紹

第三部分：簡單協議的建模舉例

第四部分：協議建模分析

第五部分：協議狀態空間分析

第六部分：協議添加攻擊模型的分析

第七部分：

參考文獻：

[1] Simonsen K I F , Kristensen L M . Towards a CPN-based modelling approach for reconciling verification and implementation of protocol models.[C]// International Workshop on Model-based Methodologies for Pervasive & Embedded Software. Springer, Berlin, Heidelberg, 2012.

[2] Yiqin Lu, Fang Fang, Runqing Quan. A simulating model of NGN based on CPN tools[M]// Theoretical and Mathematical Foundations of Computer Science. 2011.

[3]D.A.Zaitsev, T.R.Shmeleva. Simulatiing of Telecommunication Systems with CPN Tools[M]// Affiliated on meeting of Communication Networks Department Transaction NO 4 of 10.11.2006.

[4] Wells L . Performance Analysis using CPN Tools[C]// Proceedings of the 1st International Conference on Performance Evaluation Methodolgies and Tools, VALUETOOLS 2006, Pisa, Italy, October 11-13, 2006. DBLP, 2006.

[5]Kent Inge Fagerland Simonsen, Lars M. Kristensen, Ekkart Kindler. Pragmatics Annotated Coloured Petri Nets for Protocol Software Generation and Verification[M]. Springer Berlin Heidelberg, 2016.

[6]Kent Inge.Code Generation from Pragmatics Annotated Coloured Petri Nets Simonsen.[M]//

[7]https://www.cpntools.org

[8]Ole Martin Dahl. Using Colored Petri NEts in Penetration Testing