文章基本信息

标题：Verification of Resistance of Denial of Service Attacks in Extended Applied Pi Calculus with ProVerif
本地全文：下载
作者：Meng, Bo ; Wang, Wei ; Chen, Wei 等
期刊名称：Journal of Computers
印刷版ISSN：1796-203X
出版年度：2012
卷号：7
期号：4
页码：890-899
DOI：10.4304/jcp.7.4.890-899
语种：English
出版社：Academy Publisher
摘要：Owning to the damage of denial of service attacks in security protocols, resistance of denial of service attacks plays an important role in remote voting protocols. Recently Meng et al. proposed a secure remote internet voting protocol that claims to satisfy formal definitions of key properties without physical constrains. In this study firstly the review of the formal model of resistance of denial of service attacks in security protocols is introduced, then extended applied pi calculus and Huang et al. formal model are reviewed, after that Meng et al. protocol is modeled in extended applied pi calculus, finally resistance of denial of service attacks is proved with ProVerif. The result we obtain is that Meng et al. protocol is not resistance of denial of service attacks because one denial of service attack is found. At the same time we also propose a method to prevent it from the denial of service attack. To our best knowledge, we are conducting the first mechanized proof of resistance of denial of service attacks in Meng et al. protocol for an unbounded number of honest and corrupted voters.
关键词：protocol security;automatic verification;protocol state;symbolic model;availability