Abstract
Secrecy and authenticity properties of protocols are mutually dependent: every authentication is based on some secrets, and every secret must be authenticated. This interdependency is a significant source of complexity in reasoning about security. We describe a method to simplify it, by encapsulating the authenticity assumptions needed in the proofs of secrecy. This complements the method for encapsulating the secrecy assumptions in proofs of authenticity, presented in [1]. While logically straightforward, this idea of encapsulation in general, and the present treatment of secrecy in particular, allow formulating scalable and reusable reasoning patterns about the families of protocols of practical interest. The approach evolved as a design strategy in the Protocol Derivation Assistant (Pda), a semantically based environment and toolkit for derivational approach to security [2,3].
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
Cervesato, I., Meadows, C., Pavlovic, D.: An encapsulated authentication logic for reasoning about key distribution protocols. In: Guttman, J. (ed.) Proceedings of CSFW 2005, pp. 48–61. IEEE, Los Alamitos (2005)
Anlauff, M., Pavlovic, D., Waldinger, R., Westfold, S.: Proving authentication properties in the Protocol Derivation Assistant. In: Proceedings of ARSPA 2006. LNCS. IEEE, Los Alamitos (to appear 2006)
Anlauff, M., Pavlovic, D.: Pda download web site (2003–6), http://www.kestrel.edu/software/pda
Durgin, N., Mitchell, J., Pavlovic, D.: A compositional logic for proving security properties of protocols. J. of Comp. Security 11(4), 677–721 (2004)
Datta, A., Derek, A., Mitchell, J., Pavlovic, D.: A derivation system and compositional logic for security protocols. J. of Comp. Security 13, 423–482 (2005)
Meadows, C., Pavlovic, D.: Deriving, attacking and defending the GDOI protocol. In: Samarati, P., Ryan, P.Y.A., Gollmann, D., Molva, R. (eds.) ESORICS 2004. LNCS, vol. 3193, pp. 53–72. Springer, Heidelberg (2004)
Diffie, W., van Oorschot, P.C., Wiener, M.J.: Authentication and Authenticated Key Exchanges. Designs, Codes, and Cryptography 2, 107–125 (1992)
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)
Pratt, V.: Modelling concurrency with partial orders. Internat. J. Parallel Programming 15, 33–71 (1987)
Fabrega, F.J.T., Herzog, J., Guttman, J.: Strand spaces: What makes a security protocol correct? Journal of Computer Security 7, 191–230 (1999)
Abadi, M., Rogaway, P.: Reconciling two views of cryptography (the computational soundness of formal encryption). J. of Cryptology 15(2), 103–127 (2002)
Paulson, L.C.: The inductive approach to verifying cryptographic protocols. Journal of Computer Security 6, 85–128 (1998)
Millen, J.: On the freedom of decryption. Information Processing Letters 86(6), 329–333 (2003)
Goldreich, O.: Foundations of Cryptography. Basic Tools, vol. I. Cambridge University Press, Cambridge (2000)
Diffie, W., Hellman, M.E.: New directions in cryptography. IEEE Transactions on Information Theory IT-22(6), 644–654 (1976)
Kaufman, C., Perlman, R., Speciner, M.: Network Security. Private Communication in a Public World. In: Computer Networking and Distributed System, 2nd edn. Prentice Hall PTR, Englewood Cliffs (2002)
Boyd, C., Mathuria, A.: Protocols for Authentication and Key Establishment. In: Information Security and Cryptography. Springer, Heidelberg (2003)
Matsumoto, T., Takashima, Y., Imai, H.: On seeking smart public-key distribution systems. Transactions of the IECE (Japan) 69, 99–106 (1986)
Blake-Wilson, S., Menezes, A.: Authenticated diffie-hellman key agreement protocols. In: Tavares, S., Meijer, H. (eds.) SAC 1998. LNCS, vol. 1556, pp. 339–361. Springer, Heidelberg (1999)
Menezes, A., Qu, M., Vanstone, S.: Some new key agreement protocols providing mutual implicit authentication. In: SAC 1995: Proceedings of the Selected Areas in Cryptography, London, UK, pp. 22–32. Springer, Heidelberg (1995)
Law, L., Menezes, A., Qu, M., Solinas, J., Vanstone, S.: An efficient protocol for authenticated key agreement. Technical Report CORR 98-05, University of Waterloo, also in [22] (1998)
P1363 Working Group: The IEEE P1363 home page. standard specifications for public-key cryptography (2005), http://grouper.ieee.org/groups/1363/
Abadi, M., Burrows, M., Lampson, B., Plotkin, G.: A calculus for access control in distributed systems. ACM Transactions on Programming Languages and Systems 21(4), 706–734 (1993)
Lampson, B., Abadi, M., Burrows, M., Wobber, E.: Authentication in distributed systems: Theory and practice. ACM Trans. on Comput. Syst. 10(4), 265–310 (1992)
Myers, A.C., Liskov, B.: Protecting privacy using the decentralized label model. ACM Transactions on Software Engineering and Methodology 9(4), 410–442 (2000)
Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558–565 (1978)
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
Pavlovic, D., Meadows, C. (2006). Deriving Secrecy in Key Establishment Protocols. In: Gollmann, D., Meier, J., Sabelfeld, A. (eds) Computer Security – ESORICS 2006. ESORICS 2006. Lecture Notes in Computer Science, vol 4189. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11863908_24
Download citation
DOI: https://doi.org/10.1007/11863908_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-44601-9
Online ISBN: 978-3-540-44605-7
eBook Packages: Computer ScienceComputer Science (R0)