Computational Semantics for Basic Protocol Logic – A Stochastic Approach

  • Gergei Bana
  • Koji Hasebe
  • Mitsuhiro Okada
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4846)


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.


cryptographic protocols formal methods first order logic computational semantics 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abadi, M., Rogaway, P.: Reconciling two views of cryptography. Journal of Cryptology 15(2), 103–127 (2002)zbMATHMathSciNetGoogle Scholar
  2. 2.
    Backes, M., Pfitzmann, B., Waidner, M.: A composable cryptographic library with nested operations. In: Proceedings of CCS 2003, pp. 220–230. ACM Press, New York (2003)CrossRefGoogle Scholar
  3. 3.
    Bana, G., Hasebe, K., Okada, M.: Computational semantics for bpl - a stochastic approach. Available at IACR ePrint Archive, Report 2007/156Google Scholar
  4. 4.
    Datta, A., Derek, A., Mitchell, J.C., Pavlovic, D.: A derivation system and compositional logic for security protocols. Journal of Computer Security 13, 423–482 (2005)Google Scholar
  5. 5.
    Datta, A., Derek, A., Mitchell, J.C., Shmatikov, V., Turuani, M.: Probabilistic polynomial-time semantics for a protocol security logic. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 16–29. Springer, Heidelberg (2005)Google Scholar
  6. 6.
    Dolev, D., Yao, A.C.: On the security of public-key protocols. IEEE Transactions on Information Theory, 29(2), 198–208, March, Preliminary version presented at FOCS 1981 (1983)Google Scholar
  7. 7.
    Hasebe, K., Okada, M.: Completeness and counter-example generations of a basic protocol logic. In: Proceedings of RULE 2005, vol. 147(1), pp. 73–92. Elsevier, Amsterdam (2005), Available also at: Google Scholar
  8. 8.
    Micciancio, D., Warinschi, B.: Soundness of formal encryption in the presence of active adversaries. In: Naor, M. (ed.) TCC 2004. LNCS, vol. 2951, pp. 133–151. Springer, Heidelberg (2004)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2007

Authors and Affiliations

  • Gergei Bana
    • 1
  • Koji Hasebe
    • 2
  • Mitsuhiro Okada
    • 3
  1. 1.Dept of Mathematics, Tulane University, New Orleans, LAUSA
  2. 2.Research Center for Verification and Semantics, AIST, OsakaJapan
  3. 3.Department of Philosophy, Keio University, TokyoJapan

Personalised recommendations