Computationally complete symbolic attacker and key exchange

Gergei Bana, Koji Hasebe, Mitsuhiro Okada

研究成果: Conference contribution

5 被引用数 (Scopus)

抄録

Recently, Bana and Comon-Lundh introduced the notion of computationally complete symbolic attacker to deliver unconditional computational soundness to symbolic protocol verification. First we explain the relationship between their technique and Fitting's embedding of classical logic into S4. Then, based on predicates for "key usability", we provide an axiomatic system in their framework to handle secure encryption when keys are allowed to be sent. We examine both IND-CCA2 and KDM-CCA2 encryptions, both symmetric and asymmetric situations. For unforgeability, we consider INT-CTXT encryptions. This technique does not require the usual limitations of computational soundness such as the absence of dynamic corruption, the absence of key-cycles or unambiguous parsing of bit strings. In particular, if a key-cycle possibly corrupts CCA2 encryption, our technique delivers an attack. If it does not endanger security, the security proof goes through. We illustrate how our notions can be applied in protocol proofs.

本文言語English
ホスト出版物のタイトルCCS 2013 - Proceedings of the 2013 ACM SIGSAC Conference on Computer and Communications Security
ページ1231-1246
ページ数16
DOI
出版ステータスPublished - 2013
外部発表はい
イベント2013 ACM SIGSAC Conference on Computer and Communications Security, CCS 2013 - Berlin, Germany
継続期間: 2013 11月 42013 11月 8

出版物シリーズ

名前Proceedings of the ACM Conference on Computer and Communications Security
ISSN(印刷版)1543-7221

Other

Other2013 ACM SIGSAC Conference on Computer and Communications Security, CCS 2013
国/地域Germany
CityBerlin
Period13/11/413/11/8

ASJC Scopus subject areas

  • ソフトウェア
  • コンピュータ ネットワークおよび通信

フィンガープリント

「Computationally complete symbolic attacker and key exchange」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル