Computational semantics for first-order logical analysis of cryptographic protocols

Gergei Bana, Koji Hasebe, Mitsuhiro Okada

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

4 Citations (Scopus)

Abstract

This paper is concerned about relating formal and computational models of cryptography in case of active adversaries when formal security analysis is done with first order logic As opposed to earlier treatments, we introduce a new, fully probabilistic method to assign computational semantics to the syntax. The idea is to make use of the usual mathematical treatment of stochastic processes, hence be able to treat arbitrary probability distributions, non-negligible probability of collision, causal dependence or independence, and so on. We present this via considering a simple example of such a formal model, the Basic Protocol Logic by K. Hasebe and M. Okada [20], but we think the technique is suitable for a wide range of formal methods for protocol correctness proofs. We first review our framework of proof-system, BPL, for proving correctness of authentication protocols, and provide computational semantics. Then we give a full proof of the soundness theorem. We also comment on the differences of our method and that of Computational PCL.

Original languageEnglish
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Pages33-56
Number of pages24
Volume5458 LNCS
DOIs
Publication statusPublished - 2009

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5458 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Fingerprint

Cryptographic Protocols
Semantics
Formal Model
First-order
Network protocols
Correctness
Telescoping a series
Authentication Protocol
Formal methods
Security Analysis
Proof System
Probabilistic Methods
Formal Analysis
Formal Methods
Soundness
First-order Logic
Random processes
Cryptography
Computational Model
Probability distributions

Keywords

  • Computational semantics
  • Cryptographic protocols
  • First order logic
  • Formal methods

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Bana, G., Hasebe, K., & Okada, M. (2009). Computational semantics for first-order logical analysis of cryptographic protocols. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5458 LNCS, pp. 33-56). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5458 LNCS). https://doi.org/10.1007/978-3-642-02002-5_3

Computational semantics for first-order logical analysis of cryptographic protocols. / Bana, Gergei; Hasebe, Koji; Okada, Mitsuhiro.

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 5458 LNCS 2009. p. 33-56 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5458 LNCS).

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

Bana, G, Hasebe, K & Okada, M 2009, Computational semantics for first-order logical analysis of cryptographic protocols. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). vol. 5458 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 5458 LNCS, pp. 33-56. https://doi.org/10.1007/978-3-642-02002-5_3
Bana G, Hasebe K, Okada M. Computational semantics for first-order logical analysis of cryptographic protocols. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 5458 LNCS. 2009. p. 33-56. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-02002-5_3
Bana, Gergei ; Hasebe, Koji ; Okada, Mitsuhiro. / Computational semantics for first-order logical analysis of cryptographic protocols. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 5458 LNCS 2009. pp. 33-56 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{01546597d8d14a35a7ad668a7aedb86f,
title = "Computational semantics for first-order logical analysis of cryptographic protocols",
abstract = "This paper is concerned about relating formal and computational models of cryptography in case of active adversaries when formal security analysis is done with first order logic As opposed to earlier treatments, we introduce a new, fully probabilistic method to assign computational semantics to the syntax. The idea is to make use of the usual mathematical treatment of stochastic processes, hence be able to treat arbitrary probability distributions, non-negligible probability of collision, causal dependence or independence, and so on. We present this via considering a simple example of such a formal model, the Basic Protocol Logic by K. Hasebe and M. Okada [20], but we think the technique is suitable for a wide range of formal methods for protocol correctness proofs. We first review our framework of proof-system, BPL, for proving correctness of authentication protocols, and provide computational semantics. Then we give a full proof of the soundness theorem. We also comment on the differences of our method and that of Computational PCL.",
keywords = "Computational semantics, Cryptographic protocols, First order logic, Formal methods",
author = "Gergei Bana and Koji Hasebe and Mitsuhiro Okada",
year = "2009",
doi = "10.1007/978-3-642-02002-5_3",
language = "English",
isbn = "9783642020018",
volume = "5458 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "33--56",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

}

TY - GEN

T1 - Computational semantics for first-order logical analysis of cryptographic protocols

AU - Bana, Gergei

AU - Hasebe, Koji

AU - Okada, Mitsuhiro

PY - 2009

Y1 - 2009

N2 - This paper is concerned about relating formal and computational models of cryptography in case of active adversaries when formal security analysis is done with first order logic As opposed to earlier treatments, we introduce a new, fully probabilistic method to assign computational semantics to the syntax. The idea is to make use of the usual mathematical treatment of stochastic processes, hence be able to treat arbitrary probability distributions, non-negligible probability of collision, causal dependence or independence, and so on. We present this via considering a simple example of such a formal model, the Basic Protocol Logic by K. Hasebe and M. Okada [20], but we think the technique is suitable for a wide range of formal methods for protocol correctness proofs. We first review our framework of proof-system, BPL, for proving correctness of authentication protocols, and provide computational semantics. Then we give a full proof of the soundness theorem. We also comment on the differences of our method and that of Computational PCL.

AB - This paper is concerned about relating formal and computational models of cryptography in case of active adversaries when formal security analysis is done with first order logic As opposed to earlier treatments, we introduce a new, fully probabilistic method to assign computational semantics to the syntax. The idea is to make use of the usual mathematical treatment of stochastic processes, hence be able to treat arbitrary probability distributions, non-negligible probability of collision, causal dependence or independence, and so on. We present this via considering a simple example of such a formal model, the Basic Protocol Logic by K. Hasebe and M. Okada [20], but we think the technique is suitable for a wide range of formal methods for protocol correctness proofs. We first review our framework of proof-system, BPL, for proving correctness of authentication protocols, and provide computational semantics. Then we give a full proof of the soundness theorem. We also comment on the differences of our method and that of Computational PCL.

KW - Computational semantics

KW - Cryptographic protocols

KW - First order logic

KW - Formal methods

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

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

U2 - 10.1007/978-3-642-02002-5_3

DO - 10.1007/978-3-642-02002-5_3

M3 - Conference contribution

AN - SCOPUS:67650269836

SN - 9783642020018

VL - 5458 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 33

EP - 56

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

ER -