the computational slr: a logic for reasoning about computational     indistinguishability

ISCAS OpenIR > 2009年期刊/会议论文

	the computational slr: a logic for reasoning about computational indistinguishability
	Zhang Yu
	2009
会议名称	9th International Conference on Typed Lambda Calculi and Applications
会议录名称	Proceedings of the 9th International Conference on Typed Lambda Calculi and Applications
页码	401-415
会议日期	JUL 01-03,
会议地点	Brasilia, BRAZIL
收录类别	istp,acm,sci
出版地	HEIDELBERGER PLATZ 3, D-14197 BERLIN, GERMANY
出版者	TYPED LAMBDA CALCULI AND APPLICATIONS, PROCEEDINGS
ISSN	0302-9743
ISBN	978-3-642-02272-2
部门归属	CAS, Inst Software, Comp Sci Lab, Beijing, Peoples R China.
摘要	Computational indistinguishability is a notion in complexity-theoretic cryptography and is used to define many security criteria. However, in traditional cryptography, proving computational indistinguishability is usually informal and becomes error-prone when cryptographic constructions are complex. This paper presents a formal proof system based on an extension of Hofmanns SLR language, which can capture probabilistic polynomial-time computations through typing and is sufficient for expressing cryptographic constructions. We in particular define rules that justify directly the computational indistinguishability between programs and prove that these rules are sound with respect to the set-theoretic semantics, hence the standard definition of security. We also show that it is applicable in cryptography by verifying, in our proof system, Goldreich and Micalis construction of pseudorandom generator.
主办者	Univ Brasilia, Brazilian Counsel Technol & Sci Dept, CNPq, Brazilian Coordinat Improvement Higher Educ Personnel, CAPES, Fed District Res Fdn, FAPDF
语种	英语
内容类型	会议论文
URI标识	http://ir.iscas.ac.cn/handle/311060/8320
专题	2009年期刊/会议论文
推荐引用方式 GB/T 7714	Zhang Yu. the computational slr: a logic for reasoning about computational indistinguishability[C]. HEIDELBERGER PLATZ 3, D-14197 BERLIN, GERMANY:TYPED LAMBDA CALCULI AND APPLICATIONS, PROCEEDINGS,2009:401-415.