余 磊

（淮北師范大學 計算機科學與技術學院，安徽 淮北 235000）

0 引言

安全協(xié)議是建立在密碼體制上的一種消息交互協(xié)議，它運用密碼算法和協(xié)議邏輯來實現(xiàn)身份認證、密鑰分配、數(shù)據(jù)共享等安全目標，是網(wǎng)絡空間中各種安全服務與應用的主要載體. 網(wǎng)絡應用對安全協(xié)議功能需求的增加，使得安全協(xié)議的知識體系一直在不斷地擴展與壯大. 網(wǎng)絡空間安全一級學科的增設［1］，以及信息安全專業(yè)課程體系的持續(xù)優(yōu)化和發(fā)展，為系統(tǒng)全面地覆蓋安全協(xié)議的知識體系，“網(wǎng)絡安全協(xié)議”已成為高校信息安全本科專業(yè)的主干課程［2］.

受安全屬性需求的多樣性、協(xié)議運行的高并發(fā)性、消息組織結構的復雜性、網(wǎng)絡環(huán)境的開放性等因素影響，設計一個既沒缺陷也無冗余的安全協(xié)議是一件非常復雜和困難的事情［3］，安全協(xié)議在投入使用之前必須運用已有的方法和經(jīng)驗對其進行正確性分析. 形式化方法已被證實是當前最為科學、嚴謹、有效的安全協(xié)議正確性分析方法［4］. 在網(wǎng)絡安全上升為國家戰(zhàn)略的時代［5］，安全協(xié)議發(fā)揮著愈來愈重要的信息安全保障作用，掌握并熟練運用一種安全協(xié)議形式分析方法，已成為信息安全本科專業(yè)人才培養(yǎng)規(guī)格的基本要求［6］.

在眾多的安全協(xié)議形式化分析方法中由于認證測試模型在協(xié)議分析上具有方法簡潔、邏輯嚴謹、科學有效和形式化程度較高的優(yōu)點，被廣泛用于安全協(xié)議的分析和設計中［7-8］. 近年來，經(jīng)過眾多研究人員不斷地擴展、優(yōu)化和完善，認證測試模型在安全協(xié)議分析上已具有較為成熟的理論和方法體系，成為安全協(xié)議形式化分析方法的典型代表. 在“網(wǎng)絡安全協(xié)議”課程的知識體系和實踐能力體系設置上，都對認證測試模型的相關知識點進行覆蓋，認證測試模型理論已是“網(wǎng)絡安全協(xié)議”的教學重點［9］. 由于認證測試模型理論涉及到代數(shù)學、圖論、密碼學、邏輯學和計算機語言學等多門學科內(nèi)容，具有知識構成復雜、概念深奧抽象的特點，對學生的知識遷移運用能力要求較高；加上現(xiàn)有的認證測試理論缺乏對測試組件的密碼學性質(zhì)和結構性質(zhì)的深入剖析，導致學生在認證測試模型的概念理解和方法應用上很難把握到位，從而成為形式化分析方法的教學難點.

關于認證測試模型研究的現(xiàn)有文獻顯示，偏重理論擴展和方法應用的科研文獻頗豐［10-11］，鮮見從教學角度對認證測試理論模型相關概念和性質(zhì)深入解讀和探討. 為提升認證測試模型理論的教學效果，本文結合實際教學經(jīng)驗，以經(jīng)典的安全協(xié)議為實例，從消息組件、測試組件、認證測試模型結構3個方面給出一些教學注記，以幫助學生更好理解認證測試模型理論，消除在概念理解及方法應用上的一些誤區(qū).文中涉及串空間模型理論的相關概念請參閱文獻［12］，本文不再給出.

1 消息組件

消息組件是構成協(xié)議消息的基本信息單元，是協(xié)議分析和缺陷定位的主要對象. 在消息組件概念的理解上，容易混淆消息組件與消息子項、新組件與消息起源，造成概念理解錯誤和使用不準確.

定義1設t為消息項，若t不能分解成級聯(lián)類型形式，則稱t為簡單項.

定義2設n為結點且sign（n）=+，t為term（n）的消息組件.（1）若對于任意前驅(qū)結點n′?+n，t都不是n'的子項，則稱t是源發(fā)于n.（2）若消息項t在協(xié)議的串空間中有且僅有一個源發(fā)結點，則稱t是唯一源發(fā)的.

