標題: 計算機網路之安全通信協定的驗證與系統實作(I)
Verification and Simulation of Security Protocols in Computer Networks(I)
作者: 楊武
國立交通大學資訊科學學系
關鍵字: 安全通信協定;安全通信協定檢驗;安全通信協定驗證;安全通信協定模擬器;一階述詞邏輯;資料型態缺失;電腦通信
公開日期: 2004
摘要: 計算機網路愈來愈普及,也愈來愈重要。許多民生、工業、國防及人權隱私等重要課題, 均要求安全、保密的通信管道。以當前的工業水準及資訊基礎建設的普及狀況而言,計 算機之間的通信管道,大致已十分暢通,然而我們的要求也逐漸演變成通信管道的安全 性與隱密性。 欲建立安全隱密的通信管道,需完成二項工作:一是強健而有效的加解密演算,另一則 是安全通信協定。前一項奠基於密碼學及相關數學領域的進展,敝人的研究重點則在於 第二項:如何確定我們採用的安全通信協定沒有漏洞或弱點。我們打算採用二種方向來 研究此課題:一是從理論上來驗證一個安全通信協定,另一是從實務上製作一個安全通 信協定的模擬器。 理論上我們採用二種方法。首先我們採用一階述詞邏輯(first-order predicate logic)來分 析驗證安全通信協定,其次我們採用strand space 的技術來分析一個安全通信協定的結 構,進而確認它的一些性質。 在實作上,我們準備設計並製作一個安全通信協定的模擬器,此模擬器會模擬安全通信 協定的運作過程,並且提供中斷、置換等功能,來讓安全通信協定的設計人,自由嘗試 協定的各種運作方式,以其找出隱藏在安全通信協定內的漏洞或弱點。此項模擬器並且 會更進一步將理論上的分析方法實際製作出來,用來分析安全通信協定。由於理論上的 分析的方法,很可能無法百分之百的確認安全通信協定是否正確無誤。我們並且將相關 文獻上已經發現的各種安全協定缺失,製作成一系列的檢驗項目,這些項目可以用來檢 驗新提出或現有的各種安全通信協定,而安全通信協定若能通過愈多項目的檢驗,則我 們對此安全協定的信心也愈堅定。我們可以隨時增加新的檢驗項目,以卻安全協定的品 質。
官方說明文件#: NSC93-2213-E009-092
URI: http://hdl.handle.net/11536/91380
https://www.grb.gov.tw/search/planDetail?id=1007045&docId=189792
顯示於類別:研究計畫