楊京，范丹，張玉清

（1.西安電子科技大學(xué) 綜合業(yè)務(wù)網(wǎng)理論及關(guān)鍵技術(shù)國(guó)家重點(diǎn)實(shí)驗(yàn)室，陜西 西安710071；2. 中國(guó)科學(xué)院大學(xué) 國(guó)家計(jì)算機(jī)網(wǎng)絡(luò)入侵防范中心，北京 100190；3. 中國(guó)科學(xué)院 信息工程研究所 信息安全國(guó)家重點(diǎn)實(shí)驗(yàn)室，北京 100093）

1 引言

目前，安全協(xié)議的形式化分析方法大致可以分為3類：形式邏輯方法、模型檢測(cè)方法和定理證明方法[1]。其中，模型檢測(cè)方法也稱作狀態(tài)空間搜索法。模型檢測(cè)技術(shù)采用形式化方法精確地證明一個(gè)系統(tǒng)能夠按照預(yù)定目標(biāo)正確工作。模型檢測(cè)的基本思路是把安全協(xié)議看成一個(gè)分布式系統(tǒng)，而每個(gè)主體執(zhí)行協(xié)議的過程構(gòu)成局部狀態(tài)，所有的局部狀態(tài)則構(gòu)成系統(tǒng)的全局狀態(tài)，每個(gè)主體的消息接收和發(fā)送動(dòng)作都會(huì)引起局部狀態(tài)的改變，進(jìn)而引起全局狀態(tài)的改變，因此需要在系統(tǒng)可達(dá)的每個(gè)全局狀態(tài)，檢查其安全屬性是否滿足文獻(xiàn)[2]。對(duì)于安全協(xié)議分析來講，模型檢測(cè)技術(shù)已被證明是一條非常成功的途徑。首先，這種方法的自動(dòng)化程度高，在驗(yàn)證過程中不需要用戶參與；其次，如果協(xié)議存在缺陷，能夠自動(dòng)產(chǎn)生反例。但因?yàn)槿菀桩a(chǎn)生狀態(tài)空間爆炸問題，所以模型檢測(cè)方法不能用于比較復(fù)雜的安全協(xié)議分析。

雖然存在以上缺點(diǎn)，但由于模型檢測(cè)方法能夠?qū)崿F(xiàn)自動(dòng)化，這種方法得到很多研究人員的關(guān)注，并做了許多相關(guān)工作。Clark等[3]通過使用偏序歸約技術(shù)削減驗(yàn)證過程的狀態(tài)空間；Shmatikov等[4]通過規(guī)定在合法主題可以發(fā)送消息時(shí)，攻擊者就不發(fā)送消息，來實(shí)現(xiàn)削減狀態(tài)空間；Broadfoot等[5]通過把可信第三方的通信順序進(jìn)程合并到攻擊者進(jìn)程來削減狀態(tài)空間；Hui和Gavin[6]先把復(fù)雜協(xié)議轉(zhuǎn)換成簡(jiǎn)單協(xié)議（簡(jiǎn)單協(xié)議能夠體現(xiàn)復(fù)雜協(xié)議的安全缺陷），然后再利用模型檢測(cè)方法來分析復(fù)雜的安全協(xié)議；Stoller[7]提出一種決定攻擊一個(gè)協(xié)議時(shí)所需協(xié)議實(shí)例的上界的方法；Roscoe等[8]通過使用數(shù)據(jù)獨(dú)立技術(shù)，給出實(shí)現(xiàn)攻擊有用的隨機(jī)數(shù)數(shù)目的上界。

鑒于普通模型檢測(cè)方法對(duì)于存在漏洞的協(xié)議，需人為修正或重新設(shè)計(jì)，這種處理方式不僅效率低下，而且嚴(yán)重依賴于經(jīng)驗(yàn)，容易引入新的漏洞。安全協(xié)議自適應(yīng)模型檢測(cè)（adaptive model checking）方法[9]借鑒可以實(shí)時(shí)更新模型的自適應(yīng)技術(shù)將安全協(xié)議的設(shè)計(jì)過程與分析過程統(tǒng)一起來，根據(jù)反例自動(dòng)修正初始模型，并以此改進(jìn)和優(yōu)化安全協(xié)議。與現(xiàn)有的密碼協(xié)議分析和驗(yàn)證方法相比，安全協(xié)議自適應(yīng)模型檢測(cè)方法最大的優(yōu)勢(shì)在于，當(dāng)驗(yàn)證出協(xié)議漏洞或需求發(fā)生變化時(shí)，可以對(duì)協(xié)議初始模型進(jìn)行自適應(yīng)的更新。

安全協(xié)議自適應(yīng)模型檢測(cè)框架如圖 1所示。首先對(duì)安全協(xié)議（密碼協(xié)議）建模，即編碼實(shí)現(xiàn)，利用模型檢測(cè)工具（model checker）對(duì)其進(jìn)行模型檢測(cè)，檢測(cè)結(jié)果若為安全（safe）的，則終止（terminate）；否則返回反例（counter-example），可給出圖形化結(jié)果（attack graph），也可調(diào)用exe文件和cmd窗口，將結(jié)果保存為xml文件，再對(duì)xml文件進(jìn)行解析和處理，提取出反例。把反例轉(zhuǎn)換成字符串并將其輸入自動(dòng)機(jī)學(xué)習(xí)算法工具學(xué)習(xí)，以修正安全協(xié)議初始模型。模型檢測(cè)工具使用Scyther或者AVISPA/Span、spin、nusmv等。在該框架中學(xué)習(xí)算法起著非常重要的作用，它使安全協(xié)議的模型檢測(cè)過程形成一個(gè)閉環(huán)。因此，學(xué)習(xí)算法的選取顯得尤為重要。

