導航：安全管理網>> 安全論文>> 綜合安全論文>>正文

安全協議的規范化設計

文檔作者：鄧帆1 鄧少鋒1 張文政2 文檔來源： 1．信息工程大學信息工程學院 2．成都市現代通信國家重點實驗室		點擊數：	更新時間： 2022年04月11日
下載地址：點擊這里	文件大小： 407.48 KB 共5頁	文檔格式： PDF	下載點數： 1 點（VIP免費）

全屏查看

內容預覽 [文件共5頁]

本文件共5頁，如需編輯使用，請下載。

注：預覽效果可能會出現部分文字亂碼（如口口口）、內容顯示不全等問題，下載是正常的。

	文件大小：407.48 KB 共5頁文件格式：PDF 下載點數：1 點（VIP會員免費）

下一篇： WIFI協議安全性分析研究

上一篇：基于LEACH協議的安全節能路由算法研究

文本預覽

僅提取頁面文字內容，供快速閱讀使用。

Computer Engineering andApplications計算機工程與應用
安全協議的規范化設計
鄧帆1，鄧少鋒1，張文政2
DENG Fanl，DENG Shaofcn91，ZHANG Wenzhen92
1．信息工程大學信息工程學院，鄭州450002
2．成都市現代通信國家重點實驗室，成都610000
1．College of Information Engineering，Information Engineering University，Zhengzbou 450002，China
2．State Key Laboratory of Modem Communications，Chengdu 610000，China
DENG Fan．DENG Shaofeng。ZHANG Wenzheng．Standardized design of seeurlty protocols．Computer Engineering and
Applications。2011．47(18)：122-126．
Abstract：This paper presents a composition method of security protocol design．It gives the definition of the base case and
the component in the protocol，makes use of the components which have special security attributes to design single—step protocols
that can implement the special security goals，and defines composition rules which allow the combination of several
single-st@protocols part into a complicated protocol without destroying the security properties established by each independent
part．Then it carl design security protocol by the context of specific applications based on the choice of the single—step
protocols．In other words，the composition framework permits the specification of a complex protocol to be decomposed into
the specifications of simpler single-step protocols which OIl the components，and thus makes the design and verification of
the protocol easier to handle．
Key words：security protocol；component；logical analysis；composition
摘要：提出運用組合方法進行安全協議設計．給出了協議中基件與組件的定義，根據組件的安全屬性設計實現相應安全目標
的單步協議；定義組合規則，確保不同的單步協議能夠組合成為一個復合協議，同時各個單步協議還能實現各自的安全目標。根
據具體的應用背景選擇合適的單步協議，按照組合規則組合后可得到滿足需求的安全協議。該組合方法可將一個復合協議分解
為若干基于組件的簡單單步協議，使得協議的設計與分析易于實現．
關鍵詞：安全協議；組件；邏輯分析；組合
DOI：10．37780．issn．1002-8331．2011．18．036 文章編號：1002-833l(2011)18-0122-05 文獻標識碼：A 中圖分類號：TP309
l引言
安全協議是網絡安全的一個重要組成部分，人們需要安
全協議來提供身份標識與認證服務、授權與訪問控制服務、非
否認服務、機密性服務、完整性服務等。目前安全協議設計通
常的模式是：先采用基于經驗的、非形式化的方法設計出安全
協議，然后采用已有的分析方法對安全協議進行分析。如果
發現協議存在缺陷，則對協議進行改進，否則認為協議是安全
的。然而事實證明，許多在設計時被認為是正確的安全協議
都存在安全缺陷，甚至有些缺陷在協議投入使用多年后才被
發現。如果在安全協議設計之初就能夠保證協議的安全性，
不但可以極大地提高安全協議所在網絡應用的安全性，而且
能夠避免“設計．分析．再設計”模式帶來的大量重復性工作。
因此，安全協議設計的研究是十分有意義的。
為了解決協議設計過程中可能存在的問題，保證所設計
協議的安全性，文獻【l】在對協議缺陷進行深刻分析的基礎上，
提出了安全協議設計的一系列準則，然而設計準則對保證協
議的安全性既不是充分也不是必要的。文獻【2]提出了基于遺
傳算法和模擬退火算法的自動化協議設計方法，然而該方法
在生成復雜協議時效率較低。文獻【3】提出了應用串空間模型
和認證測試方法來指導安全協議設計，并且所設計的協議其
安全性可以直接由設計過程本身得到保證，然而該方法首先
假設協議參與方之間存在共享秘密，因而其適用范圍受到限
制。文獻【4．5】提出了模塊化設計安全協議的思想，首先在理
想環境AM下設計安全協議，然后通過UC(Universally Com．
posable Security)安全模型，將AM下安全協議轉換到實際環
境UM下便可得到所需的協議，但是沒有說明如何形式化地設
計AM下的安全協議。文獻[6．7】提出了一個用于協議導出的
形式化框架，能夠從簡單的協議成分出發，通過組合、精化和
變形等操作導出一系列協議，然而該方法不適用于對稱密鑰
算法。文獻【8】指出安全協議之間可以進行組合，在UC安全模
基金項目：通信技術重點實驗室基金(NO．9140C1103040902)。
作者簡介：鄧帆(1980一)，男。碩士，研究領域為安全協議設計與分析；鄧少鋒(1984一)，男，碩士；張文政(1960一)，男，研究員。總工。E-mail：
windcctvl23456789@163．o咖
收稿日期：2009-11-02；修回日期：2009．12-29
萬方數據
鄧帆，鄧少鋒，張文政：安全協議的規范化設計
型下證明了任意兩個安全協議組合后仍然是安全的。
本文提出應用組合方法進行安全協議設計。針對對稱環
境下的若干組件，運用SPALL(Security Protocol Analysis Latent
Logic)邏輯分析了這些組件所具有的安全屬性，同時基于
這些組件設計了與其對應的若干單步協議。定義了單步協議
的組合規則，通過選擇合適的單步協議按照組合規則組合后
便可得到所需協議，最后以對稱環境下的安全認證協議和安全
密鑰協商協議為例說明如何運用該方法漫計安全協議。與文
獻is．11】中的其他組合沒計方法相比，本文提出的方法特點：
(1)所定義的組合規則簡單可靠，組合規則不影響單步協
議安全目標的實現，同時可以保證單步協議能夠組合成為復
合協議。
(2)指出組件作為協議的基本組成部分，對組件的形式化
分析可以從協議底層開始保證協議能夠實現安全目標，減少協
議可能存在的安全隱患，使安全協議的設計與分析都易于實現。
(3)適用于不同初始假設的多種環境。本文方法的關鍵
在于對具體環境下組件安全屬性的正確分析，對初始假設的
環境無特別要求。
2應用組合方法設計安全西漢
判斷一個協議是否安全，其本質就是考察協議所期望的
安全目標是否都能達到。傳統的設計方法將所有安全目標作
為—個整體，然而，要找到—個協議能同時滿足所有安全目標
并不是一件容易的事。隨著安全目標的增加，找到一個滿足
條件的安全協議將更加困難。為解決此問題，本文提出了應
用組合方法進行安全協議設計，步驟為：(1)定義基件的概念，
如用戶A、B，A生成的隨機數Ⅳ。，4和B的共享密鑰足．。
等被稱為基件，單個基件是不具有任何安全屬性的。將基件
進行組合后可得到組件，如【彳，M】邑。，組件是協議中具有安
全屬性的基本單位。(2)對不同的組件進行分析，得出一定環
境下單個組件所具有的安全屬性，如：B收到A產生的組件
似，M}后回復組件【A，M】E。給A，則A’認證了占的身份，即
組件[彳，Ⅳ．】t。具有認證屬性。將分析后的組件進行合理組
合，可得到能實現相應安全目標的單步協議。如基于組件
M，H】髟口的單步協議為：A--*B：A，M；占一彳：口，M，虬】巧B，
該單步協議實現了A認證B身份的安全目標。(3)定義組合規
則使單步協議通過組合可得到新的協議，然后根據具體的應
用背景和需求選擇合適的單步協議按照規則進行組合后得到
滿足需求的安全協議。這種組合方法設計協議，將協議的安
全目標分散為多個子目標由不同的單步協議實現，組件作為
協議的基本組成部分，在保證單步協議達到對應安全目標的
同時也從底層保證了協議能達到預期的安全目標，這比將所
有安全目標作為—個整體來設計協議容易得多。組合規則的
使用使協議設計過程有了規范，避免了單純基于經驗或抽象
的設計原則設計協議容易造成的安全隱患，確保了協議能夠
實現所期望的安全目標。
該方法還有兩個主要優點：(1)協議設計易于實現。協議
安全目標能否實現依賴于單步協議是否能實現其安全目標。
而單步協議的安全目標是由其所基于的組件所決定的，保證
單個細件具有某些安全屬性比保證協議實現安全目標相對容易
實現。(2)協議安全性易于分析。協議安全目標的實現是由組件
的安全屬性、單步協議的安全目標決定的。因此，在分析協議的
安全性時，可以g．t底層的組件開始分析，然后分析單步協議的
安全性，這比綜合分析整個協議的安全性相對更容易。
3基礎知識
SPALL(”1邏輯是一種新的BAN類邏輯，它把BAN類邏輯
置于數理邏輯這一理論基礎之上，使BAN類邏輯進一步理論
化、系統化，同時省去了理想化過程，避免了理想化過程帶來
的許多問題。SPALL邏輯的公理可靠，使用簡便。
3．1 SPALL邏輯的基本命題符號
記所有消息的集合為三，3表示所有時戳的集合，Ⅳ表
示所有隨機數的集合。簡單命題爿的否定記作一，A并且
曰，記為A^口，如果A那么口記為彳j口，彳當且僅當曰記為
彳付曰。如果】，是由x和其他比特串級聯而成或者就是x，
則稱y包含了X，并記作y=廈柳。用(x--y)表示從l，中可
以恢復出x。由9和@·∽可直接得到||f，，該規則稱為分
離規則，簡記為MP。
PgX表示P生成了x，P司Z表示尸看見了z，x卜尸
表示x是給P的，&amp;amp;(一表示P正在參與執行協議的通信。
Pj曰表示P意定的通信對象是B，Pl；X表示P相信x是
真的，PI—X表示P說過X，群(20表示x是新鮮的，KI_-->P
表示足是P的公開密鑰，PB表示P和曰共享秘密x。
【硼x表示足加密x所得密文，PI毫0(棚表示x對于戶來說
具有雙向可追溯性。所謂雙向可追溯性，是指消息x由確定的
主機給出，由合法的接收者接收。PI*X表示PI～x^撐(加，
稱為尸剛剛說過x。
3．2 SPALL邏輯的公理及定理
本文所用到的公理及定理均來自文獻[12】，所用的編號也
與該文獻相同。此處列出了將用到的一部分公理或定理，更
多請參考原文獻。
(1)新鮮性公理AFM(Axiom about Fresh Message)
a)AFM2撐p㈣一撐(．D
(2)身份認證公理AlP(Axiom about the Identity of Partieipator)
a)越P2 PI-3(QI≈X^XEΣ)_PI￡&amp;amp;(Q)
b)AP6(XeΣ^PI-z>-Q)一PjQ
(3)信宿公理AMD(Axiom about Message Destination)
a)AMD4醐卜P專X卜P
(4)滟鼠生成公理AMG(Axiom about Message Genemtion)
a)AMGl P3X->妒liz∈ΣAPIio(抑)
b)AMG2 x∈3UⅣ一(P3x_PIi撐∽)
(5)ASP(Axiom about See Predicate)
a)ASP2 P司廈．D．-4PQ，P|毫●Pj閑幻，PImXeΣ}_
PI．OI-x
b)TSD3{P<】r>Q，尸．日日(以以】，)，Pl--p(X)eΣ，PI--
萬方數據
124 2011。47(18) ComputerEngineeringandApplicationsi'f．算機工程與應用
—(P弓日(從以y)))一PI-QI—x
c)TSD6 PI=-X∈Σ—÷(Pl=QI一廈的—'PI；QI～．聊
(8)關于信宿的定理TMD(Themem about Message Deliver)
a)TMDl{P司【加KP<足>Q，Pl；一P弓Ⅸ】幻，PI=-X∈B—
PI§X>-P
b)1加B{PQ，尸司日(五Y),PI---XeΣ，_1(P弓壩五y))}寸
PI；．r卜P
4基件與組件
協議的運行是通過協議消息的交換來完成的，本文定義
基本消息與基件的概念如下：
定義1(基本消息)下列4種消息稱為基本消息：(1)協議
實體標識，D。如A、B等代表用戶，S代表服務器或管理中
心。(2)密鑰K。K代表各實體的公鑰、私鑰、會話密鑰、共享
密鑰等。(3)亂數Ⅳ。協議實體在協議運行期間產生的臨時
值，如隨機數Ⅳ。，時戳L等。(4)數據消息D。實體之間通過
協議傳送的信息。
定義2(基件)基本消息和密碼函數統稱為基件。常見的一
些密碼函數：(1)Hash函數Hash(．)。(2)簽名函數S／GH(·)。
此處為研究方便，將簽名函數表示為[·】K～，足。1為用戶私
鑰。(3)加密函數【×Ⅸ，K為加密密鑰。
組件通過下列三種操作產生：(1)級聯操作。兩個或多個
基件通過級聯操作后可得到一個組件。如A和Ⅳ．是兩個基
件，級聯后形成{A，Ⅳ。}便是—個組件。(2)密碼函數操作。如
彳、M、Hash(．)是基件，H(A，M)便形成—個組件。(3)混合操
作。組件與組件、組件與基件之間通過級聯、密碼函數的混合
操作而形成新的組件。
5對稱環境下安全協議組件的安全屬性分析
5．1基本假設
在分析協議組件的安全屬性時，假定所用的基件都是安
全的。如選取的隨機數不發生重復，用戶間的共享秘密未發
生泄漏，用戶所使用的密鑰、所采用的Hash函數和加密函數是
安全的等等。只有在這些基本假沒下保證了基件的安全，討論
組件的安全屬性才是有意義的。
5．2組件的安全屬性分析
通過對對稱環境下大量協議的歸納總結，得到了如下一
些對稱環境下協議中的經典組件(其中髟。表示A、B雙方的
共享對稱密鑰)：(1)gl，：日∞，虬，髟≯，該組件的背景為：A
產生隨機數Ⅳ．后發送組件似，Ⅳ。}給口，曰收到后回復組件
蜀，給A，(2)92．：M，M】％，該組件的背景為：彳產生隨機數
M后發送組件塒，M}給曰，曰收到后回復組件92。給彳。
(3)93。：【彳，B，M，髟一髟。，該組件的背景為：A產生隨機數
M，A、S雙方共享對稱密鑰K。。，s收到組件{A，B，M}后
回復組件毋．給A。(4)94。：M，心一l】髟。，該組件的背景為：彳
產生隨機數Ⅳ。后發送組件{彳，Ⅳ。)給B，8收到后回復組
件飄，給A。(5)爵：【彳，M，虬】髟。，該組件的背景為：A產生
隨機數Ⅳ。，口產生隨機數％，口收到組件臼，Ⅳ。}后回復組
件95。給A。(6)96。：[日(彳，虬，巧p】巧口，該組件的背景為彳
生成隨機數虬，曰收到組件{A，M)后回復組件&amp;amp;，給彳。
(7)97，：lib，％】巧1】髟。，該組件的背景為曰生成隨機數％，
巧1為彳的私鑰，彳收到組件{曰，％}后回復組件島。給曰。
下面運用SPALLj星輯對組件H(B，虬，髟0進行分析(初
始假設簡記為BAS)：
(1)A<％>丑BAS
(2)A3虬BAS
(3)A司覷口，也，蚴’BAS
(4)aj．-ta H(B，M，％)) BAS
(5)以∈N BAS
(6)4懌虬∈三(2)AMGI
(7)糾s撐∽) (2)，(5)AMG2
(8)a[-(B，以，K朋)eZ(3)ATM4
(9)OH(B，M，‰)∈三(3)ATM4
(10){(1)，(3)，(4)，(9)}斗4卜口卜p，以，巧p TSD3
(11)AI-BI-s BAS
(4)爿j也BAS
(5)_t-SA-Z(4)AMGI
(6)AI"岸(M) (4)AMG2
(7)爿|；“，B，心，髟≯∈三(2)ATM3
(8){(1)，(2)，(3)，(7))_al-sl-(A，B，也，蚴TSDI
(9)a1．sl-<_，B，M，蚴(8)MP
(10)al-sl-(彳，B，M，xo呻彳l；sl～也TSD6
(11)OSI-N』(10)MP
(12)“l；sI一心^一l；撐(Ⅳo)—}彳IzsI*虬符號“I~”的定義
(13)彳l；sI*也(6)，(11)，(12)MP
(14)AI．SI*N』斗一I；＆∞ AIP2
(15)al---＆∞ (14)MP
(16){(1)，(2)，(3)，(7)}哼
Al-=(a．B．NpK0>-A TMDI
(17)AI-(A，B，M，‘曲卜一(16)MP
萬方數據
鄧帆，鄧少鋒，張文政：安全協議的規范化設計
(Is)(07)^(9))_彳IzSj一
(19)A[=-SjA
(20)A司似，B，Ⅳ^，¨
(21)Aq％
(22)一Iz撐僻o
(23)AI．SI-K』,
(24)彳I暑K曲卜彳
AlP6
(18)N口
(7)ATMI
(20)ASP2
(6)，(20)AFM2
(9)TSD6
(17)A～n34
(25)似f；s卜^o^4卜j％卜田一一卜暑o(心≯符號“I；o’’的定義
通過上述分析可知，該組件所具有的安全屬性描述為：
糾；&amp;amp;∞Alffi-S=A，A司巧口，彳I；撐(髟。)，彳Iso(髟。)，即該組件
所具有的安全屬性為彳認證了s的身份。S分配密鑰髟。給
彳，并保證了密鑰的機密性、新鮮性。
。其膨腫睬用米1出滯．力法哪融Ⅱ下結論：(1)92，：叫，以】孟％，
該組件所具有的安全屬性為A認證了曰的身份。(2)94，：
M，Ⅳ．一1]KA。，該組件除了可進行身份認證外，還可以用于驗
證密鑰的正確性。(3)95，：阻，M，心】髟。，該組件所具有的安全
屬性為4認證曰身份的同時傳遞了隨機數以，并保證了心
的機密性和新鮮性。(4)甌．：[日似，M，髟塒‘。，該組件所具有
的安全屬性為A認證曰身份的同時可進行數據完整性校驗。
(5)97，：[陋，％】巧1】髟。，該組件所具有的安全屬性為曰認證
了A的身份，保護了數據完整性。同時對A來說具有非否認性
以及匿名性。根據組件安全屬性分析的結果，可設計與其對應
的單步協議如下：(不難看出，采用與分析組件安全屬性的類似
方法可證明單步協議的安全目標與組件的安全屬性是一致的。)
(1)glI舊(口。M，髟≯ M4一B：A，虬
(2)912：片(爿，^0，巧p
(3)92I私，川】％
(4)如：陴，虬】％
(5)93I：M，B，也，^oj％
(6)932：陋，A，％。％】^，囂
(7)94I：口，M—l】如
(8)94r'[B，％一l】％
(9)95l：弘，虬，W％
00)gs2：陋。％，Wj％
(11)＆。：【日似，心，％)】j％
(12)962：[H(B。％。蚴】‰
(13)97l：[陋，^啊髟1】如
(14)972：[[A，M】巧'足0
M28_A：B。H(B，N^，X0
N、B_A：B，NB
NlA_B：A，H(A。Ne’K0
MIA—B：A。N^
鴆口一彳：B“A，也】％
NIB●A：B，N|
Ⅳ2A_口：4，陋，ⅣB1％
MA-+S：A，B，心
鴆s_一：S，M，B，圯，x一_％
NL8一s：B．A，Nl
MS·B：S，疆，A。N B’K心KBs
MtA呻B：A，N^
鴆口一一：B，似，虬一l】K0
NlB-)A：B．NB
Ⅳ2彳斗口：A，陴，％一l】‰
MA_丑：A，以
鴆口_彳：B，叫，心，虬1％
ⅣI口_爿：B，％
Ⅳ2■_丑：一，【B，心，M】％
MA_口：A，M
鴆曰o■：口，【日似，M，巧p】j％
NlB崎A：B。NB
Ⅳ2A-+B：A，【川且心，¨】Ji，仰
MB啼』：口，％
塢彳—'占：A，【【占，w巧1】J【0
ⅣIA．+口：A，虬
也口_彳：B，時，NAlX；1‰
6對稱環境F安全協議的設計
6．1組合規則
利用單步協議設計安全協議時，首先要根據具體的背景
和需求選擇合適的單步協議。在選取單步協議時需遵循以下
原則：(1)選取應用環境相符的單步協議。如安全協議的應用
背景為對稱環境，則只能選擇對稱環境下的單步協議，并根據
安全協議需要達到的安全目標來選擇相應的單步協議。(2)選
取安全目標相容的單步協議。選取單步協議只和P，進行組
合時必須保證單步協議P；的安全目標不會影響到單步協議
只的安全目標。也就是說，基于組件&amp;amp;的單步協議只實現安
全目標的I司時，基于組件蜀的單步協議只也能實現其安全目
標。(3)規范所選單步協議的符號表示。如P；中用Ⅳ。表示彳
生成的隨機數，那么只中不能再使用M表示占生成的隨機
數，以免混淆。
正確選擇完單步協議后，需定義單步協議的組合順序。
假定P。={只，P2，?Pj代表基于組件的一系列單步協議的集
合，這些單步協議能達到的安全目標是由其基于的組件的安
全屬性所保障的。P為單步協議組合后得到的安全協議，即
P=P，0P2 o?0P．。各單步協議進行組合時必須遵守某
個順序用D(P)表示。記e為協議中的運行動作，如果協議消
息分別為P，：M，鴆；P，：Ⅳ1，Ⅳ2。那么每個發送消息的步驟即
為一個動作，即動作有dM)’“心)，P(Ⅳ1)'d^協0(尸)=dM)<
d蚴<反Ⅳ1)></足>

網友評論 more

綜合安全論文最新內容

04-10