安全協(xié)議理論與方法-在線瀏覽
2025-02-17 11:39本頁面
【正文】 P says Xi SVO邏輯的推理規(guī)則及公理續(xù) 8 (8)仲裁公理 P controls ? ? P says ? ?? SVO邏輯的推理規(guī)則及公理續(xù) 9 (9)I9新鮮公理 如果消息的一部分是新鮮的，那么整個消息 也是新鮮的。 shared(P,K,Q) ?shard(Q,K,P) SVO邏輯的推理規(guī)則及公理續(xù) 11 (11) I11所有公理 P has K ? P sees K SVO邏輯語義 — 計算模型 Pe： 代表環(huán)境 ,可用于模擬攻擊者的任意行為 。 全局狀態(tài) : n+1維局部狀態(tài)。 r: 一輪協(xié)議 r是一個由整數(shù)時間索引的全局變量的有限集合。 ri(t): 對應(yīng)的主體 Pi的局部變量記為ri(t)。 SVO邏輯語義 — 計算模型續(xù) 2 主體 Pi在 (r,t)收到的消息集合包括： 1) 局部消息歷史中或 t之前出現(xiàn)的 received(X)中的 X。 3) P持有所收到的加密消息 {X}K的解密密鑰，則 P可得到 X。 2)主體新近生成消息集。 4)主體通過規(guī)則和公理從已知的消息集衍生的消息集。 SVO邏輯語義 — 計算模型續(xù) 4 主體 Pi在 (r,t)發(fā)送的消息集合包括： 1)主體對已發(fā)送過消息的級聯(lián)。 3)簽名密鑰為主體所持有的簽名消息的非簽名部分，且此部分為主體所看到。 SVO邏輯語義 — 公式成立的條件 定義： ?將每一個常量命題 p?T映射為點集?(p), 即命題 p為真的點。 ╞ ? 意味著 ?全真。 (r,t) ╞ ??? iff(r,t) ╞ ? ?(r,t)╞ ?。 SVO邏輯語義 — 公式成立的條件 2 (2)原始命題 1) 接收命題 (r,t) ╞ p received X 當(dāng)且僅當(dāng) X屬于主體 P在 (r,t)時已收消息集合。 (r,t) ╞ p has X 當(dāng)且僅當(dāng) X屬于主體 P在 (r,t)時已收消息集合。 SVO邏輯語義 — 公式成立的條件 5 4)仲裁命題 (r,t)╞ p controls ?， 當(dāng)且僅當(dāng) (r,t)╞ p says ?且對于所有的 t’0, 有： (r,t) ╞ ?。 SVO邏輯語義 — 公式成立的條件 7 6) 四種密鑰命題： 共享密鑰 公開加密密鑰 公開簽名密鑰 公開協(xié)商密鑰 SVO邏輯語義 — 公式成立的條件 8 共享密鑰？？ (r,t’) ╞ R received{X}K 或者 R?{P,Q}。 SVO邏輯語義 — 公式成立的條件 10 公開簽名密鑰 (r,t) ╞ PK?(P,K)當(dāng)且僅當(dāng)對于所有的 t’， (r,t) ╞ Q received {X}K1，則表明 (r,t) ╞ P said X。(P,K)當(dāng)且僅當(dāng)對于所有的 t’： 對于某些 Q， Kpq=f(K1, PK211。(R))以及 (r,t’) ╞?goodkey(P,Kpr,R) 且對于所有 U， Kur=f(PK211。1(R))且 (r,t’) ╞?goodkey(U,Kur,R)。則 不大可能會出現(xiàn)否認(rèn)性。收費后否認(rèn)收費或者因質(zhì)量問題而否認(rèn)發(fā)貨。 SVO邏輯的應(yīng)用實例續(xù) 1 Schneider 在下列文獻(xiàn) 中運用通信順序進(jìn)程CSP對一個 不可否認(rèn)協(xié)議實例進(jìn)行了形式化的描述與分析。 用 SVO也可對不可否認(rèn)性進(jìn)行分析。 二是借助一個可信第三方 (TTP)。 NRR(Nonrepudiation of Receipt):收方不可否認(rèn)。 NRD:(Nonrepudiation of Delivery): 傳遞不可否認(rèn) ,證明 TTP已交付給了意定接收者，由 TTP提供。 NRO= SA(fNRO,B,L,C) NRR= SB(fNRR,A,L,C) NRS_K= SA(fNRS,B,L,K) NRD_K= STTP(fNRD,A,B,L,K) SVO邏輯 不可否認(rèn)協(xié)議實例分析 定義 不可否認(rèn)協(xié)議的公平性： 是指從協(xié)議執(zhí)行的開始到協(xié)議執(zhí)行結(jié)束的任何一個階段，通信的雙方要么能夠同時得到它們所期望的，要么任何一方都得不到有利于自己的信息，從而避免協(xié)議的任一方中斷執(zhí)行的協(xié)議，或否認(rèn)其已發(fā)生的行為以達(dá)成利益不平等的可能。 2)在協(xié)議結(jié)束時提供主體參與協(xié)議行為的證據(jù)，即證據(jù)的有效性。 A1: 每個主體的公鑰是公開的。 A3: TTP believes SA A4: TTP believes SB A5: P believes STTP:P 為參與協(xié)議運行的主體 A6: TTP believes (B received C)?TTP believes (A said C) SVO邏輯 ZG證明假設(shè)續(xù) A7: A said (A,B,L,Ek(M)) ? A said (A,B,L,K) ? A said M A8: B received (A,B,L,Ek(M)) ? B received(A,B,L,K) ? B received M A9: TTP believes (A said C ? B received C ? TTP received K) ? TTP
教學(xué)課件相關(guān)推薦
鄂ICP備17016276號-1