Institutional Repository
| an inductive approach to strand spaces | |
| Li Yongjian; Pang Jun | |
| 2011 | |
| Source | Formal Aspects of Computing
 |
| ISSN | 9345043 |
| Issue | 1Pages:1-37 |
| English Abstract | In this paper, we develop an inductive approach to strand spaces, by introducing an inductive definition for bundles. This definition provides us not only a constructive illustration for bundles, but also an effective and rigorous technique of rule induction to reason about properties of bundles. With this induction principle, we can prove that our bundle model is sound in the sense that a bundle is a causally well-founded graph. This approach also gives an alternative to rigorously prove a generalized version of authentication tests. To illustrate the applicability of our approach, we have performed case studies on verification of secrecy and authentication properties of the Needham-Schroeder-Lowe and Otway-Rees protocols. Our approach has been mechanized using Isabelle/HOL. © 2011 British Computer Society. |
| Indexed Type | EI |
| Department | (1) The State Key Laboratory of Computer Science and The State Key Laboratory of Information Security, Institute of Software, Chinese Academy of Sciences, P.O. Box 8717, Beijing, China; (2) Faculte des Sciences de la Technologie et de la Communication, Computer Science and Communications, Université du Luxembourg, Luxembourg, Belgium |
| WOS ID | WOS:000319912300001 |
| Citation statistics | |
| Content Type | 期刊论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/14069 |
| Collection | 基础软件与系统重点实验室 |
| Recommended Citation GB/T 7714 | Li Yongjian,Pang Jun. an inductive approach to strand spaces[J]. Formal Aspects of Computing,2011(1):1-37. |
| APA | Li Yongjian,&Pang Jun.(2011).an inductive approach to strand spaces.Formal Aspects of Computing(1),1-37. |
| MLA | Li Yongjian,et al."an inductive approach to strand spaces".Formal Aspects of Computing .1(2011):1-37. |
| Files in This Item: | ||||||
| File Name/Size | DocType | Version | Access | License | ||
| An inductive approac（784KB） | 开放获取 | -- | Application Full Text | |||
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment