Abstract
We present a framework for modeling adversaries in security protocol analysis, ranging from a Dolev-Yao style adversary to more powerful adversaries who can reveal different parts of principals’ states during protocol execution. Our adversary models unify and generalize many existing security notions from both the computational and symbolic settings. We extend an existing symbolic protocol-verification tool with our adversary models, resulting in the first tool that systematically supports notions such as weak perfect forward secrecy, key compromise impersonation, and adversaries capable of state-reveal queries. In case studies, we automatically find new attacks and rediscover known attacks that previously required detailed manual analysis.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abadi, M., Blanchet, B., Fournet, C.: Just Fast Keying in the Pi calculus. ACM Transactions on Information and System Security (TISSEC) 10(3), 1–59 (2007)
Basin, D., Cremers, C.: Degrees of security: Protocol guarantees in the face of compromising adversaries. In: 19th EACSL Annual Conferences on Computer Science Logic (CSL 2010). Advanced Research in Computing and Software Science, Springer, Heidelberg (2010) (to appear)
Bellare, M., Pointcheval, D., Rogaway, P.: Authenticated key exchange secure against dictionary attacks. In: Preneel, B. (ed.) EUROCRYPT 2000. LNCS, vol. 1807, pp. 139–155. Springer, Heidelberg (2000)
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)
Bellare, M., Rogaway, P.: Provably secure session key distribution: the three party case. In: STOC 1995, pp. 57–66. ACM Press, New York (1995)
Blanchet, B.: A computationally sound mechanized prover for security protocols. In: IEEE Symposium on Security and Privacy, pp. 140–154 (May 2006)
Bresson, E., Manulis, M.: Securing group key exchange against strong corruptions. In: ASIACCS, pp. 249–260. ACM, New York (2008)
Bresson, E., Manulis, M., Schwenk, J.: On security models and compilers for group key exchange protocols. In: Miyaji, A., Kikuchi, H., Rannenberg, K. (eds.) IWSEC 2007. LNCS, vol. 4752, pp. 292–307. Springer, Heidelberg (2007)
Canetti, R., Krawczyk, H.: Analysis of key-exchange protocols and their use for building secure channels. In: Pfitzmann, B. (ed.) EUROCRYPT 2001. LNCS, vol. 2045, pp. 453–474. Springer, Heidelberg (2001)
Choo, K.-K., Boyd, C., Hitchcock, Y.: Examining indistinguishability-based proof models for key establishment proofs. In: Roy, B. (ed.) ASIACRYPT 2005. LNCS, vol. 3788, pp. 624–643. Springer, Heidelberg (2005)
Choo, K.-K., Boyd, C., Hitchcock, Y., Maitland, G.: On session identifiers in provably secure protocols. In: Blundo, C., Cimato, S. (eds.) SCN 2004. LNCS, vol. 3352, pp. 351–366. Springer, Heidelberg (2005)
Clark, J., Jacob, J.: A survey of authentication protocol literature (1997), http://citeseer.ist.psu.edu/clark97survey.html
Cremers, C.: Scyther tool with compromising adversaries extension. Includes protocol description files and test scripts, http://people.inf.ethz.ch/cremersc/scyther/
Cremers, C.: The Scyther Tool: Verification, falsification, and analysis of security protocols. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 414–418. Springer, Heidelberg (2008)
Cremers, C.: Unbounded verification, falsification, and characterization of security protocols by pattern refinement. In: CCS ’08: Proc. of the 15th ACM Conference on Computer and Communications Security, pp. 119–128. ACM, New York (2008)
Cremers, C.: Session-state reveal is stronger than ephemeral key reveal: Attacking the NAXOS authenticated key exchange protocol. In: Abdalla, M., et al. (eds.) ACNS 2009. LNCS, vol. 5536, pp. 20–33. Springer, Heidelberg (2009)
Günther, C.: An identity-based key-exchange protocol. In: Quisquater, J.-J., Vandewalle, J. (eds.) EUROCRYPT 1989. LNCS, vol. 434, pp. 29–37. Springer, Heidelberg (1990)
Gupta, P., Shmatikov, V.: Towards computationally sound symbolic analysis of key exchange protocols. In: Proc. FMSE 2005, pp. 23–32. ACM, New York (2005)
Gupta, P., Shmatikov, V.: Key confirmation and adaptive corruptions in the protocol security logic. In: FCS-ARSPA 2006, pp. 113–142 (2006)
Guttman, J.D.: Key compromise, strand spaces, and the authentication tests. In: 17th Annual Conference on Mathematical Foundations of Programming Semantics. Invited lecture, ENTCS, vol. 45, pp. 1–21 (2001)
Just, M., Vaudenay, S.: Authenticated multi-party key agreement. In: Kim, K.-c., Matsumoto, T. (eds.) ASIACRYPT 1996. LNCS, vol. 1163, pp. 36–49. Springer, Heidelberg (1996)
Katz, J., Yung, M.: Scalable protocols for authenticated group key exchange. In: Boneh, D. (ed.) CRYPTO 2003. LNCS, vol. 2729, pp. 110–125. Springer, Heidelberg (2003)
H. Krawczyk. HMQV: A high-performance secure Diffie-Hellman protocol. Cryptology ePrint Archive, Report 2005/176 (2005), http://eprint.iacr.org/ (retrieved on April 14, 2009)
Krawczyk, H.: HMQV: A high-performance secure Diffie-Hellman protocol. In: Shoup, V. (ed.) CRYPTO 2005. LNCS, vol. 3621, pp. 546–566. Springer, Heidelberg (2005)
LaMacchia, B., Lauter, K., Mityagin, A.: Stronger security of authenticated key exchange. In: Susilo, W., Liu, J.K., Mu, Y. (eds.) ProvSec 2007. LNCS, vol. 4784, pp. 1–16. Springer, Heidelberg (2007)
Lauter, K., Mityagin, A.: Security analysis of KEA authenticated key exchange protocol. In: Yung, M., et al. (eds.) PKC 2006. LNCS, vol. 3958, pp. 378–394. Springer, Heidelberg (2006)
Law, L., Menezes, A., Qu, M., Solinas, J., Vanstone, S.: An efficient protocol for authenticated key agreement. Designs, Codes and Cryptography 28, 119–134 (2003)
Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 147–166. Springer, Heidelberg (1996)
Menezes, A., Ustaoglu, B.: Comparing the pre- and post-specified peer models for key agreement. In: Mu, Y., Susilo, W., Seberry, J. (eds.) ACISP 2008. LNCS, vol. 5107, pp. 53–68. Springer, Heidelberg (2008)
Menezes, A., van Oorschot, P., Vanstone, S.: Handbook of Applied Cryptography. CRC Press, Boca Raton (October 1996)
Paulson, L.: Relations between secrets: Two formal analyses of the Yahalom protocol. Journal of Computer Security 9(3), 197–216 (2001)
Shoup, V.: On formal models for secure key exchange (version 4), (November 1999); revision of IBM Research Report RZ 3120 (April 1999)
Ustaoglu, B.: Obtaining a secure and efficient key agreement protocol from (H)MQV and NAXOS. Des. Codes Cryptography 46(3), 329–342 (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Basin, D., Cremers, C. (2010). Modeling and Analyzing Security in the Presence of Compromising Adversaries. In: Gritzalis, D., Preneel, B., Theoharidou, M. (eds) Computer Security – ESORICS 2010. ESORICS 2010. Lecture Notes in Computer Science, vol 6345. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15497-3_21
Download citation
DOI: https://doi.org/10.1007/978-3-642-15497-3_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-15496-6
Online ISBN: 978-3-642-15497-3
eBook Packages: Computer ScienceComputer Science (R0)