Computational semantics for basic protocol logic a stochastic approach

Gergei Bana, Koji Hasebe, Mitsuhiro Okada

Research output: Contribution to journalArticle

Abstract

This paper relates formal and computational models of cryptography in case of active adversaries when formal security analysis is done with first order logic. Instead of the way Datta et al. defined computational semantics to their Protocol Composition Logic, we introduce a new, fully probabilistic method to assign computational semantics to the syntax. We present this via considering a simple example of such a formal model, the Basic Protocol Logic by K. Hasebe and M. Okada [7] , but the technique is suitable for extensions to more complex situations such as PCL. We make use of the usual mathematical treatment of stochastic processes, hence are able to treat arbitrary probability distributions, non-negligible probability of collision, causal dependence or independence.

Original languageEnglish
Pages (from-to)86-94
Number of pages9
JournalLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4846 LNCS
Publication statusPublished - 2007

Fingerprint

Formal Model
Semantics
Logic
Security Analysis
Probabilistic Methods
Formal Analysis
First-order Logic
Random processes
Cryptography
Computational Model
Probability distributions
Stochastic Processes
Assign
Probability Distribution
Collision
Arbitrary
Chemical analysis
Independence
Syntax

Keywords

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

ASJC Scopus subject areas

  • Computer Science(all)
  • Biochemistry, Genetics and Molecular Biology(all)
  • Theoretical Computer Science

Cite this

@article{b6a897780da240ff95040cd511b3728f,
title = "Computational semantics for basic protocol logic a stochastic approach",
abstract = "This paper relates formal and computational models of cryptography in case of active adversaries when formal security analysis is done with first order logic. Instead of the way Datta et al. defined computational semantics to their Protocol Composition Logic, we introduce a new, fully probabilistic method to assign computational semantics to the syntax. We present this via considering a simple example of such a formal model, the Basic Protocol Logic by K. Hasebe and M. Okada [7] , but the technique is suitable for extensions to more complex situations such as PCL. We make use of the usual mathematical treatment of stochastic processes, hence are able to treat arbitrary probability distributions, non-negligible probability of collision, causal dependence or independence.",
keywords = "Computational semantics, Cryptographic protocols, First order logic, Formal methods",
author = "Gergei Bana and Koji Hasebe and Mitsuhiro Okada",
year = "2007",
language = "English",
volume = "4846 LNCS",
pages = "86--94",
journal = "Lecture Notes in Computer Science",
issn = "0302-9743",
publisher = "Springer Verlag",

}

TY - JOUR

T1 - Computational semantics for basic protocol logic a stochastic approach

AU - Bana, Gergei

AU - Hasebe, Koji

AU - Okada, Mitsuhiro

PY - 2007

Y1 - 2007

N2 - This paper relates formal and computational models of cryptography in case of active adversaries when formal security analysis is done with first order logic. Instead of the way Datta et al. defined computational semantics to their Protocol Composition Logic, we introduce a new, fully probabilistic method to assign computational semantics to the syntax. We present this via considering a simple example of such a formal model, the Basic Protocol Logic by K. Hasebe and M. Okada [7] , but the technique is suitable for extensions to more complex situations such as PCL. We make use of the usual mathematical treatment of stochastic processes, hence are able to treat arbitrary probability distributions, non-negligible probability of collision, causal dependence or independence.

AB - This paper relates formal and computational models of cryptography in case of active adversaries when formal security analysis is done with first order logic. Instead of the way Datta et al. defined computational semantics to their Protocol Composition Logic, we introduce a new, fully probabilistic method to assign computational semantics to the syntax. We present this via considering a simple example of such a formal model, the Basic Protocol Logic by K. Hasebe and M. Okada [7] , but the technique is suitable for extensions to more complex situations such as PCL. We make use of the usual mathematical treatment of stochastic processes, hence are able to treat arbitrary probability distributions, non-negligible probability of collision, causal dependence or independence.

KW - Computational semantics

KW - Cryptographic protocols

KW - First order logic

KW - Formal methods

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

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

M3 - Article

AN - SCOPUS:38349081077

VL - 4846 LNCS

SP - 86

EP - 94

JO - Lecture Notes in Computer Science

JF - Lecture Notes in Computer Science

SN - 0302-9743

ER -