安全協議理論與方法(ppt 60頁)

安全協議理論與方法目錄：
一、SVO術語集合
二、SVO術語集合續
三、SVO邏輯的推理規則及公理
四、SVO邏輯語義—計算模型
五、SVO邏輯語義—公式成立的條件
六、SVO邏輯的應用實例
七、SVO邏輯-ZG證明假設

安全協議理論與方法內容提要：
Syverson和Oracho提出，建立了用於推證合理性的理論模型。
提供獨立明確的語義基礎。
相當詳細的模型。消除理解模糊，有助於準確理解消息的真實含義和協議理想化。
通用語義，擴展性好，簡潔。
SVO術語集合：
定義T為初始術語集合, 包括互不相交的常量符號集合：主體、共享密鑰、公鑰、私鑰以及序列號等。
n維函數表示有n個變量的函數，如加、解密函數等。
消息語言MT：滿足下列性質的最小語言集合。
1)如果X?T，則X是消息。
2)如果X1,…,Xn是消息，F是任意一個n維函數,則F(X1,…,Xn)是消息。
3)如果?是公式，則?是消息。
4. 公式語言FT：滿足下列性質的最小公式集合。
1)如果P是原始命題，則P是公式。
如果?,?是公式，則??和???是公式。
P believes ?和P controls ?是公式，其中P是主體， ?是公式。
P sees X, P says X, P said X, P received X 和fresh(X)是公式,其中P是主體, X是消息。
Shared(P,K,Q),PK(P,K)和P has K是公式，其中P是主體， K是消息。

..............................