圖1 安全協(xié)議自適應(yīng)模型檢測(cè)框架

自動(dòng)機(jī)學(xué)習(xí)算法相關(guān)文獻(xiàn)提出了許多種學(xué)習(xí)算法，例如機(jī)器學(xué)習(xí)相關(guān)的蟻群優(yōu)化算法[10]、遺傳算法、基于SAT求解器的算法、IVAP算法[11]。新的算法層出不窮，而安全協(xié)議自適應(yīng)模型檢測(cè)中最實(shí)用的學(xué)習(xí)算法是基于 L*學(xué)習(xí)算法[12]的一些算法，將自動(dòng)機(jī)學(xué)習(xí)算法用于修正協(xié)議初始模型。本文介紹了L*學(xué)習(xí)算法及其相關(guān)算法，描述了自動(dòng)機(jī)如何通過反例來學(xué)習(xí)目標(biāo)語(yǔ)言。基于L*學(xué)習(xí)算法的一系列算法包括推斷確定型自動(dòng)機(jī)（如文獻(xiàn)[13]中的 Lm+算法等）和非確定型自動(dòng)機(jī)（文獻(xiàn)[14]中的NL*，文獻(xiàn)[15]中的L*nm等）的多種算法。

考慮實(shí)際場(chǎng)景：復(fù)雜的安全協(xié)議發(fā)送者、接收者、入侵者、加解密、認(rèn)證等狀態(tài)繁多；在許多應(yīng)用場(chǎng)景中，一個(gè)老師可能并不能回答某些成員資格詢問，因?yàn)橐獙W(xué)習(xí)的對(duì)象不是完全具象的，是不可觀察的或者要回答這些提問所付出的代價(jià)是非常高昂的等，所以這些詢問可能是懸而未決的。然而，當(dāng)前的學(xué)習(xí)算法顯然不能滿足日益復(fù)雜的安全協(xié)議，有必要對(duì)其進(jìn)行改進(jìn)。

本文提出一種改進(jìn)的安全協(xié)議自適應(yīng)分析算法，即修正學(xué)習(xí)算法La*，對(duì)L*學(xué)習(xí)算法做了2方面的修正，一方面字母表可以是大字符集（無窮的或不可枚舉的），引入符號(hào)自動(dòng)機(jī)，并將觀察表擴(kuò)展為符號(hào)觀察表；另一方面對(duì)老師做了修正，將最小勝任教師(MAT，minimal adequate teacher)推廣至缺乏經(jīng)驗(yàn)的老師（inexperienced teacher）。修正學(xué)習(xí)算法將有助于提高安全協(xié)議自適應(yīng)模型檢測(cè)的效率、降低分析和設(shè)計(jì)成本、緩解狀態(tài)空間爆炸并增強(qiáng)協(xié)議本身對(duì)環(huán)境和各種攻擊手段的自適應(yīng)防御能力。

2 預(yù)備知識(shí)

2.1 確定型有窮接受器

首先介紹的自動(dòng)機(jī)是操作確定的有窮接受器，這種類型的自動(dòng)機(jī)特點(diǎn)是沒有臨時(shí)存儲(chǔ)。因?yàn)檩斎胛募豢筛膶懀杂懈F自動(dòng)機(jī)在計(jì)算過程中所能記住的東西是相當(dāng)有限的。通過把控制部件放在某一個(gè)特殊狀態(tài)上，自動(dòng)機(jī)可以把有限的信息保存到這個(gè)控制部件中。但是由于這種特殊狀態(tài)是有限的，有窮自動(dòng)機(jī)只能處理這種情況，即每一時(shí)刻可以存儲(chǔ)的信息都是有嚴(yán)格限制的[16]。下面給出精確的形式化定義。

定義1確定型有窮接受器（DFA, deterministic finite accepter）是一個(gè)五元組M=(Q，Σ，δ，q0，F(xiàn))其中，Q是內(nèi)部狀態(tài)（internal states）的有限集合，Σ是符號(hào)的有限集合，叫做輸入字母表（input alphabets），δ：Q×Σ→Q是一個(gè)全函數(shù)，叫轉(zhuǎn)移函數(shù)（transition function），q0∈Q是初態(tài)，F(xiàn)?Q是終態(tài)集合。

每個(gè)有窮自動(dòng)機(jī)都接受某種語(yǔ)言，如果考察所有可能的有窮自動(dòng)機(jī)，就獲得了一個(gè)和這些自動(dòng)機(jī)相關(guān)的語(yǔ)言集合[17]。能夠被確定型有窮接受器接受的語(yǔ)言族是正則語(yǔ)言。

2.2 3個(gè)值的確定型有窮自動(dòng)機(jī)

對(duì)確定型有窮接受器（DFA）進(jìn)行擴(kuò)展，將其狀態(tài)集合進(jìn)行擴(kuò)充，這對(duì)后面的討論尤為重要，參見第 4節(jié)。下面給出 3個(gè)值的確定型有窮自動(dòng)機(jī)（3DFA）的形式化定義[18]。一個(gè) 3DFA 的示例如圖2所示。

圖2 一個(gè)3DFA的示例

