計算機網路之安全通信協定的驗證與系統實作(I)

Abstract

計算機網路愈來愈普及，也愈來愈重要。許多民生、工業、國防及人權隱私等重要課題， 均要求安全、保密的通信管道。以當前的工業水準及資訊基礎建設的普及狀況而言，計 算機之間的通信管道，大致已十分暢通，然而我們的要求也逐漸演變成通信管道的安全 性與隱密性。 欲建立安全隱密的通信管道，需完成二項工作：一是強健而有效的加解密演算，另一則 是安全通信協定。前一項奠基於密碼學及相關數學領域的進展，敝人的研究重點則在於 第二項：如何確定我們採用的安全通信協定沒有漏洞或弱點。我們打算採用二種方向來 研究此課題：一是從理論上來驗證一個安全通信協定，另一是從實務上製作一個安全通 信協定的模擬器。 理論上我們採用二種方法。首先我們採用一階述詞邏輯（first-order predicate logic）來分 析驗證安全通信協定，其次我們採用strand space 的技術來分析一個安全通信協定的結 構，進而確認它的一些性質。 在實作上，我們準備設計並製作一個安全通信協定的模擬器，此模擬器會模擬安全通信 協定的運作過程，並且提供中斷、置換等功能，來讓安全通信協定的設計人，自由嘗試 協定的各種運作方式，以其找出隱藏在安全通信協定內的漏洞或弱點。此項模擬器並且 會更進一步將理論上的分析方法實際製作出來，用來分析安全通信協定。由於理論上的 分析的方法，很可能無法百分之百的確認安全通信協定是否正確無誤。我們並且將相關 文獻上已經發現的各種安全協定缺失，製作成一系列的檢驗項目，這些項目可以用來檢 驗新提出或現有的各種安全通信協定，而安全通信協定若能通過愈多項目的檢驗，則我 們對此安全協定的信心也愈堅定。我們可以隨時增加新的檢驗項目，以卻安全協定的品 質。