Paper 2007/156

Computational Semantics for Basic Protocol Logic - A Stochastic Approach

Gergei Bana, Koji Hasebe, and Mitsuhiro Okada

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. We first present a criticism of the way Datta et al. defined computational semantics to their Protocol Composition Logic, concluding that problems arise from focusing on occurrences of bit-strings on individual traces instead of occurrences of probability distributions of bit-strings across the distribution of traces. We therefore 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 of K. Hasebe and M. Okada, but the technique is suitable for extensions to more complex situations such as PCL. 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.

Note: Added some final fixes.

Metadata
Available format(s)
PDF
Category
Foundations
Publication info
Published elsewhere. Unknown where it was published
Keywords
formal methodscomputational methodssoundnessfirst order logicactive adversaries
Contact author(s)
bana @ math upenn edu
History
2009-02-17: last of 6 revisions
2007-05-07: received
See all versions
Short URL
https://ia.cr/2007/156
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2007/156,
      author = {Gergei Bana and Koji Hasebe and Mitsuhiro Okada},
      title = {Computational Semantics for Basic Protocol Logic - A Stochastic Approach},
      howpublished = {Cryptology {ePrint} Archive, Paper 2007/156},
      year = {2007},
      url = {https://eprint.iacr.org/2007/156}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.