定義23DFA是一個(gè)7元組(Σ,S,s0,δ,Acc,Rej,Don’t)，其中Σ,S,s0和δ的定義與 DFA中的相同。將S分割成3個(gè)不相交的集合Acc，Rej和Don’t。其中，Acc是接受狀態(tài)的集合，Rej是拒絕狀態(tài)的集合，Don’t是不確定狀態(tài)的集合。

對(duì)于一個(gè) 3DFA C = (Σ,S,s0,δ,Acc,Rej,Don’t)，

如果δ(s0,u) ∈Acc，則字符串u被接受；

如果δ(s0,u) ∈Rej，則字符串u被拒絕；

如果δ(s0,u) ∈Don’t，則字符串u可能被接受也可能被拒絕。

C+表示 DFA (Σ,S,s0,δ,Acc∪Don’t)，這樣所有的不確定狀態(tài)都變成了接受狀態(tài)。

C-表示 DFA (Σ,S,s0,δ,Acc)，這樣所有的不確定狀態(tài)都變成了拒絕狀態(tài)。

由此可得出這樣的結(jié)論，L(C-)是C中可接受的字符串的集合，L(C+)是C中拒絕狀態(tài)集合的補(bǔ)集。

當(dāng)且僅當(dāng)一個(gè)確定性有窮自動(dòng)機(jī)A接受所有C接受的字符串并拒絕所有C拒絕的字符串時(shí)，稱A與C相一致。也就是說，A接受L(C-) 中的所有字符串，并拒絕L(C+)中的所有字符串，即L(C-)?L(A) ?L(C+)。C的一個(gè)與其相一致的最小化的有窮自動(dòng)機(jī)A是所有與C相一致的自動(dòng)機(jī)中狀態(tài)數(shù)目最少的。

圖3給出了一個(gè)與C（3DFA）相一致的有窮自動(dòng)機(jī)A。圖中矩形框表示全集，即Σ*中所有字符串，深色陰影表示L(C-)，深色陰影與淺色陰影的交集代表L(C+)。與C相一致的A接受L(C-)中所有字符串，拒絕所有不在L(C+)中的字符串。

圖3 與C (3DFA)相一致的有窮自動(dòng)機(jī)A

給定2個(gè)不相交的正則語(yǔ)言L1 和L2，一個(gè)有窮自動(dòng)機(jī)（DFA），A滿足L1 ?L(A) 和L(A) ∩L2=?。A接受L1中的所有字符串，拒絕L2中的所有字符串。即L1 ?L(A) ?L2。當(dāng)且僅當(dāng)A是一個(gè)區(qū)分DFA時(shí)，稱一個(gè)確定型有窮狀態(tài)機(jī)A區(qū)分L1和L2。如果一個(gè)DFA在所有可以區(qū)分L1和L2的有窮自動(dòng)機(jī)中是擁有狀態(tài)數(shù)目最少的有窮自動(dòng)機(jī)，則稱它為最小化的區(qū)分DFA。區(qū)分L1和L2的DFA如圖4所示。

圖4 區(qū)分L1和L2的有窮自動(dòng)機(jī)A

3 L*學(xué)習(xí)算法

3.1 算法背景

問題：從一個(gè)集合的成員和非成員中識(shí)別一個(gè)未知的正則語(yǔ)言集合。這個(gè)正則語(yǔ)言集合由一個(gè)最小勝任教師給出，該老師可以回答關(guān)于集合的成員資格詢問，并且能夠判斷一個(gè)假定的集合是否等價(jià)于未知集合（目標(biāo)語(yǔ)言集），如果不等價(jià)則給出一個(gè)反例。反例是正確集合（目標(biāo)語(yǔ)言集）與假設(shè)集合的對(duì)稱差。

基于 JFLAP的 DFA工具[19]實(shí)現(xiàn)了 L*學(xué)習(xí)算法。L*算法在多項(xiàng)式時(shí)間（關(guān)于最少狀態(tài)數(shù)目的DFA和由老師提供的最大長(zhǎng)度的反例）內(nèi)向最小勝任教師正確學(xué)習(xí)正則語(yǔ)言。在隨機(jī)化背景下，老師測(cè)試假設(shè)的能力可由隨機(jī)采樣預(yù)言機(jī)替代。

3.2 算法描述

下面詳細(xì)描述L*學(xué)習(xí)算法。

學(xué)習(xí)者L*維護(hù)一個(gè)觀察表(S,E,T)，其中S和E分別代表前綴封閉和后綴封閉的集合。S是狀態(tài)集合，E是區(qū)分狀態(tài)的集合。T是一個(gè)函數(shù)，它把(S∪SΣ)E中的元素字符串映射到{0, 1}。對(duì)于s∈(S∪SΣ)E，如果se∈U，則T(s,e)=1；否則T(s,e)=0。L*學(xué)習(xí)算法具體步驟如下。

1) 初始化：將S和E初始化為空串λ，對(duì)λ和字母表A中的每一個(gè)字母進(jìn)行成員資格詢問，構(gòu)建初始化的觀察表(S,E,T)。

2) 完備性和一致性校驗(yàn)：如果(S,E,T)不一致，則需找到S中的s1和s2，a∈A，e∈E，使row(s1)=row(s2)，且T(s1ae)≠T(s2ae)，將ae添加至E中。通過成員資格詢問擴(kuò)展T至(S∪SA)。

如果(S,E,T)不完備，則需找到s1∈S,s2∈S使對(duì)于任意a∈A,row(s1a)與row(s)都不同，并將s1a添加至S中。通過成員資格詢問擴(kuò)展T至(S∪SA)。