定義3設t0，t為消息項，t0為簡單項且t0?t. 若所有滿足子項關系t0t1?t和t1≠t0的消息項t1只能為級聯(lián)類型，則稱t0為t的消息組件.

定義4設n為結點，t為term（n）的消息組件. 如果對于任意前驅(qū)結點n′?+n，t都不是n′的消息組件，則稱t是結點n上的新組件.

圖1 Denning-Sacco協(xié)議

注記1消息組件的類型只能為原子類型或加密類型.

任何攻擊者都有能力對級聯(lián)類型的消息進行拆分、重構等操作，破壞消息構成和結構次序以達到攻擊目的，而這些操作對簡單項是無效的，所以消息組件是協(xié)議正確性保障的重要基本信息單元. 在圖1的m2=ABS{BkABT{AkABT}kBS}kAS中，則m2只包含A、B、S、{BkABT{AkABT}kBS}kAS4 個消息組件，AB、ABS、S{BkABT{AkABT}kBS}kAS等級聯(lián)類型都不是m2的消息組件.

注記2消息的簡單子項并不一定是消息組件.

在m2=ABS{BkABT{AkABT}kBS}kAS中，{AkABT}kBS并不是m2的消息組件. 如果{AkABT}kBS是m2的消息組件，則在m2中存 在 {AkABT}kBS?{BkABT{AkABT}kBS}kAS?ABS{BkABT{AkABT}kBS}kAS子項關系，根據(jù)定義2，{BkABT{AkABT}kBS}kAS并不是級聯(lián)類型，所以{AkABT}kBS并不是m2的消息組件.

注記3結點n的新組件并不一定源發(fā)于結點n.

新組件的定義中沒有對結點的符號進行限制，所以消息項t是結點n的新組件，但t并不一定源發(fā)于n. 在圖1 中，m3的消息組件{AkABT}kBS為term()= -ABS{BkABT{AkABT}kBS}kAS的新組件，由于sign(sA,2)=-，{AkABT}kBS不是源發(fā)于結點，根據(jù)定義2可知，才是其源發(fā)結點.

2 測試組件

測試組件體現(xiàn)的是協(xié)議主體對消息組件的加工運算能力，是認證測試模型的核心，是實現(xiàn)協(xié)議安全屬性和協(xié)議功能的基礎. 原有認證測試理論缺乏對測試組件的組成要素、參數(shù)類型，以及協(xié)議主體角色的分析，在概念理解上容易給學生造成一些誤區(qū).

定義5設a為原子消息項，n為結點，t={h}k為term（n）的消息組件. 如果：（1）a是h的消息組件；（2）t不是協(xié)議串空間中任意其它常規(guī)結點消息組件的真子項，稱t是a在結點n中的測試組件.

注記4測試值、加密秘鑰和測試主體標識是構成測試組件的三要素，其中測試主體標識具有顯性和隱性兩種形式.

要借助測試組件實現(xiàn)對協(xié)議主體身份合法性的測試，則測試對象、唯一代表測試對象合法身份的信息、信息加工的載體三者缺一不可，這三者在測試組件中分別被形式化為測試主體標識符、加密秘鑰和測試值. 根據(jù)定義5，從測試組件t={h}k的結構形式上，只能看出測試值a?h和加密秘鑰k兩個要素，在測試組件的概念中也沒有體現(xiàn)測試主體標識這個要素. 這是因為測試主體在測試組件中具有顯性和隱性兩種形式. 在圖2 的m1={NaA}kB中，A?{NaA}kB，主體A的身份標識是以顯性形式存在m1中的. 在m2={NaNb}kA中，A并不是m2的子項，主體A的身份是以隱含形式存在測試組件的加密秘鑰kA中的.kA為A的公鑰，與主體A的身份存在一一對應關系，只有擁有的主體才能對{NaNb}kA進行運算.

圖2 Needham-Schroeder協(xié)議

如何提取隱含在測試組件中的協(xié)議主體標識，結合文獻［11］中主體身份標識符概念，可給出主體身份標識提取方法的法則.

推論1設t={h}k為測試組件，X，Y為協(xié)議主體，id(t)為t的主體標識符集合.（1）若X?h，則X∈id(t)；（2）若sXY?h，sXY為X和Y的共享秘密，則X,Y∈id(t)；（3）若k=kXY，kXY為X和Y的共享秘鑰，則X,Y∈id(t)；（4）若k=kX或分別為X的公鑰和私鑰，則X∈id(t).

