安全協(xié)議多目標(biāo)語言代碼自動化實現(xiàn)的研究與實現(xiàn).pdf

1、目前，安全協(xié)議的代碼實現(xiàn)仍然主要依賴于手工編碼，但手工編碼低效、易錯，容易引入各種漏洞，也不利于安全協(xié)議的修訂和更新。人們對安全協(xié)議的代碼自動化實現(xiàn)還未開展廣泛和深入的研究，已有的工作也存在諸多不足。
　　針對這些問題，本文提出了一個安全協(xié)議多目標(biāo)語言代碼自動化實現(xiàn)方案。首先，設(shè)計了一個安全協(xié)議XML形式化描述方法，完成抽象協(xié)議與XML描述之間的映射。其次，提出了一個可復(fù)用的面向?qū)ο髤f(xié)議代碼框架，為安全協(xié)議的運行提供了一個基本的支

2、撐。最后，開發(fā)了一個解析器，將安全協(xié)議的XML描述轉(zhuǎn)化為多目標(biāo)語言實現(xiàn)。為了增強(qiáng)協(xié)議及生成代碼的安全性和健壯性，本文從兩個方面著手：（1）在協(xié)議設(shè)計方面。在代碼自動化實現(xiàn)前，將安全協(xié)議XML描述轉(zhuǎn)換為CAPSL語言描述，進(jìn)而利用現(xiàn)有形式化驗證工具分析協(xié)議安全性，以發(fā)現(xiàn)和避免一些協(xié)議設(shè)計方面的缺陷和攻擊；（2）協(xié)議實現(xiàn)方面。安全協(xié)議中常見的并行會話攻擊和類型攻擊，在編碼階段存在切實可行的防止方法，本文在方案中提出并實現(xiàn)了這些方法，從而避免