基于UML的形式化框架及其在安全協(xié)議驗(yàn)證中的應(yīng)用.pdf

1、隨著信息技術(shù)的飛速發(fā)展，計(jì)算機(jī)軟件系統(tǒng)已廣泛應(yīng)用到社會的各個領(lǐng)域。軟件規(guī)模和復(fù)雜性在不斷增加，軟件出現(xiàn)錯誤的可能性也隨之增加。為了保證軟件的質(zhì)量、提高軟件的可靠性，將主流的軟件開發(fā)方法與形式化方法相結(jié)合是一種可行的方法。
　　本文結(jié)合UML方法與形式化方法的優(yōu)點(diǎn)，提出了基于擴(kuò)展UML的輕量級形式化框架。通過領(lǐng)域分析，選取并擴(kuò)展合適的UML模型，形成領(lǐng)域輪廓以支持特定領(lǐng)域建模，進(jìn)而提供UML模型向形式化模型轉(zhuǎn)換的可行性方案。該框架避

2、免了復(fù)雜建模過程，降低了形式化方法的使用門檻，擴(kuò)大了形式化方法在實(shí)際軟件開發(fā)中的應(yīng)用。基于該框架，本文還提出了安全協(xié)議形式化驗(yàn)證方法，并從工程的角度給出了一套完整的安全協(xié)議形式化驗(yàn)證工程方法。該方法制定了適用于安全協(xié)議建模的UM L類圖和時序圖擴(kuò)展機(jī)制，用工程化的協(xié)議表達(dá)方式形式化安全協(xié)議，完成協(xié)議安全性驗(yàn)證。通過匹配及轉(zhuǎn)換規(guī)則，本文實(shí)現(xiàn)了從擴(kuò)展UML模型向ProVerif規(guī)格的Pi演算模型的轉(zhuǎn)化，以驗(yàn)證安全協(xié)議的私密性和認(rèn)證性。此外，