根據(jù)注記4和推論1，圖2中的3個消息m1、m2、m3都滿足測試組件的條件，可以確定m1的三要素為(Na,kB,{A,B})，m2的三要素為(Na,kA,A)或(Nb,kA,A)，m3的三要素(Nb,kB,B).

注記5并不是所有主體標識都是測試主體標識，測試主體標識只包含挑戰(zhàn)主體標識和響應主體標識.

測試主體代表的是測試組件的信源和信宿，在協(xié)議安全目標實現(xiàn)過程中起到關鍵保障作用. 根據(jù)測試主體在測試組件中的地位和角色，認證測試模型中把驗證主體稱為挑戰(zhàn)主體，把被驗證主體稱為響應主體，測試主體標識也就相應地分為挑戰(zhàn)主體標識和應答主體標識. 當一個協(xié)議包含多個協(xié)議主體時，在測試組件除含有挑戰(zhàn)主體標識和應答主體標識，還含有其它協(xié)議主體標識，這些主體標識只起到數(shù)據(jù)共享的輔助作用，并不影響測試組件的安全屬性，可稱這些主體為協(xié)商主體. 如在圖1 的m3=AB{AkABT}kBS中，根據(jù)定義5，id({AkABT}kBS)={A,B,S}，m3中包含著A、B、S3個主體標識，其中A為挑戰(zhàn)主體標識，S為應答主體標識，B是協(xié)商主體標識. {AkABT}kBS的三要素為(T,kAB,{A,S}).

注記6測試組件的加密秘鑰必定隱含響應主體標識.

在測試組件{h}k中，假設a?h為測試值，挑戰(zhàn)主體只能基于測試值a，通過響應主體在k或k-1上運算的唯一性來判斷響應主體的合法性，即響應主體與k或k-1存在一一對應關系，所以響應主體的身份標識必然隱含在k中. 在圖2中的m1，由于主體B的公鑰kB是公開的，與A不存在一一對應關系，B無法通過{NaA}kB上的加密運算實現(xiàn)對A的合法性測試. 由于只屬于主體B，所以A可以通過對{NaA}kB的解密運算驗證B的合法性，所以{NaA}kB的響應主體為B，這與B隱含在秘鑰kB中是一致的.

由注記6可得出性質(zhì)1.

性質(zhì)1設t={h}k為測試組件，如果X是隱含在k中唯一主體標識符，則X一定是響應主體標識.

根據(jù)性質(zhì)1，可以判斷圖2中的消息組件m2和m3的響應主體分別是A和B.

3 認證測試結構

根據(jù)測試方式的不同，認證測試模型分為出測試、入測試和主動測試3種類型，相應的3個認證測試理論主要用于安全協(xié)議的認證性分析，認證性分析是通過參數(shù)一致性判斷來實現(xiàn). 當運用認證測試定理對協(xié)議進行參數(shù)一致性分析時，證明過程較為復雜，且不直觀，學生難以掌握和運用. 協(xié)議的參數(shù)一致性、認證性和保密性之間關系復雜，概念把握不準容易造成協(xié)議分析結果錯誤.

定義6設結點n1和n2滿足n1?+n2，消息項t1、t2分別為n1和n2的消息組件，且t2為n2的新組件，消息項a滿足a?t1∧a ?t2.（1）若sign(n1)）=+，sign(n2)=-，則稱n1?+n2為a的被轉換邊；（2）若sign(n1)=-，sign(n2)=+，則稱n1?+n2為a的轉換邊.

定義7設邊n1?+n2為a的被轉換邊，t={h}k是a在結點n1中的測試組件，KP為攻擊者秘鑰集合. 如果a唯一源發(fā)于結點n1，且k-1?KP，則稱n1?+n2是a在t上的出測試.

定義8設邊n1?+n2為a的被轉換邊，t={h}k是a在結點n2中的測試組件，KP為攻擊者秘鑰集合. 如果a唯一源發(fā)于結點n1，且k?KP，則稱n1?+n2是a在t上的入測試.

定義9設消息t={h}k是消息項a在結點中的測試組件，sign（n）=-，KP為攻擊者秘鑰集合. 如果a在串空間中是唯一源發(fā)的，且k?KP，則稱結點n是a在t上的主動測試.

注記7認證測試模型基于的是挑戰(zhàn)與應答結構，主動測試是入測試的一種特殊情況.

