之前一直在懷疑我是不是因為對CPN Tools的原理結構還是不夠理解，對Petri網的還沒有弄清楚，越往后面看這種質疑越來越嚴重。 之前說CPN Tools在對稱和非對稱算法中不能形式化的問題，后續看到的文獻，雖然有對加解密做出示例，但是文獻中並沒有將如何加密和解密過程形式化，而是定義攻擊者初始知識的解密函數，函數功能只能按照 case ：k 其中k指代公鑰，而函數輸出是私鑰。其實函數的功能相當於寫了一對密鑰對 （Pk,Sk）,所以說並沒有將 一個消息如何加密輸出，和密文如何解密表達出來。這樣 對協議中存在的對稱和非對稱加密算法就不能形式化。 內蒙古大學 [1] 關於CPN Tools協議分析這方面的的論文也沒有真正定義如何實現對稱和非對稱算法。
1、ML 簡單顏色集的定義
CPN ML 提供這些簡單顏色集： Unit、 Boolean、Integer、String 、Enumerated、 Index (在CPN Tools中顏色集屬性關鍵字是小寫)
unit 顏色集包含單個元素：
colset name =unit [with new_unit] 如果沒有token 名，與顏色集名字重合。在之前的博客中寫過的灰姑娘例子中可以這樣定義：
colset p=unit with pumpkin; colset c= unit with Cinderella; colset m=uint with mouse;
boolean顏色集定義： 其值為 true 或者 false :
colset name =bool [with (new_fale, new_true)] 選擇的名字可以是 true 或者 false 。yes或者 no
colset Answer= bool with (no,yes);
Integers 顏色集定義： 是整形數字不是小數點。
colset name=int [with int-exp1... -exp3.... int.....int-expn] 將選擇的數字限定在 定義的數字間隔之間。
colset Dozen= int with 1..12; 跟隨整形變量的計算操作包括“ + - div mod abs Int.min Int.max ”
String 顏色集定義：定義字符串序列可由ASCII字符序列指定。用引號引起來。
colset name =string [with string-exp1........string-exp2] [and int-exp1....int-exp2] 指定字符的范圍
colset LowerString =with "a"...."z"; 附加在String顏色集的操作運算包括 ： -表示級聯 ， String.size ,substring
Enumerated 顏色集定義 ：在聲明中顯示標識符
colset name =with id0 | id1 | ....idn;
colset g=with rice | wheat | oat;
Indexed 顏色集定義： 索引標識由索引標識符和說明值組成序列
colset PH =index ph with 1..5;
colset FR= index fork with 1..5;
2、ML復合顏色集的定義
復合顏色集是簡單顏色集的組合。CPN 提供的復合顏色集有 ： products ,records , unions, lists, subsets, aliases
其中 lists 和 unions兩種 復合顏色集很少用到。
Products 和 records 兩種顏色集都表示笛卡爾積的數據范圍，不同之處在於 product 顏色集的組件沒有名字，而record顏色集組件由自己的名字。
product 顏色集定義：
colset name = product name1*name2*.......namen;
(v1,v2......vn) 在 1<=i<=n之間 vi的類型為 namei ,提取第 i 個 product 聲明的元素操作為：----> # i name
record 顏色集定義：
colset name = record id1:name1 * id2:name2 *........*idn:namen;
{id1=v1, id2=v2, ..... idn=vn} vi 是namei 類型的對應的值。 for 1<=i<=n .提取第 i record顏色集中的值操作： # idi name
在之前的博客中寫過定義 EtherNet幀結構的顏色集定義， EtherNet幀結構構成： Source address 、 destination address 、 data 。我們定義MAC地址為integer顏色 ，幀數據為string 顏色集
colset MAC= int;
colset DATA=string;
colset frame =product MAC*MAC*DATA;
colset frame1= record src:MAC *dst:MAC *d:DATA
這里我們也就能看出 product 和 record復合顏色集之間的差異 。EtherNet幀使用了兩種定義的方式，在實例化的時候也是不同的。如果是使用 frame 則值 X=（2,4，“Hello”） ， 相同的值在frame1中的表達方式是 x1={src=2,dst=4, d="Hello"}
提取 frame顏色集中的目標地址操作： #2 x
提取frame1顏色集中的目標地址操作： # dst x1
alias 顏色集定義：別名顏色集合之前的的顏色集有相同的屬性和值
colset name =name0
定義變量和常數：
變量是一個標識符，其值在模擬執行的時候可以改變，在Petri網中的元素銘文：
var id1 , id2 ..... idn:Cs_name ; 其中 idi 是標識符， Cs_name 是是之前定義的顏色集。我們可以這樣定義 如下：
var f1,f2: frame;
var f3, f4:frame1;
將申明的值綁定到標識符上： 使用 val id=exp; 其中 id是標識符 exp 是 CPN ML表達式， 表示一個值綁定到一個表示符上，例如：
val CheckFrame= （3,5，“Ping”）;
val ResponseFramel={src=5, dst=3, d="OK"} ；
函數的定義： CPN Tools中 只有邏輯函數，沒有更進一步的復雜運算函數。 直到目前為止我查閱的文獻中沒有關於CPN Toll三可以形式化復雜函數，像 加解密哈數和 協議中出現的對稱和非對稱算法。
新限制變量是輸出弧上的變量，沒有綁定到輸入弧和門衛上，當模型執行的時候分配一個隨機值
函數 ran 生成衣蛾隨機值，應用在大型顏色集中，
CPN Tools還提供特殊的隨機數分布函數，像我們比較熟悉的伯努利分布函數，二項式分布函數，指數分布函數，愛爾朗分布函數，泊松分布函數等，那么這些特殊的函數這里不再講了。
好現在我們就論文中出現的 如何將客戶端和服務端之間選擇密鑰材料參數算法進行建模。
文獻資料：
[1]白雲莉. 基於CP-nets模型的安全協議形式化方法研究[D]. 2014.