Computational Indistinguishability Logic

被引：24

作者：

Barthe, Gilles ^{[1
]}

Daubignard, Marion ^{[2
]}

Kapron, Bruce ^{[3
]}

Lakhnech, Yassine ^{[2
]}

机构：

[1] IMDEA Software, Madrid, Spain

[2] Univ Grenoble, VERIMAG, Grenoble, France

[3] Univ Victoria, Victoria, BC V8W 2Y2, Canada

来源：

PROCEEDINGS OF THE 17TH ACM CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY (CCS'10) | 2010年

关键词：

Logic; provable security; signature schemes; random oracle; bisimulation; determinization; EXACT SECURITY; SOUNDNESS; PROTOCOLS;

D O I：

10.1145/1866307.1866350

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

Computational Indistinguishability Logic (CIL) is a logic for reasoning about cryptographic primitives in computational models. It captures reasoning patterns that are common in provable security, such as simulations and reductions. CIL is sound for the standard model, but also supports reasoning in the random oracle and other idealized models. We illustrate the benefits of CIL by formally proving the security of the probabilistic signature scheme (PSS).

引用

页码：375 / 386

页数：12

共 40 条

[1] Reconciling two views of cryptography (The computational soundness of formal encryption) [J].

Abadi, M ;

Rogaway, P .

JOURNAL OF CRYPTOLOGY, 2002, 15 (02) :103-127

[2] A calculus for cryptographic protocols: The spi calculus [J].

Abadi, M ;

Gordon, AD .

INFORMATION AND COMPUTATION, 1999, 148 (01) :1-70

[3]

[Anonymous], 2009, P TYP LAMB CALC APPL

[4]

[Anonymous], P 23 NAT C ART INT A

[5]

[Anonymous], 2004, 2004332 CRYPT EPRINT

[6]

Backes Michael, P LPAR 08, P353

[7]

Backes Michael., 2003, CCS 03, P220, DOI [10.1145/948109.948140, DOI 10.1145/948109.948140]

[8] Formal Certification of Code-Based Cryptographic Proofs [J].

Barthe, Gilles ;

Gregoire, Benjamin ;

Beguelin, Santiago Zanella .

ACM SIGPLAN NOTICES, 2009, 44 (01) :90-101

[9]

Barthe Gilles, 2010, PROVABLE SECUR UNPUB

[10]

Barthe Gilles, 2010, LECT NOTES IN PRESS

← 1 2 3 4 →