認證測試模型的核心思想是協(xié)議的一方借助測試值向另一方發(fā)起消息運算挑戰(zhàn)，然后根據(jù)對測試值的運算反饋，來判斷另一方的存在性和身份的合法性，所以整個認證過程就是測試值的挑戰(zhàn)與應答過程. 在認證測試模型中稱發(fā)起測試值運算挑戰(zhàn)的一方為挑戰(zhàn)主體，接受測試值運算挑戰(zhàn)的一方為響應主體. 在認證測試3種模型的定義和定理中，只有出測試和入測試中存在挑戰(zhàn)與應答結構，但主動測試比較特殊，結構中只存在應答不存在挑戰(zhàn). 這主要是因為主動測試的測試值不同于出測試和入測試，出測試和入測試的測試值是由挑戰(zhàn)主體生成的，而主動測試的測試值是測試主體雙方共享的，一般為時間戳，所以在主動測試結構中就缺省測試值的挑戰(zhàn)步驟，從形式上好像是響應主體主動發(fā)起的認證測試，顧名思義，把這種結構叫做主動測試模型. 如果把測試值共享看作協(xié)議主體發(fā)起的隱性挑戰(zhàn)，則主動測試其實就是入測試的一種特殊情況.

注記8測試組件參數(shù)是判斷協(xié)議一致性的主要依據(jù)，測試組件的參數(shù)可以分為測試主體標識參數(shù)、新鮮值參數(shù)、秘鑰參數(shù)和協(xié)商數(shù)據(jù)參數(shù)4種類型. 非加密秘鑰和協(xié)商主體標識為協(xié)商數(shù)據(jù)參數(shù).

運用認證測試模型的3個定理對安全協(xié)議進行分析時，最終歸結到挑戰(zhàn)主體與響應主體在串參數(shù)的一致性判斷上，測試組件的參數(shù)正是串參數(shù)一致判斷的核心依據(jù). 根據(jù)測試組件中參數(shù)的功能和作用，可以把測試組件的參數(shù)分為測試主體標識參數(shù)、新鮮值參數(shù)、秘鑰參數(shù)和協(xié)商數(shù)據(jù)參數(shù)4種類型. 測試主體標識參數(shù)決定參與測試的協(xié)議主體是誰；新鮮值參數(shù)主要為測試值，其主要作用是標識協(xié)議運行的輪次和確保測試組件的新鮮性，防止重放攻擊和協(xié)同攻擊；秘鑰參數(shù)確保響應主體串的唯一性和數(shù)據(jù)的保密性；協(xié)商數(shù)據(jù)參數(shù)輔助協(xié)議實現(xiàn)特定的功能和安全目標. 非加密秘鑰和協(xié)商主體標識只起到數(shù)據(jù)共享和信息輔助作用，不是測試組件的核心要素，屬于協(xié)商數(shù)據(jù)參數(shù)范疇. 在圖3 中邊?+既是Na在{NaMAB}kAS中的出測試，又是Na在{NaNbkab}kAS中的入測試. 在測試組件{NaMAB}kAS中，由于id(kAS)={A,S}，{A,S}為測試主體標識參數(shù)，Na為新鮮值參數(shù)，kAS為秘鑰參數(shù)，{M,B}為協(xié)商數(shù)據(jù)參數(shù).在{NaNbkab}kAS中，{kab,Nb}為協(xié)商數(shù)據(jù)參數(shù).

圖3 Amended Otway-Rees協(xié)議

由注記4、注記6和注記8可得性質(zhì)2.

性質(zhì)2挑戰(zhàn)主體通過測試組件能夠確認與響應主體在秘鑰參數(shù)、新鮮值參數(shù)和響應主體標識參數(shù)上達成一致.

由注記4可知，秘鑰參數(shù)、新鮮值和測試主體標識參數(shù)為測試組件的三要素. 由注記6可知，響應主體標識一定隱含在測試組件中. 所以挑戰(zhàn)主體一定與響應主體在秘鑰參數(shù)、新鮮值和響應主體參數(shù)具有一致性.

根據(jù)性質(zhì)2，在圖3 的m4中，主體A通過{NaNbkab}kAS能確認與S在串參數(shù){A,S,Na,kAS}上具有一致性.

注記9主動測試的測試值并不一定是時間戳，也可以是能夠確認當輪協(xié)議運行具有新鮮性和唯一性的隨機值.