3) 一旦(S,E,T)是完備且一致的，就可以構(gòu)造狀態(tài)機(jī)M，并進(jìn)行等價(jià)詢問。如果老師返回一個(gè)反例ce，則將該反例及其所有前綴添加至S中。并用成員資格詢問擴(kuò)展T至(S∪SA)。然后再返回步驟2）做一致性和完備性校驗(yàn)，滿足一致性和完備性之后再做步驟 3）的等價(jià)詢問，以此循環(huán)往復(fù)，直至返回M=L(U)方才停止，并輸出M。

4 修正學(xué)習(xí)算法La*

由于安全協(xié)議的發(fā)送者、接收者、入侵者以及加密、解密、認(rèn)證等狀態(tài)繁多，在許多應(yīng)用場(chǎng)景中，老師可能并不能回答某些成員資格詢問，因此本文提出一種改進(jìn)的安全協(xié)議自適應(yīng)分析算法，即修正學(xué)習(xí)算法La*，運(yùn)用符號(hào)自動(dòng)機(jī)，并把教師定義為缺乏經(jīng)驗(yàn)的老師，學(xué)習(xí)大字符集。本節(jié)還對(duì)修正學(xué)習(xí)算法進(jìn)行正確性證明和復(fù)雜度分析，以及實(shí)例分析。

4.1 缺乏經(jīng)驗(yàn)老師

因?yàn)橐獙W(xué)習(xí)的對(duì)象可能不是完全具體的，是不可觀察的或者要回答這些提問所付出的代價(jià)是非常高昂的等，所以這些詢問可能是懸而未決的。最小勝任教師顯然不能滿足這種實(shí)際需要，下面引入缺乏經(jīng)驗(yàn)的老師(inexperienced teacher)[20]，并向缺乏經(jīng)驗(yàn)的老師學(xué)習(xí)，從而獲得所需的知識(shí)。

定義 3 缺乏經(jīng)驗(yàn)的教師。一個(gè)缺乏經(jīng)驗(yàn)的教師有權(quán)訪問 2個(gè)不相交的語(yǔ)言集L1，L2?Σ*，并回答下面2類詢問。

1) 成員資格詢問：如果給定的字符串在L1中，老師返回真(+)；如果給定的字符串在L2中，老師返回假(-)；如果給定的字符串既不在L1中，又不在L2中，老師返回不確定(?)。

2) 包含關(guān)系詢問：老師解決下面4種類型的語(yǔ)言集合包含問題，①L1?L(Ai)，②L(Ai)?L1，③其中，Ai是一個(gè)假定的符號(hào)自動(dòng)機(jī)。如果包含關(guān)系滿足，老師返回真；否則老師返回假并給出一個(gè)反例。

正如定義3所述，給定一個(gè)缺乏經(jīng)驗(yàn)的老師，學(xué)習(xí)者的任務(wù)是用成員資格詢問和等價(jià)詢問獲得一個(gè)可行的符號(hào)自動(dòng)機(jī)。即學(xué)習(xí)者的任務(wù)是找到一個(gè)接受L1的超集并拒絕L2的符號(hào)自動(dòng)機(jī)。

L1，L2?Σ*，是2個(gè)不相交的語(yǔ)言集。分3種情況討論。

1) 如果L1和L2都是正則語(yǔ)言，那么一定存在一個(gè)可行的DFA，例如精確接受L1的DFA。

2) 如果L1和L2都是確定性上下文無關(guān)語(yǔ)言，那么這個(gè)判定性問題是否可判定是未知的。

3) 如果L1和L2都是非確定性上下文無關(guān)語(yǔ)言，那么這個(gè)判定性問題是不可判定的。

后者可以通過一個(gè)簡(jiǎn)單的歸約來判定一個(gè)（非確定性）上下文無關(guān)語(yǔ)言是否為正則語(yǔ)言。

4.2 符號(hào)學(xué)習(xí)算法

Oded Maler 和 Irini Eleftheria Mens[21]定義了一種大字符集（無限集或不可列集合）上的廣義模型，過渡狀態(tài)由字母表有限分割的元素（子集）標(biāo)記。然后把從實(shí)例中學(xué)習(xí)正則語(yǔ)言的有窮自動(dòng)機(jī)擴(kuò)展至符號(hào)自動(dòng)機(jī)，改進(jìn)了學(xué)習(xí)算法。

定義 5 符號(hào)觀察表。符號(hào)觀察表是一個(gè)八元組A= (Σ,Σ',S,R,ψ,E,f,μ)，其中，–Σ是符號(hào)的集合，叫做字母表（字符集）；–E是Σ*的子集合；–f:(S∪R)E→{0, 1}是符號(hào)分類函數(shù)。

下面用一種直觀的表述方式來描述符號(hào)學(xué)習(xí)算法。假設(shè)字符集是有序的，且a0表示它的最小值。假設(shè)老師總是提供關(guān)于長(zhǎng)度和Σ*上字典序最小的反例。這個(gè)算法與L*算法非常類似，只是在處理反例時(shí)有所不同。

先對(duì)符號(hào)觀察表T= (Σ,Σ',S,R,ψ,E,f,μ)初始化，其中，Σ={a0},S={λ}，R= {a0},E= {λ}，和μ(a0)={a0}。無論何時(shí)，若T不完備，對(duì)于任意s∈S，一定存在某個(gè)r∈R使fr≠fs。為了使觀察表完備，要把r從R移動(dòng)至S并把r′=ra添加到R中，其中，a是一個(gè)新的字符。

當(dāng)?shù)玫揭粋€(gè)反例w時(shí)，對(duì)其進(jìn)行分解，即w=uav，其中，u是最大前綴，且u∈S∪R，滿足u∈μ(u)，分2種情況討論。

1) 若u∈S。反例表明ua被錯(cuò)誤的假設(shè)為[ua]的一部分，而且a被錯(cuò)誤的假設(shè)為[a]的一部分，有以下兩種情況。

