Computationally complete symbolic attacker and key exchange

Gergei Bana, Koji Hasebe, Mitsuhiro Okada

Research output: Chapter in Book/Report/Conference proceedingConference contribution

4 Citations (Scopus)

Abstract

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.

Original languageEnglish
Title of host publicationProceedings of the ACM Conference on Computer and Communications Security
Pages1231-1246
Number of pages16
DOIs
Publication statusPublished - 2013
Event2013 ACM SIGSAC Conference on Computer and Communications Security, CCS 2013 - Berlin, Germany
Duration: 2013 Nov 42013 Nov 8

Other

Other2013 ACM SIGSAC Conference on Computer and Communications Security, CCS 2013
CountryGermany
CityBerlin
Period13/11/413/11/8

Fingerprint

Cryptography
Network protocols

Keywords

  • computational soundness
  • security protocols

ASJC Scopus subject areas

  • Software
  • Computer Networks and Communications

Cite this

Bana, G., Hasebe, K., & Okada, M. (2013). Computationally complete symbolic attacker and key exchange. In Proceedings of the ACM Conference on Computer and Communications Security (pp. 1231-1246) https://doi.org/10.1145/2508859.2516710

Computationally complete symbolic attacker and key exchange. / Bana, Gergei; Hasebe, Koji; Okada, Mitsuhiro.

Proceedings of the ACM Conference on Computer and Communications Security. 2013. p. 1231-1246.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Bana, G, Hasebe, K & Okada, M 2013, Computationally complete symbolic attacker and key exchange. in Proceedings of the ACM Conference on Computer and Communications Security. pp. 1231-1246, 2013 ACM SIGSAC Conference on Computer and Communications Security, CCS 2013, Berlin, Germany, 13/11/4. https://doi.org/10.1145/2508859.2516710
Bana G, Hasebe K, Okada M. Computationally complete symbolic attacker and key exchange. In Proceedings of the ACM Conference on Computer and Communications Security. 2013. p. 1231-1246 https://doi.org/10.1145/2508859.2516710
Bana, Gergei ; Hasebe, Koji ; Okada, Mitsuhiro. / Computationally complete symbolic attacker and key exchange. Proceedings of the ACM Conference on Computer and Communications Security. 2013. pp. 1231-1246
@inproceedings{9110b7f632c14dad936fba1469dcf6b6,
title = "Computationally complete symbolic attacker and key exchange",
abstract = "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.",
keywords = "computational soundness, security protocols",
author = "Gergei Bana and Koji Hasebe and Mitsuhiro Okada",
year = "2013",
doi = "10.1145/2508859.2516710",
language = "English",
isbn = "9781450324779",
pages = "1231--1246",
booktitle = "Proceedings of the ACM Conference on Computer and Communications Security",

}

TY - GEN

T1 - Computationally complete symbolic attacker and key exchange

AU - Bana, Gergei

AU - Hasebe, Koji

AU - Okada, Mitsuhiro

PY - 2013

Y1 - 2013

N2 - 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.

AB - 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.

KW - computational soundness

KW - security protocols

UR - http://www.scopus.com/inward/record.url?scp=84889060853&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84889060853&partnerID=8YFLogxK

U2 - 10.1145/2508859.2516710

DO - 10.1145/2508859.2516710

M3 - Conference contribution

AN - SCOPUS:84889060853

SN - 9781450324779

SP - 1231

EP - 1246

BT - Proceedings of the ACM Conference on Computer and Communications Security

ER -