Abstract
We introduce a probabilistic framework for the automated analysis of security protocols. Our framework provides a general method for expressing properties of cryptographic primitives, modeling an attacker more powerful than conventional Dolev-Yao attackers. It allows modeling equational properties of cryptographic primitives as well as property statements about their weaknesses, e.g. primitives leaking partial information about messages or the use of weak random generation algorithms. These properties can be used to automatically find attacks and estimate their success probability. Existing symbolic methods can neither model such properties nor find such attacks. We show that the probability estimates we obtain are negligibly different from those yielded by a generalized random oracle model based on sampling terms into bitstrings while respecting the stipulated properties of cryptographic primitives.
As case studies, we use a prototype implementation of our framework to model non-trivial properties of RSA encryption and automatically estimate the probability of off-line guessing attacks on the EKE protocol.
Chapter PDF
Similar content being viewed by others
References
Cortier, V., Delaune, S., Lafourcade, P.: A survey of algebraic properties used in cryptographic protocols. J. Comput. Secur. 14, 1–43 (2006)
Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: Proc. of the 14th IEEE Workshop on Computer Security Foundations, CSFW 2001, pp. 82–96. IEEE Computer Society, Washington, DC (2001)
Schmidt, B., Meier, S., Cremers, C.J.F., Basin, D.A.: Automated analysis of Diffie-Hellman protocols and advanced security properties. In: Chong, S. (ed.) CSF, pp. 78–94. IEEE (2012)
Goldwasser, S., Micali, S.: Probabilistic encryption. J. Comput. Syst. Sci. 28(2), 270–299 (1984)
Bellare, M., Rogaway, P.: Entity authentication and key distribution. In: Stinson, D.R. (ed.) CRYPTO 1993. LNCS, vol. 773, pp. 232–249. Springer, Heidelberg (1994)
Blanchet, B.: Security protocol verification: Symbolic and computational models. In: Degano, Guttman (eds.) [30], pp. 3–29
Abadi, M., Rogaway, P.: Reconciling two views of cryptography (the computational soundness of formal encryption). J. Cryptology 20(3), 395 (2007)
Backes, M., Malik, A., Unruh, D.: Computational soundness without protocol restrictions. In: Yu, T., Danezis, G., Gligor, V.D. (eds.) ACM Conference on Computer and Communications Security, pp. 699–711. ACM (2012)
Backes, M., Pfitzmann, B., Waidner, M.: A composable cryptographic library with nested operations. In: Jajodia, S., Atluri, V., Jaeger, T. (eds.) ACM Conference on Computer and Communications Security, pp. 220–230. ACM (2003)
Comon-Lundh, H., Cortier, V.: Computational soundness of observational equivalence. In: Ning, P., Syverson, P.F., Jha, S. (eds.) ACM Conference on Computer and Communications Security, pp. 109–118. ACM (2008)
Blanchet, B.: A computationally sound mechanized prover for security protocols. IEEE Trans. Dependable Sec. Comput. 5(4), 193–207 (2008)
Barthe, G., Grégoire, B., Béguelin, S.Z.: Formal certification of code-based cryptographic proofs. In: Shao, Z., Pierce, B.C. (eds.) POPL, pp. 90–101. ACM (2009)
Barthe, G., Crespo, J.M., Grégoire, B., Kunz, C., Zanella Béguelin, S.: Computer-aided cryptographic proofs. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 11–27. Springer, Heidelberg (2012)
Bana, G., Comon-Lundh, H.: Towards unconditional soundness: Computationally complete symbolic attacker. In: Degano, Guttman (eds.) [30], pp. 189–208
Comon-Lundh, H., Cortier, V., Scerri, G.: Tractable inference systems: An extension with a deducibility predicate. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 91–108. Springer, Heidelberg (2013)
Baudet, M.: Deciding security of protocols against off-line guessing attacks. In: Proceedings of the 12th ACM Conference on Computer and Communications Security, CCS 2005, pp. 16–25. ACM, New York (2005)
Corin, R., Doumen, J., Etalle, S.: Analysing password protocol security against off-line dictionary attacks. Electron. Notes Theor. Comput. Sci. 121, 47–63 (2005)
Halevi, S., Krawczyk, H.: Public-key cryptography and password protocols. ACM Trans. Inf. Syst. Secur. 2(3), 230–268 (1999)
Abadi, M., Warinschi, B.: Password-based encryption analyzed. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 664–676. Springer, Heidelberg (2005)
Abadi, M., Baudet, M., Warinschi, B.: Guessing attacks and the computational soundness of static equivalence. Journal of Computer Security, 909–968 (December 2010)
Sectools.org: Top 125 network security tools (January 2013), http://sectools.org/tag/crackers/
Bellovin, S.M., Merritt, M.: Encrypted Key Exchange: Password-based protocols secure against dictionary attacks. In: IEEE Symposium on Research in Security and Privacy, pp. 72–84 (1992)
Munilla, J., Peinado, A.: Off-line password-guessing attack to Peyravian-Jeffries’s remote user authentication protocol. Computer Communications 30(1), 52–54 (2006)
Köpf, B., Basin, D.A.: An information-theoretic model for adaptive side-channel attacks. In: CCS 2007, pp. 286–296. ACM (2007)
(2013), http://www.infsec.ethz.ch/people/brunoco/infsec/people/brunoco/esorics13_tech.pdf
Abadi, M., Cortier, V.: Deciding knowledge in security protocols under equational theories. Theor. Comput. Sci. 367, 2–32 (2006)
Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: POPL 2001, pp. 104–115. ACM, New York (2001)
(2013), http://www.infsec.ethz.ch/people/brunoco/prob_rsa.tar.gz
Montalto, B., Caleiro, C.: Modeling and reasoning about an attacker with cryptanalytical capabilities. ENTCS 253(3), 143–165 (2009)
Degano, P., Guttman, J.D. (eds.): POST 2012. LNCS, vol. 7215. Springer, Heidelberg (2012)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Conchinha, B., Basin, D., Caleiro, C. (2013). Symbolic Probabilistic Analysis of Off-Line Guessing. In: Crampton, J., Jajodia, S., Mayes, K. (eds) Computer Security – ESORICS 2013. ESORICS 2013. Lecture Notes in Computer Science, vol 8134. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40203-6_21
Download citation
DOI: https://doi.org/10.1007/978-3-642-40203-6_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-40202-9
Online ISBN: 978-3-642-40203-6
eBook Packages: Computer ScienceComputer Science (R0)