《移動自組網無需可信第三方的可信公平非抵賴協定研究》是依託中國科學技術大學，由熊焰擔任項目負責人的面上項目。
基本介紹
- 中文名：移動自組網無需可信第三方的可信公平非抵賴協定研究
- 項目類別：面上項目
- 項目負責人：熊焰
- 依託單位：中國科學技術大學
中文摘要,結題摘要,
中文摘要
由於移動自組網Manet中所有結點的不可信性，傳統的信息安全機制和方法因需要一個集中提供非抵賴服務的可信第三方TTP而無法完全保證Manet的安全性和可靠性。本課題擬在可信平台模組TPM的安全體系結構基礎上提出一個無需TTP的可信非抵賴協定，並研究該協定及軟體的形式化建模、證明、評估、檢測與驗證技術以保證其可信性即研究基於Pi演算的可信公平非抵賴協定形式化建模和驗證技術；研究基於高階邏輯的可信公平非抵賴協定軟體的形式化建模與證明技術；研究基於數據挖掘的可信公平非抵賴協定的動態評估技術；研究基於模型檢測的可信公平非抵賴協定軟體的形式化檢測技術；研究Manet中無需可信第三方的可信公平非抵賴協定軟體以驗證其安全可靠性。本課題的目的就是為Manet提供一個無需TTP的可信公平非抵賴協定軟體以便徹底拋棄TTP，克服現有無需TTP公平非抵賴協定的機率公平缺點，進一步推動國內可信移動計算的研究和發展。
結題摘要
移動自組網 Manet(Mobile Ad-hoc Networks)是由若干帶有無線收發器的移動節點所組成的無基站的自治網路，廣泛套用于軍事、民用、商業等領域。為保證其安全性,在交易結束後,交易雙方都應得到相應的證據,在出現爭議時,仲裁方便能依據雙方提供的證據進行仲裁,為此人們提出了公平非抵賴協定。 傳統的公平非抵賴協定大多基於可信第三方TTP(Trusted Third Party),選擇一個權威、中立、可信任的第三方節點或組織作為TTP 來實現證據交換。但是, 由於Manet的無中心性及拓撲的動態性, 傳統TTP因採用集中服務會帶來協定的效率瓶頸,同時TTP的崩潰將導致網路中所有節點都無法得到公平非抵賴服務。於是,無需TTP的公平非抵賴協定成為研究的重點。 我們的項目有以下貢獻： (1) 提出針對TPM可信認證協定軟體的形式化建模、精化與證明方法。由於TPM體系中，普遍認為TPM是可信的，這樣我們需要假設TPM外的軟體平台是不可信的。針對這個問題，我們對傳統的敵方模型進行了修改，提出新的安全模型。在新的安全模型中，我們提出額外假設：未被TPM進行完整性驗證平台是可能遭遇敵方的攻擊的。進一步，我們使用Event-B精化語言，進行逐層精化； (2) 基於TPM及虛擬化技術的最小化可信基系統。由於部分程式涉及到用戶的隱私、機密數據，需要保證這些安全敏感程式（Security-sensitive Application）代碼和數據的安全。我們提出一個新的架構，使用較小的最小可信基(Trusted Computing Base, TCB)，實現安全敏感程式在不可信作業系統中的安全執行，並且安全敏感程式擁有和傳統程式一樣的作業系統服務。 (3) 針對可信計算架構中遮蔽技術的形式化證明框架。為了保護安全敏感程式不受這些來自主機系統的威脅，通常會在主機系統之下增加遮蔽系統，對安全敏感程式進行保護。之前的針對遮蔽系統的形式化方法僅考慮了一個防護機制的作用在一個形式化工作中。基於這個動機，我們提出了一個綜合性的形式化框架來分析遮蔽系統是否給安全敏感程式提供了足夠的安全保證。 基於本項目已發表文章31篇，其中SCI期刊15篇，國際會議7篇，CCF A類論文3篇，B類論文3篇，申請發明專利8項，完成預期研究計畫。
