安全協(xié)議理論與方法-展示頁
2025-01-22 11:39本頁面
【正文】 和generate(X)，但只能生成集合 T0中的元素 SVO邏輯語義 — 計算模型續(xù) 1 每一個行為導致狀態(tài)的一次遷移。 Si: 每個主體 Pi有一個局部狀態(tài) Si。 1) fresh(Xi) ?fresh(X1,… ,Xn) 2) fresh(X1,… ,Xn)?fresh(F(X1,… ,Xn)) 3) fresh(X)? P said X ? P says X SVO邏輯的推理規(guī)則及公理續(xù) 10 (10)I10 共享密鑰的良好對稱性公理 如果 K是 P， Q之間的良好密鑰當且僅當 K是 Q，P之間的良好密鑰。 SVO邏輯的推理規(guī)則及公理續(xù) 7 (7)I7敘述公理 一個主體說過一個級聯(lián)消息，那么它一定說 過且看到消息的每一部分。 SVO邏輯的推理規(guī)則及公理續(xù) 6 (6)I6理解公理 1) P believes (P sees F(X)) ? P believes (P sees X) 2) P received F(X) ? P believes (P sees X) ? P believes (P received F(X)) 如果一個主體理解一個消息，并看到此消息 的一個函數(shù)，那么它理解它所看到的。 SVO邏輯的推理規(guī)則及公理續(xù) 4 I4 接收公理 主體對接收到的一個級聯(lián)的加密消息可用有效的密鑰解密。它表明如果主體 Q收到一個簽名的消息，并且 Q知道簽名的驗證密鑰是 K，就可以確定發(fā)送者身份。(Q,K))?R received {X}K1 ?Q said X PK211。 SVO邏輯的推理規(guī)則及公理 1. SVO邏輯遵從兩條基本推理規(guī)則 1)??(???) ╞ ? 2) ╞ ? ? P believes ? SVO邏輯的推理規(guī)則及公理續(xù) 1 2. SVO邏輯共有 20條公理 (1)I1 相信公理 對于任一主體 P和公式 ?， ?有： 1) P believes ? ? P believes(???) ? P believes ? 2) P believes ? ? P believes ( P believes ?) SVO邏輯的推理規(guī)則及公理續(xù) 2 (2) I2源關(guān)聯(lián)公理 密鑰用于推斷消息發(fā)送者的身份。 4) P sees X, P says X, P said X, P received X 和 fresh(X)是公式 ,其中 P是主體 , X是消息。 2) 如果 ?,?是公式，則 ??和 ???是公式。 SVO術(shù)語集合續(xù) 4. 公式語言 FT： 滿足下列性質(zhì)的最小公式集合。 2) 如果 X1,…,X n是消息， F是任意一個 n維函數(shù) ,則F(X1,…,X n)是消息。 3. 消息語言 MT： 滿足下列性質(zhì)的最小語言集合。 SVO術(shù)語集合 1. 定義 T為初始術(shù)語集合 , 包括互不相交的常量符號集合：主體、共享密鑰、公鑰、私鑰以及序列號等。 2. 推理規(guī)則及公理。 3)通用語義，擴展性好，簡潔。 2)相當詳細的模型。安全協(xié)議理論與方法 基于推理結(jié)構(gòu)性方法 SVO邏輯 Syverson和 Oracho提出，建立了用于推證合理性的理論模型。 1)提供獨立明確的語義基礎(chǔ)。消除理解模糊，有助于準確理解消息的真實含義和協(xié)議理想化。 SVO邏輯的基本結(jié)構(gòu) 1. 術(shù)語集合。 3. 基于的假設。 2. n維函數(shù)表示有 n個變量的函數(shù)，如加、解密函數(shù)等 。 1) 如果 X?T，則 X是消息。 3) 如果 ?是公式，則 ?是消息。 1) 如果 P是原始命題，則 P是公式。 3) P believes ?和 P controls ?是公式，其中 P是主體， ?是公式。 5) Shared(P,K,Q),PK(P,K)和 P has K是公式，其中 P是主體， K是消息。 1) shared(P,K,Q)?R received {XQ}K?Q said X 2) (PK211。(Q,K)表示 K是主體 Q的數(shù)字簽名驗證密鑰。 SVO邏輯的推理規(guī)則及公理續(xù) 3 (3)I3 密鑰協(xié)商公理 (PK(P, KP) ? PK(P, Kq)) ? shared(P,KPq,Q)) Kpq= f(Kp, Kq1) = f(Kp1, Kq) f為密鑰協(xié)商函數(shù)，比如 DiffieHellman密鑰交換。 1)P received(X1, … , Xn) ? P received Xi 2)P received {X}K ? P has K1 ? P received X SVO邏輯的推理規(guī)則及公理續(xù) 5 (5)I5 看到公理 1)P received X ? P sees X 2)P sees (X1,… ,Xn)? P sees Xi 3)P sees X1?… ?P sees Xn ? P sees (F(X1,… ,Xn)) 主體只要接收到一個消息就看到了這個消息， 并且看到了這個消息的每一部分。 F可視為加密函數(shù)， K為參數(shù)。 1) P said(X1,… ,Xn) ? P said Xi ? P sees Xi 2) P says (X1,… ,Xn) ? P said (X1,… ,Xn) ?
教學課件相關(guān)推薦
鄂ICP備17016276號-1