①若存在某個(gè)a′≠a，使由符號(hào)自動(dòng)機(jī)分類的ua'v與uav的分類相一致，要把a(bǔ)及所有比a大的字符從[a]移動(dòng)至[a′]中，此時(shí)沒有新狀態(tài)產(chǎn)生。

②如果沒有上述字符，要生成一個(gè)新的a′，[a′]={b∈[a]:b≥a} ， 并 把 [a]-[a′]更 新 為 [a]，μ(ua′)=μ(u)a，把ua′添加到R中。

2) 若u∈R。反例表明g(u)=s∈S，由于該觀察表是最簡(jiǎn)化的，有對(duì)于其他任意s′∈S，fu≠fs′。因?yàn)閣是最短的反例，所以sav的分類是正確的。這樣可以推斷出u是一個(gè)新狀態(tài)并將其添加至S中。為了區(qū)分u和s，要把a(bǔ)v及其后綴添加到E中。根據(jù)a區(qū)分下面2種情況。

經(jīng)此改制，中科印刷目前股權(quán)制的架構(gòu)為國(guó)有、民營(yíng)、中科管理團(tuán)隊(duì)各占一部分。在企業(yè)決策中，以持股方的利益為出發(fā)點(diǎn)來進(jìn)行企業(yè)決策，可以更好、更貼切地指導(dǎo)企業(yè)的發(fā)展。“這一股權(quán)制架構(gòu)，從目前看，效果是非常好的?！鄙蛐胰A董事長(zhǎng)表示。

①如果a=a0是Σ的最小元素，則把字符a添加至Σ中，字符ua添加至R中。

②如果如果a≠a0，則把2個(gè)字符a及a'都添加至Σ中，其中，[a]={b:b

4.3 修正學(xué)習(xí)算法La*

基于以上對(duì)學(xué)習(xí)算法的討論和缺乏經(jīng)驗(yàn)老師的描述，以及安全協(xié)議狀態(tài)繁多可能造成狀態(tài)空間爆炸的問題，本文提出一種修正學(xué)習(xí)算法La*。該算法可用于大字符集的場(chǎng)景，并結(jié)合經(jīng)驗(yàn)不足的老師可能無法回答某些提問，對(duì)之前的算法進(jìn)行改進(jìn)。

修正學(xué)習(xí)算法 La*是一種主動(dòng)學(xué)習(xí)算法，它可以識(shí)別正則語(yǔ)言。假設(shè)一個(gè)老師可以回答2類詢問：成員資格詢問和包含關(guān)系詢問。

修正學(xué)習(xí)算法流程如圖5所示。

圖5 La*學(xué)習(xí)算法流程

1) 候選生成步驟由候選生成器操作，運(yùn)用擴(kuò)展的L*算法（多了一項(xiàng)不確定狀態(tài)）以及符號(hào)學(xué)習(xí)算法，產(chǎn)生一系列以3DFAC為目標(biāo)的候選自動(dòng)機(jī)（3DFA）。候選生成器通過成員資格詢問來構(gòu)造觀察表。如表1和圖6所示，舉例說明了一個(gè)觀察表和與之相對(duì)應(yīng)的 3DFA（方框表示不確定狀態(tài)）[18]。根據(jù)觀察表產(chǎn)生一個(gè)Ci（3DFA），如果這個(gè)Ci（3DFA）是不完備的或不一致的，候選生成器從反例中提取出區(qū)分字符串來擴(kuò)展觀察表，然后產(chǎn)生一個(gè)猜測(cè)的3DFA。N是完備且一致的3DFA的大小，m是由集合包含關(guān)系返回的最長(zhǎng)反例的長(zhǎng)度。候選生成器生成一個(gè)完備且一致的3DFA所需要的成員資格詢問數(shù)目為O(n2+nlogm)，至多產(chǎn)生n-1個(gè)不正確的3DFA。

表1 符號(hào)觀察

圖6 與表1相對(duì)應(yīng)的3DFA（方框表示不確定狀態(tài)）

2) 完備性校驗(yàn)步驟：檢驗(yàn)Ci關(guān)于L1和L2是否完備，如果Ci不完備，會(huì)返回給候選生成器一個(gè)反例來精化下一個(gè)猜測(cè)。否則，Ci是完備的，至下一步，計(jì)算與Ci相一致的Ai。修正學(xué)習(xí)算法通過計(jì)算與Ci相一致的最小化的符號(hào)自動(dòng)機(jī)來找到分割L1和L2的最小化的符號(hào)自動(dòng)機(jī)。為了確保所有分割L1和L2與Ci相一致的最小化的符號(hào)自動(dòng)機(jī)都被考慮到，所以修正學(xué)習(xí)算法要檢驗(yàn)Ci是否完備。檢驗(yàn)完備性可以歸約為檢驗(yàn)L(Ci-) ?L1 和L(Ci+)是否成立，這些可以通過集合包含關(guān)系來得到。