主動測試一般用于分析測試值為時間戳的認證測試結構. 在協(xié)議運行系統(tǒng)的時鐘同步機制上，時間戳可以用來保證消息的新鮮性，防止消息重放攻擊. 由于時間戳的共享省略測試值的傳遞過程，所以在協(xié)議設計中常?；跁r間戳來實現(xiàn)協(xié)議主體身份的主動認證，如圖1中的m2和m3. 但主動測試的測試值并不全部基于時間戳的，如果能夠使協(xié)議主體確認其它數(shù)據(jù)在當輪協(xié)議中的新鮮性和在串空間中的唯一性，也可作為測試值用于構建主動測試. 在圖3的m4中，可信主體S通過把Nb與Na在{NaNbkab}kAS中的綁定，使得主體A可以通過Na的新鮮性來確認Nb的新鮮性，從而使得結點成為Nb在{Nb}kAB中的主動測試. 為確保高并發(fā)運行環(huán)境中消息的新鮮性，有的協(xié)議中同時使用隨機值和時間戳，如圖4m1中的Ta和Na，m2中的Tb和Nb.

圖4 CCITT X.509協(xié)議

圖5 NSPK協(xié)議的內(nèi)部攻擊

注記10測試組件的三要素只能確保協(xié)議滿足弱一致性，當且僅當在挑戰(zhàn)主體標識和協(xié)商數(shù)據(jù)上滿足一致性時，才能確保協(xié)議滿足強一致性，弱一致性不能保證協(xié)議的認證性.

設A，B為某一認證協(xié)議的兩個通信主體，若A要實現(xiàn)對B身份的認證，根據(jù)認證邏輯［15］，當A收到B發(fā)送的認證消息m時，A不僅知道m(xù)是B發(fā)送的，還要知道是針對自己發(fā)送的. 放在認證測試模型中，只有挑戰(zhàn)主體標識和響應主體標識同時包含測試組件中，才能確保挑戰(zhàn)主體對響應主體的正確認證. 即只有挑戰(zhàn)主體與響應主體在挑戰(zhàn)主體標識、響應主體標識、新鮮值和密鑰參數(shù)上達成一致性，協(xié)議才滿足認證性. 如果挑戰(zhàn)主體還能進一步與響應主體在協(xié)商數(shù)據(jù)上滿足一致性，則協(xié)議滿足強一致性.弱一致性容易遭受來自協(xié)議內(nèi)部的協(xié)同攻擊，無法保證協(xié)議的認證性. 圖5為NSPK協(xié)議的內(nèi)部攻擊叢圖，I為內(nèi)部攻擊者，冒充A向B發(fā)起身份認證，A可以通過測試組件{NaA}kI能實現(xiàn)對I的正確認證，但是B無法通過測試組件{NaNb}kA實現(xiàn)對A的正確認證. 導致NSPK存在攻擊的主要原因是，{NaNb}kA

中缺少挑戰(zhàn)主體B的標識符，B與A不能在挑戰(zhàn)主體標識符B上達成一致.

由性質(zhì)2可知，挑戰(zhàn)主體通過測試組件只能確保與應答主體在響應主體標識，新鮮值和密鑰參數(shù)上具有一致性，而不能確保在挑戰(zhàn)主體標識和協(xié)商數(shù)據(jù)上的一致性，故測試組件的三要素只能確保協(xié)議的弱一致性.

4 結論

認證測試模型的上述教學注記既涉及到概念的剖析和性質(zhì)挖掘，又涉及到方法的優(yōu)化和萃取. 對測試組件的組成要素、參數(shù)類型和主體角色的深入剖析，進一步加深學生對認證測試模型結構性質(zhì)和密碼學性質(zhì)的理解. 對消息子項與消息組件、新組件與消息起源、顯性主體標識和隱形主體標識、挑戰(zhàn)主體與應答主體、時間戳與隨機值、一致性與認證性、認證性和保密性等概念關系的辨析，可以消除學生在概念理解和方法應用上存在的誤區(qū)，提高認證測試模型概念使用的準確性和方法應用的嚴謹性. 對串參數(shù)一致性判斷方法、協(xié)議認證性分析方法、認證測試結構判斷和設計方法的優(yōu)化，以及對主體標識符提取方法、協(xié)議保密性分析方法的擴展，讓認證測試方法變得更加簡潔、具體和直觀，讓學生更加易于理解、掌握和運用，能夠有效提升認證測試模型的教學效果.