基于通信順序進(jìn)程的安全協(xié)議形式化研究.pdf

1、隨著計(jì)算機(jī)網(wǎng)絡(luò)和通信網(wǎng)絡(luò)的日趨復(fù)雜，協(xié)議的種類和數(shù)量也越來越多，其規(guī)模也越來越大，如何設(shè)計(jì)出功能上正確可靠，邏輯上一致完整的通信協(xié)議，并系統(tǒng)地進(jìn)行協(xié)議實(shí)現(xiàn)，協(xié)議驗(yàn)證和協(xié)議測試，已經(jīng)成為了一個(gè)非常具有挑戰(zhàn)性的課題。于是就出現(xiàn)了一門新興的軟件工程分支學(xué)科——協(xié)議工程，協(xié)議工程是形式化的協(xié)議開發(fā)過程，它使用形式化的方法來描述協(xié)議的設(shè)計(jì)和維護(hù)中的各個(gè)活動(dòng)，其核心部分就是通信協(xié)議的形式化描述技術(shù)。目前，常用的協(xié)議形式化描述技術(shù)主要包括：有限狀態(tài)機(jī)

2、(FSM)模型、Petri網(wǎng)模型以及LOTOS,CAPSL等形式化描述語言。這些方法各有優(yōu)點(diǎn)和缺點(diǎn)，因此，非常有必要繼續(xù)研究和探索這一領(lǐng)域的新理論和新方法。
　　 在對(duì)通信順序進(jìn)程CSP框架做了深入研究的基礎(chǔ)上，從協(xié)議建模和分析等各個(gè)方面進(jìn)行了探討，研究和分析比較了目前常用的協(xié)議形式化描述技術(shù)的特點(diǎn)及各自的局限。然后通過對(duì)Yahalom認(rèn)證協(xié)議的建模，給出了用CSP方法對(duì)認(rèn)證協(xié)議進(jìn)行建模和分析的一般方法和步驟。
　　 緊

3、接著，通過對(duì)RIP等協(xié)議的CSP實(shí)例模型的描述，將CSP方法擴(kuò)展到對(duì)一般通信協(xié)議的描述，總結(jié)了用CSP建立協(xié)議模型的一般方法。最后，鑒于協(xié)議形式化描述到協(xié)議實(shí)施中存在的不一致性，從理論上提出一種基于系統(tǒng)API平臺(tái)的安全協(xié)議CSP開發(fā)框架，將形式化方法與高級(jí)語言有機(jī)結(jié)合起來，實(shí)現(xiàn)了協(xié)議的形式化描述轉(zhuǎn)換為可執(zhí)行代碼處理過程的自動(dòng)化，有利于快捷準(zhǔn)確地將已完成CSP驗(yàn)證的安全協(xié)議翻譯為可執(zhí)行代碼，避免了在將CSP描述轉(zhuǎn)換為可執(zhí)行代碼預(yù)處理過程中