3) 最小化符號(hào)自動(dòng)機(jī)步驟：完備性校驗(yàn)完成后，下一步是計(jì)算一個(gè)與Ci相一致最小化的符號(hào)自動(dòng)機(jī)。本文把該問題歸約為不完全具體化的有限狀態(tài)機(jī)的最小化問題，可參照文獻(xiàn)[22]。修正學(xué)習(xí)算法將 3DFACi轉(zhuǎn)換成一個(gè)不完全具體化的符號(hào)自動(dòng)機(jī)M。引入文獻(xiàn)[21]中的算法，得到一個(gè)與M相一致的最小化的符號(hào)自動(dòng)機(jī)Mi。最后再把Mi轉(zhuǎn)換成一個(gè)符號(hào)自動(dòng)機(jī)Ai。也可參照文獻(xiàn)[20]中的最小化方法，運(yùn)用CSP求解器、SAT求解器或者SMT求解器。其中，CSP可以轉(zhuǎn)化為等價(jià)的SAT。

4) 可行性檢驗(yàn)：修正學(xué)習(xí)算法在計(jì)算出來與Ci相一致的最小化的符號(hào)自動(dòng)機(jī)Ai之后，要通過集合包含關(guān)系詢問來驗(yàn)證Ai是否區(qū)分開了L1 和L2。如果滿足了上述集合包含關(guān)系，則輸出正確結(jié)果，即最小化的符號(hào)自動(dòng)機(jī)。否則將反例輸入第1步，以此循環(huán)往復(fù)，直至正確結(jié)果輸出方才停止。

4.4 正確性證明和復(fù)雜度分析

下面的定理表明了修正學(xué)習(xí)算法的正確性。

定理 1修正學(xué)習(xí)算法會(huì)終止并輸出一個(gè)最小的可以區(qū)分L1和L2的符號(hào)自動(dòng)機(jī)。

定理證明過程可參考文獻(xiàn)[18]。

引理1假設(shè)Bi是可以接受正則語(yǔ)言Li的最小化的符號(hào)自動(dòng)機(jī)，其中i=1，2。最小化的接受L1中所有字符串并拒絕L2中所有字符串的C（3DFA）的大小不超過|B1| × |B2| 。

定理2假設(shè)Bi是可以接受正則語(yǔ)言Li的最小化的符號(hào)自動(dòng)機(jī)，其中i=1，2。修正學(xué)習(xí)算法學(xué)習(xí)區(qū)分L1和L2的最小化的符號(hào)自動(dòng)機(jī)所需要的成員資格詢問數(shù)目至多為O((|B1| × |B2|)2+ (|B1| × |B2|)logm)，包含關(guān)系詢問數(shù)目至多為4(|B1|×|B2|)- 1。其中，m為老師返回的最長(zhǎng)反例的長(zhǎng)度。

修正學(xué)習(xí)算法所需要的成員資格詢問數(shù)目至多為O((|B1| × |B2|)2+ (|B1| × |B2|) logm)，包含關(guān)系詢問數(shù)目至多為4(|B1|×|B2|)- 1。其中，m為老師返回的最長(zhǎng)反例的長(zhǎng)度。

證明假設(shè)C是接受L1中所有字符串并拒絕L2中所有字符串的最小化的3DFA。候選生成器所需要的成員資格詢問數(shù)目至多為O((|C|2×|C|logm)，提出錯(cuò)誤假設(shè)的3DFA數(shù)目至多為(|C|- 1)。根據(jù)引理，C（3DFA）的大小不超過|B1| × |B2|。由此可得，在最壞的情況下，修正學(xué)習(xí)算法學(xué)習(xí)一個(gè)最小化的符號(hào)自動(dòng)機(jī)所需要的成員資格詢問數(shù)目至多為O((|B1| × |B2|)2+ (|B1| × |B2|) logm)，包含關(guān)系詢問數(shù)目至多為(4(|B1|×|B2|)-1)（對(duì)于每一個(gè)假設(shè)的3DFA，修正學(xué)習(xí)算法需要2次包含關(guān)系詢問來檢驗(yàn)完備性是否滿足，以及2次包含關(guān)系詢問來檢驗(yàn)可行性是否滿足）。其中，m為老師返回的最長(zhǎng)反例的長(zhǎng)度。

4.5 學(xué)習(xí)算法實(shí)例分析

目標(biāo)語(yǔ)言集合為：L= {au:b≤a

運(yùn)用修正學(xué)習(xí)算法對(duì)L進(jìn)行學(xué)習(xí)，可得如下的觀察表（如表 2～表 6所示）和自動(dòng)機(jī)模型（如圖7～圖10所示）。

表2 觀察表T0

表3 觀察表T1

表4 觀察表T2

表5 觀察表T3

表6 觀察表T4

圖7 觀察表T0對(duì)應(yīng)的自動(dòng)機(jī)

圖8 觀察表T2對(duì)應(yīng)的自動(dòng)機(jī)

圖9 觀察表T3對(duì)應(yīng)的自動(dòng)機(jī)

圖10 觀察表T4對(duì)應(yīng)的自動(dòng)機(jī)

4.6 安全協(xié)議實(shí)例分析

Needham-Schroeder公鑰協(xié)議（NSPK協(xié)議）[23]按功能分為獲取公開密鑰和雙方身份認(rèn)證2部分。這里研究其身份認(rèn)證部分。

首先使用Scyther[24]工具對(duì)經(jīng)典的NS認(rèn)證協(xié)議進(jìn)行模型檢測(cè)，然后運(yùn)用修正學(xué)習(xí)算法對(duì)攻擊圖（即反例）進(jìn)行學(xué)習(xí)，最后得到改進(jìn)的NS協(xié)議，即NSL協(xié)議[25]。

4.6.1 Needham-Schroeder協(xié)議分析

2) 檢測(cè)結(jié)果（scyther results:autoverify）如圖11所示。

圖11 Scyther工具對(duì)NS協(xié)議的檢測(cè)結(jié)果

3）攻擊圖如圖12所示。

4) 反例學(xué)習(xí)及協(xié)議改進(jìn)

