Abstract
It is far from obvious to find logical counterparts to crytographic protocol primitives. In logic, a common assumption is that agents are perfectly rational and have no computational limitations. This creates a dilemma. If one merely abstracts from computational aspects, protocols become trivial and the difference between tractable and intractable computation, surely an essential feature of protocols, disappears. This way, the protocol gets lost. On the other hand, if one ‘merely′ (scare quotes indeed) models agents with computational limitations (or otherwise bounded rationality), very obvious aspects of reasoning become problematic. That way, the logic gets lost. We present a novel way out of this dilemma.We propose an abstract logical architecture wherein public and private, or symmetric keys, and their roles in crytographic protocols, all have formal counterparts. Instead of having encryption and decryption done by a principal, the agent sending or receiving messages, we introduce additional, virtual, agents to model that, so that one-way-function aspects of computation can be modelled as constraints on the communication between principals and these virtual counterparts. In this modelling it does not affect essential protocol features if agents are computationally unlimited.We have implemented the proposal in a dynamic epistemic model checker called DEMO.
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
Dechesne, F., Wang, Y.: To know or not to know: epistemic approaches to security protocol verification. Synthese 177, 51–76 (2010)
van Ditmarsch, H., van der Hoek, W., Kooi, B.: Dynamic Epistemic Logic. Synthese Library, vol. 337. Springer, Heidelberg (2007)
van Eijck, J.: DEMO — a demo of epistemic modelling. In: van Benthem, J., Gabbay, D., Löwe, B. (eds.) Interactive Logic — Proceedings of the 7th Augustus de Morgan Workshop. Texts in Logic and Games, vol. 1, pp. 305–363. Amsterdam University Press (2007)
Halpern, J.Y., Pucella, R.: Modeling Adversaries in a Logic for Security Protocol Analysis. In: Abdallah, A.E., Ryan, P.Y.A., Schneider, S. (eds.) FASec 2002. LNCS, vol. 2629, pp. 115–132. Springer, Heidelberg (2003)
Ramanujam, R., Suresh, S.P.: Information based reasoning about security protocols. Electr. Notes Theor. Comput. Sci. 55(1) (2001)
Rivest, R.L., Shamir, A., Adleman, L.: A method for obtaining digital signatures and public-key cryptosystems. Commun. ACM 21(2), 120–126 (1978)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
van Ditmarsch, H., van Eijck, J., Hernández-Antón, I., Sietsma, F., Simon, S., Soler-Toscano, F. (2012). Modelling Cryptographic Keys in Dynamic Epistemic Logic with DEMO. In: Pérez, J., et al. Highlights on Practical Applications of Agents and Multi-Agent Systems. Advances in Intelligent and Soft Computing, vol 156. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28762-6_19
Download citation
DOI: https://doi.org/10.1007/978-3-642-28762-6_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-28761-9
Online ISBN: 978-3-642-28762-6
eBook Packages: EngineeringEngineering (R0)