IACR paper details
Title  Computational Semantics for Basic Protocol Logic  A Stochastic Approach 

Booktitle  IACR Eprint archive 

Pages  

Year  2007 

URL  http://eprint.iacr.org/2007/156 

Author  Gergei Bana 

Author  Koji Hasebe 

Author  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 bitstrings on individual traces instead of occurrences of probability distributions of bitstrings 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, nonnegligible probability of collision, causal dependence or independence.


Search for the paper
@misc{eprint200713438,
title={Computational Semantics for Basic Protocol Logic  A Stochastic Approach},
booktitle={IACR Eprint archive},
keywords={foundations / formal methods, computational methods, soundness, first order logic, active adversaries},
url={http://eprint.iacr.org/2007/156},
note={ bana@math.upenn.edu 13812 received 27 Apr 2007, last revised 25 Oct 2007},
author={Gergei Bana and Koji Hasebe and Mitsuhiro Okada},
year=2007
}
Download a complete BibTeX file.