使用Alloy分析安全群播機制

Automatic Analysis of Secure Multicast Scheme Using Alloy

李思穎(Ssu-Ying Li)

指導教授 ： 雷欽隆

國立臺灣大學/電機資訊學院/電機工程學研究所/碩士(2007年)

https://doi.org/10.6342/NTU.2007.10462

摘要

目前分析安全群播機制大多是使用人工的方式，但是利用人工的方式來分析安全群播機制時，往往有不足、設想不夠周全的地方，因此若能使用自動化工具來分析，可以幫助我們研究發展更安全的機制。

Alloy是一種關係式的模擬語言，在不給予機制的狀況下，只需要簡單的雛型，就可以建構所要模擬的行為，並有效率的模擬所想的狀況及加以分析。

我們利用Alloy Analyzer 來模擬分析使用轉密方式的安全群播機制，經過驗證的結果，找出這個安全群播機制的缺失，修正機制後更可以達到群播機制的基本安全特性。

關鍵字

Alloy ； 安全群播機制 ； 代理人加密 ； 模擬 ； 協定分析

並列摘要

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.

並列關鍵字

Alloy ； secure multicast ； scheme ； proxy encryption ； modeling ； protoccl analysis

參考文獻

[1] Matt Blaze and Gerrit Bleumer, Divertible Protocols and Atomic Proxy Cryp-

cations Security, 2005

(TOCS), May 1990

the tenth Network and Distributed System Security Symposium, February 2003

[5] Daniel Jackson, Automating ‾rst-order relational logic, In Proceedings 8th ACM