实验室硕士研究生参加ABZ2012国际会议

撰稿人 王婷

2012年6月18日至20日，王婷参加了在意大利Pisa举行的the 3rd International Conference on ASM, Alloy, B, VDM, and Z （ABZ 2012）。该会议旨在为5种state-based和machine-based的形式化方法提供相互交流的平台：Abstract State Machines (ASM)、Alloy、B、VDM 和Z，他们被广泛应用于学术界和工业界的硬件和软件系统的设计和分析。

会上，王婷做了题为“Active Attacking Multicast Key Management Protocol Using Alloy” 的报告，与参会的各国专家学者进行了交流。此报告的主要内容是：讲解如何用Alloy Analyzer（一种自动分析工具）来检测由Tanaka和Sato提出的组播密钥管理协议的漏洞，并且发现了一些新的漏洞。首先用Alloy（建模语言）为组播密钥管理协议和主动攻击者建模，然后用Alloy Analyzer来检测攻击者是否能攻击这个协议，最后发现攻击者使这个协议的4个基本性质都不能满足，这个协议不能抵抗主动攻击。尽管Taghdiri和Jackson之前也分析了这个协议，但是他们忽略了主动攻击，致使他们没有发现这些由主动攻击者造成的漏洞。虽然Steel和Bundy也分析了这个协议，但是他们用的工具是CORAL，存在一些缺陷，尤其是运行时间，长达3.5个小时检测到一个攻击。与此相比，我们用Alloy来分析，仅用几秒钟就可以检测到攻击，Alloy的高速主要归功于SAT求解器。