運(yùn)用安全協(xié)議自適應(yīng)學(xué)習(xí)算法對(duì)反例（攻擊路徑或不安全的路徑）進(jìn)行學(xué)習(xí)，通過循環(huán)往復(fù)的執(zhí)行學(xué)習(xí)算法，將反例的前綴和后綴分別添加到觀察表的前綴集合和后綴集合中，直至輸出一個(gè)滿足完備性和一致性的觀察表所對(duì)應(yīng)的自動(dòng)機(jī)為止。最后通過協(xié)議模型逆向指導(dǎo)安全協(xié)議的優(yōu)化和改進(jìn)。如NS協(xié)議存在遺漏身份的攻擊，當(dāng)在協(xié)議執(zhí)行的第2)步驟加入發(fā)送者B的身份，即可修復(fù)該漏洞。下面介紹NS協(xié)議的改進(jìn)協(xié)議NSL協(xié)議。

4.6.2 Needham-Schroeder-Lowe協(xié)議

圖12 基于Scyther工具的NS協(xié)議攻擊

檢測(cè)結(jié)果如圖13所示。

圖13 基于Scyther工具的NS協(xié)議模型檢測(cè)結(jié)果

5 相關(guān)工作

當(dāng)前學(xué)術(shù)界在自動(dòng)機(jī)學(xué)習(xí)算法方面已經(jīng)有很多相關(guān)工作。在此簡(jiǎn)要介紹并與本文的工作進(jìn)行比較，具體見表7。

表7 相關(guān)工作比較

現(xiàn)有的自動(dòng)機(jī)學(xué)習(xí)算法從方法上主要分為主動(dòng)(active)學(xué)習(xí)算法和被動(dòng)（passive）學(xué)習(xí)算法。主動(dòng)學(xué)習(xí)算法也稱作在線（online）學(xué)習(xí)算法，被動(dòng)學(xué)習(xí)算法也稱作離線（offline）學(xué)習(xí)算法。

被動(dòng)學(xué)習(xí)算法得到正反例和負(fù)反例的固定集合，包括接受和拒絕的字符串。學(xué)習(xí)算法提供一個(gè)接受正字符串拒絕負(fù)字符串的(最小化的)自動(dòng)機(jī)。Oncina和Garcia提出一種被動(dòng)學(xué)習(xí)算法RPNI，該算法是一種推斷非必需最小化的DFA的有效算法。Denis等提出一種離線學(xué)習(xí)算法 DeLeTe2，該算法是在 RPNI算法的基礎(chǔ)上提出來的，文獻(xiàn)[8]中闡述領(lǐng)該算法的擴(kuò)展算法以及學(xué)習(xí)的NFA的離線學(xué)習(xí)算法。

主動(dòng)學(xué)習(xí)算法有可能提出更深的詢問，某字符串是否在目標(biāo)語(yǔ)言中。經(jīng)典的主動(dòng)學(xué)習(xí)算法Angluin’s L*算法基于成員資格詢問和等價(jià)詢問學(xué)習(xí)一個(gè)最小化的DFA。以L*為基礎(chǔ)，后續(xù)又出現(xiàn)多種主動(dòng)學(xué)習(xí)算法。Benedikt等提出 NL*算法，用來學(xué)習(xí) NFA 或 RFSA。Muzammil Shahbaz 和 Roland Groz提出LM*和LM+2種算法，可以推斷出Mealy自動(dòng)機(jī)，前者是對(duì)L*的改進(jìn)，后者在前者的基礎(chǔ)上增加了處理反例的新方法。Pacharoen等提出 LNM*算法，可以推斷可觀察的不確定的有窮狀態(tài)機(jī)。Chen等提出一種主動(dòng)學(xué)習(xí)算法Lsep，可以學(xué)習(xí)并產(chǎn)生區(qū)分DFA。 Martin Leucker和Daniel Neider提出學(xué)習(xí)正則語(yǔ)言的學(xué)習(xí)算法CL1,L2，可以在缺乏經(jīng)驗(yàn)的老師情形下學(xué)習(xí)，但此時(shí)字符集依然是有限的。

6 結(jié)束語(yǔ)

安全協(xié)議是保障網(wǎng)絡(luò)安全的基礎(chǔ)。安全協(xié)議自適應(yīng)分析框架[9]通過反例指導(dǎo)協(xié)議的修正，其中，學(xué)習(xí)算法起著至關(guān)重要的作用。然而，經(jīng)典的 L*學(xué)習(xí)算法并不能滿足日益復(fù)雜的安全協(xié)議的分析需要，為此，本文提出一種改進(jìn)的安全協(xié)議自適應(yīng)分析算法，即修正學(xué)習(xí)算法La*，解決部分教師缺乏經(jīng)驗(yàn)的問題，并將字符集擴(kuò)展為大字符集。將該修正學(xué)習(xí)算法運(yùn)用到安全協(xié)議自適應(yīng)模型檢測(cè)中，可以實(shí)現(xiàn)對(duì)復(fù)雜協(xié)議的檢測(cè)結(jié)果（較長(zhǎng)反例）的學(xué)習(xí)。修正學(xué)習(xí)算法 La*將有助于提高安全協(xié)議自適應(yīng)模型檢測(cè)的效率、降低分析和設(shè)計(jì)成本、緩解狀態(tài)空間爆炸并增強(qiáng)協(xié)議本身對(duì)環(huán)境和各種攻擊手段的自適應(yīng)防御能力。

