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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Abadi, M., Baudet, M., Warinschi, B.: Guessing attacks and the computational soundness of static equivalence. In: Aceto, L., Ingólfsdóttir, A. (eds.) FOSSACS 2006. LNCS, vol. 3921, pp. 398–412. Springer, Heidelberg (2006)
Abadi, M., Rogaway, P.: Reconciling two views of cryptography. Journal of Cryptology 15(2), 103–127 (2002)
Adão, P., Bana, G., Herzog, J., Scedrov, A.: Soundness of formal encryption in the presence of key-cycles. In: di Vimercati, S.d.C., Syverson, P.F., Gollmann, D. (eds.) ESORICS 2005. LNCS, vol. 3679, pp. 374–396. Springer, Heidelberg (2005)
Adão, P., Bana, G., Scedrov, A.: Computational and information-theoretic soundness and completeness of formal encryption. In: Proceedings of CSFW 2005, Aix-en-Provence, France, June 20–22, pp. 170–184. IEEE Computer Society Press, Los Alamitos (2005)
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)
Bana, G., Hasebe, K., Okada, M.: Computational semantics for basic protocol logic - a stochastic approach. In: Cervesato, I. (ed.) ASIAN 2007. LNCS, vol. 4846, pp. 86–94. Springer, Heidelberg (2007)
Baudet, M., Cortier, V., Kremer, S.: Computationally sound implementations of equational theories against passive adversaries. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 652–663. Springer, Heidelberg (2005)
Bellare, M., Boldyreva, A., Micali, S.: Public-key encryption in a multi-user setting. In: Preneel, B. (ed.) EUROCRYPT 2000. LNCS, vol. 1807, pp. 259–274. Springer, Heidelberg (2000)
Canetti, R., Herzog, J.: Universally composable symbolic analysis of mutual authentication and key exchange protocols. In: Halevi, S., Rabin, T. (eds.) TCC 2006. LNCS, vol. 3876, pp. 380–403. Springer, Heidelberg (2006)
Cervesato, I., Meadows, C., Pavlovic, D.: An encapsulated authentication logic for reasoning about key distribution protocols. In: Proceedings of CSFW 2005, pp. 48–61 (2005)
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)
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)
Datta, A., Derek, A., Mitchell, J.C., Roy, A.: Protocol composition logic (pcl). Electron. Notes Theor. Comput. Sci. 172, 311–358 (2007)
Dolev, D., Yao, A.C.: On the security of public-key protocols. IEEE Transactions on Information Theory 29(2), 198–208 (1983); Preliminary version presented at FOCS 1981
Durgin, N.A., Mitchell, J.C., Pavlovic, D.: A compositional logic for proving security properties of protocols. Journal of Computer Security 11, 677–721 (2003)
Goldwasser, S., Micali, S.: Probabilistic encryption. Journal of Computer and Systems Sciences 28(2), 270–299 (1984); Preliminary version presented at STOC (1982)
Guttman, J.D., Thayer Fábrega, F.J.: Authentication tests. In: IEEE Symposium on Security and Privacy, pp. 96–109 (2002)
Guttman, J.D., Thayer, F.J., Zuck, L.D.: The faithfulness of abstract protocol analysis: Message authentication. In: Proceedings of CCS 2001, November 05–08, pp. 186–195. ACM Press, New York (2001)
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 Science, Amsterdam (2005), http://dx.doi.org/10.1016/j.entcs.2005.06.038
Laud, P.: Symmetric encryption in automatic analyses for confidentiality against active adversaries. In: Proceedings of S&P 2004, May 9–12, pp. 71–85. IEEE Computer Society Press, Los Alamitos (2004)
Lowe, G.: A hierarchy of authentication specifications. In: PCSFW: Proceedings of The 10th Computer Security Foundations Workshop. IEEE Computer Society Press, Los Alamitos (1997)
Micciancio, D., Warinschi, B.: Completeness theorems for the Abadi-Rogaway logic of encrypted expressions. Journal of Computer Security 12(1), 99–130 (2004)
Needham, R., Schroeder, M.: Using encryption for authentication in large networks of computers. Communications of the ACM 21(12), 993–999 (1978)
Woo, T., Lam, S.: Verifying authentication protocols: Methodology and example. In: Proceedings of the International Conference on Network Protocols (1993)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Bana, G., Hasebe, K., Okada, M. (2009). Computational Semantics for First-Order Logical Analysis of Cryptographic Protocols. In: Cortier, V., Kirchner, C., Okada, M., Sakurada, H. (eds) Formal to Practical Security. Lecture Notes in Computer Science, vol 5458. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02002-5_3
Download citation
DOI: https://doi.org/10.1007/978-3-642-02002-5_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02001-8
Online ISBN: 978-3-642-02002-5
eBook Packages: Computer ScienceComputer Science (R0)