an inductive approach to strand spaces

	an inductive approach to strand spaces
	Li Yongjian; Pang Jun
	2011
发表期刊	Formal Aspects of Computing
ISSN	9345043
期号	1 页码:1-37
摘要	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.
收录类别	EI
部门归属	(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记录号	WOS:000319912300001
引用统计	被引频次：6[WOS] [WOS记录] [WOS相关记录]
内容类型	期刊论文
URI标识	http://ir.iscas.ac.cn/handle/311060/14069
专题	基础软件与系统重点实验室
推荐引用方式 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.

条目包含的文件
文件名称/大小	文献类型	版本类型	开放类型	使用许可
An inductive approac（784KB）			开放获取	--	请求全文