自動(dòng)機(jī)學(xué)習(xí)算法仍有待于深入研究，比如對(duì)上下文無關(guān)語(yǔ)言的學(xué)習(xí)。上下文無關(guān)語(yǔ)言包括正則語(yǔ)言，需要對(duì)學(xué)習(xí)正則語(yǔ)言的修正學(xué)習(xí)算法做進(jìn)一步推廣和改進(jìn)。

[1] 王亞弟, 束妮娜, 韓繼紅, 等. 密碼協(xié)議形式化分析[M]. 北京: 機(jī)械工業(yè)出版社, 2006.WANG Y D, SHU N N,HAN J H. Formal Analysis of Security Protocol[M]. Beijing: China Machine Press, 2006.

[2] WOO T, LAM S S. A semantic model for authentication protocols[A].Proceedings of IEEE symposium on security and privacy[C]. 1993.178-194.

[3] CLARKE E M, JHA S, MARRERO W. Partial order reductions for security protocol verification[A]. Tools and Algorithms for the Construction and Analysis of Systems[C]. 2000.

[4] SHAMATIKOV V, STERN U. Efficient finite state analysis for large security protocols[A]. Proceedings of 11th IEEE Computer Security Foundation Workshop[C]. 1998. 106-115.

[5] BROADFOOT P J, ROSCOE A W. Internalising agents in CSP protocol models[A]. Proceedings of Workshop on Issues in the Theory of Security[C]. 2002.

[6] HUI M L, GAVIN L. Fault-preserving simplifying transformations for security protocols[J].Journal of Computer Security, 2001,9(1-2):3-46.

[7] STOLLER S D. A Bound on Attacks on Authentication protocols[M].Foundations of Information Technology in the Era of Network and Mobile Computing. New Yorks Springer US, 2002.

[8] ROSCOE A W. Proving security protocols with model checkers by data independence techniques[A]. Proceedings of 11th IEEE Computer Security Foundations Workshop[C]. 1998. 84-95.

[9] FAN D, ZHANG Y Q. An adaptive formal modeling and analysis schema for security protocols[A]. Chinese Association for Cryptologic Research[C]. ZhengZhou, China, 2014.

[10] MAZHARI S M, MONSEF H, FALAGHI H. A hybrid heuristic and learning automata‐based algorithm for distribution substations siting,sizing and defining the associated service areas[J]. International Transactions on Electrical Energy Systems, 2014, 24(3): 433-456.

[11] 張孝紅. 基于形式化方法的安全協(xié)議自動(dòng)化驗(yàn)證算法的研究[D].湖南: 湖南大學(xué), 2010.ZHANG X H. Automated verification algorithm for security protocols based on formal methods[D]. Hunan: Hunan University, 2010.

[12] ANGLUIN D. Learning regular sets from queries and counterexamples[J]. Information and computation, 1987, 75(2): 87-106.

[13] SHAHBAZ M, GROZ R. Inferring Mealy Machines[M]. FM 2009:Formal Methods. Springer Berlin Heidelberg, 2009. 207-222.

[14] BOLLIG B, HABERMEHL P, KERN C,et al. Angluin-style learning of NFA[A]. IJCAI[C]. 2009. 1004-1009.

[15] PACHAROEN W, AOKI T, BHATTARAKOSOL P,et al. Active learning of nondeterministic finite state machines[J]. Mathematical Problems in Engineering. 2013. 2013(8):1-11.

[16] LINZ P,et al. 形式語(yǔ)言與自動(dòng)機(jī)導(dǎo)論[M]. 北京: 機(jī)械工業(yè)出版社,2005.LINZ P,et al. An Introduction to Formal Languages and Automata[M].Beijing: China Machine Press. 2005.

[17] SALOMAA A. Formal Languages[M].New York: Academic Press.1973.

[18] CHEN Y F, FARZAN A, CLARKE E M,et al. Learning minimal separating DFA’s for compositional verification[A]. Tools and Algorithms for the Construction and Analysis of Systems[C]. Springer Berlin Heidelberg, 2009.

[19] ALECHA M, HERMO M. A learning algorithm for deterministic finite automata using JFLAP[J]. Electronic Notes in Theoretical Computer Science, 2009, 248: 47-56.

[20] LEUCKER M, NEIDER D. Learning minimal deterministic automata from inexperienced teachers[A]. Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change[C]. Springer Berlin Heidelberg, 2012.

[21] MALER O, MENS I E. Learning regular languages over large alphabets[A]. Tools and Algorithms for the Construction and Analysis of Systems[C]. Springer Berlin Heidelberg, 2014.

[22] PAULL M C, UNGER S H. Minimizing the number of states in incompletely specified sequential switching functions[A]. IRE Transitions on Electronic Computers EC-8[C]. 1959.356–366.

[23] NEEDHAM R M, SCHROEDER M D. Using encryption for authentication in large networks of computers[J]. Communications of the ACM, 1978, 21(12): 993-999.

[24] CREMERS C J F. The scyther tool: verification, falsification, and analysis of security protocols[A]. Computer Aided Verification[C].Springer Berlin Heidelberg, 2008. 414-418.

[25] LOWE G. Breaking and fixing the needham-schroeder public-key protocol using FDR[A].Tools and Algorithms for the Construction and Analysis of Systems[C]. Springer Berlin Heidelberg, 1996. 147-166.