Abstract
We present a framework for reasoning about secrecy in a class of Diffie-Hellman protocols. The technique, which shares a conceptual origin with the idea of a rank function, uses the notion of a message-template to determine whether a given value is generable by an intruder in a protocol model. Traditionally, the rich algebraic structure of Diffie-Hellman messages has made it difficult to reason about such protocols using formal, rather than complexity-theoretic, techniques. We describe the approach in the context of the MTI A(0) protocol, and derive the conditions under which this protocol can be considered secure.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
[AC04] Abadi, M., Cortier, V.: Deciding knowledge in security protocols under equational theories. In: DÃaz, J., Karhumäki, J., Lepistö, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 46–58. Springer, Heidelberg (2004)
[AST00] Ateniese, G., Steiner, M., Tsudik, G.: Authenticated group key agreement and friends. In: Proceedings of the 5th ACM Conference on Computer and Communication Security. ACM Press, New York (2000)
[BCP01] Bresson, E., Chevassut, O., Pointcheval, D.: Provably authenticated group diffie-hellman key exchange - the dynamic case. In: Boyd, C. (ed.) ASIACRYPT 2001. LNCS, vol. 2248, p. 290. Springer, Heidelberg (2001)
[BM03] Boyd, C., Mathuria, A.: Protocols for Authentication and Key Establishment. Springer, Heidelberg (2003)
[BR02] Broadfoot, P., Roscoe, A.W.: Internalising agents in CSP protocol models. In: Workshop on Issues in the Theory of Security: WITS 2002 (2002)
[DH76] Diffie, W., Hellman, M.E.: New directions in cryptography. IEEE Transactions on Information Theory IT-22(6) (1976)
[DS05]Delicata, R., Schneider, S.: Temporal rank functions for forward secrecy. In: Proceedings of the 18th Computer Security Foundations Workshop: CSFW-18. IEEE Computer Society Press, Los Alamitos (2005)
[Hea01] Heather, J.: Oh! Is it really you? using rank functions to verify authentication protocols. Ph.D Thesis, Royal Holloway, University of London (2001)
[JV96] Just, M., Vaudenay, S.: Authenticated multi-party key agreement. In: Kim, K.-c., Matsumoto, T. (eds.) ASIACRYPT 1996. LNCS, vol. 1163, Springer, Heidelberg (1996)
[Mea00] Meadows, C.: Extending formal cryptographic protocol analysis techniques for group protocols and low-level cryptographic primitives. In: Workshop on Issues in the Theory of Security: WITS 2000 (2000)
[MTI86] Matsumoto, T., Takashima, Y., Imai, H.: On seeking smart public-key-distribution systems. Transactions of the IECE of Japan E69(2) (1986)
[PQ01]Pereira, O., Quisquater, J.-J.: Security analysis of the Cliques protocols suites. In: Proceedings of the 14th IEEE Computer Security Foundations Workshop: CSFW-14. IEEE Computer Society Press, Los Alamitos (2001)
[Sch97]Schneider, S.: Verifying authentication protocols with CSP. In: Proceedings of The 10th Computer Security Foundations Workshop: CSFW-10. IEEE Computer Society Press, Los Alamitos (1997)
[Sch00]Schneider, S.: Concurrent and Real-time Systems: The CSP Approach. John Wiley and Sons, Ltd, Chichester (2000)
[THG99] Fábrega, F.J.T., Herzog, J., Guttman, J.: Strand spaces: Proving security protocols correct. Journal of Computer Security 7(2/3) (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Delicata, R., Schneider, S. (2006). A Formal Approach for Reasoning About a Class of Diffie-Hellman Protocols. In: Dimitrakos, T., Martinelli, F., Ryan, P.Y.A., Schneider, S. (eds) Formal Aspects in Security and Trust. FAST 2005. Lecture Notes in Computer Science, vol 3866. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11679219_4
Download citation
DOI: https://doi.org/10.1007/11679219_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-32628-1
Online ISBN: 978-3-540-32629-8
eBook Packages: Computer ScienceComputer Science (R0)Springer Nature Proceedings Computer Science
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.