雷欽隆臺灣大學：電機工程學研究所李思穎Li, Ssu-YingSsu-YingLi2007-11-262018-07-062007-11-262018-07-062007http://ntur.lib.ntu.edu.tw//handle/246246/53400目前分析安全群播機制大多是使用人工的方式，但是利用人工的方式來分析安全群播機制時，往往有不足、設想不夠周全的地方，因此若能使用自動化工具來分析，可以幫助我們研究發展更安全的機制。 Alloy是一種關係式的模擬語言，在不給予機制的狀況下，只需要簡單的雛型，就可以建構所要模擬的行為，並有效率的模擬所想的狀況及加以分析。 我們利用Alloy Analyzer 來模擬分析使用轉密方式的安全群播機制，經過驗證的結果，找出這個安全群播機制的缺失，修正機制後更可以達到群播機制的基本安全特性。At the present time, the secure multicast scheme analyze mostly by manual. But it considered comprehensive enough frequently. It can help us to develop a more secure multicast scheme by using the automatic tool. Alloy is a model language based on relation. It can construct model of some behavior without mechanism, and modeling more efficient. We use Alloy Analyzer to simulate and analyze the secure multicast scheme that use proxy encryption. These analyses display one flaw when consider the transmit delay. The analyzer suggests and checks some fixes. Then the result makes sure the secure multicast scheme to achieve the basic properties.1 Introduction 1 2 Related Work 3 2.1 Proxy Encryption . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 3 Overview of Alloy 6 3.1 Language . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 3.1.1 Operators for Expressions . . . . . . . . . . . . . . . . . . . . . 7 3.1.2 Elementary Formulas . . . . . . . . . . . . . . . . . . . . . . . . 8 3.1.3 Higher-Order Quanti‾ers . . . . . . . . . . . . . . . . . . . . . . 8 3.1.4 Hight-level Constructs . . . . . . . . . . . . . . . . . . . . . . . 9 3.2 Analyzer . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 4 Secure Multicast Using Proxy Encryption 13 4.1 Description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 5 Model 16 5.1 Basic Signatures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 5.2 Extended Signatures . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 5.3 Fact . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 5.4 Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 5.5 Assections . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 6 Analysis 33 7 Conclusions and Future Work 361059428 bytesapplication/pdfen-USAlloy安全群播機制代理人加密模擬協定分析secure multicastschemeproxy encryptionmodelingprotoccl analysisthesishttp://ntur.lib.ntu.edu.tw/bitstream/246246/53400/1/ntu-96-J94921023-1.pdf