Automatic verification of web service protocols for epistemic specifications under dolev-yao model | |
Chen, Qingliang ; Su, Kaile ; Liu, Chanjuan ; Xiao, Yinyin | |
2010 | |
英文摘要 | Web service protocols are designed in XML formats so the message structures within are quite different from the conventional protocols. Therefore, the traditional formal verification techniques which have gain substantial achievements in practice, cannot be applied directly to them because their underlying models are written in Alice&Bob-style descriptions using high-level message formats instead of XML tags. In this paper, we propose a justification-oriented and automatic formal approach to verify, in the standard Dolev-Yao model, security properties expressed as epistemic notions for a Web service protocol, based on a fault-preserving mapping tool called SuD (SOAP under Dolev-Yao). Our approach can shed more light on Web service protocols in another perspective because the concerned properties to be verified are some inherent features of protocols. ? 2010 IEEE.; EI; 0 |
语种 | 英语 |
DOI标识 | 10.1109/ICSS.2010.33 |
内容类型 | 其他 |
源URL | [http://ir.pku.edu.cn/handle/20.500.11897/330163] |
专题 | 信息科学技术学院 |
推荐引用方式 GB/T 7714 | Chen, Qingliang,Su, Kaile,Liu, Chanjuan,et al. Automatic verification of web service protocols for epistemic specifications under dolev-yao model. 2010-01-01. |
个性服务 |
查看访问统计 |
相关权益政策 |
暂无数据 |
收藏/分享 |
除非特别说明,本系统中所有内容都受版权保护,并保留所有权利。
修改评论