Modelling Cryptographic Keys In Dynamic Epistemic Logic With DEMO

Abstract : It is far from obvious to find logical counterparts to cryptographic 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 cryptographic 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.
Type de document :
Communication dans un congrès
Perez, J. B. and et al. PAAMS 2012 - 10th International Conference on Practical Applications of Agents and Multi-Agent Systems, Mar 2012, Salamanca, Spain. Springer, Advances in Intelligent and Soft Computing, 156, pp.155-162, 2012, Highlights on Practical Applications of Agents and Multi-Agent Systems. 〈10.1007/978-3-642-28762-6_19〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00756869
Contributeur : Jurgen Vinju <>
Soumis le : vendredi 23 novembre 2012 - 21:39:46
Dernière modification le : mercredi 14 mars 2018 - 15:40:26

Lien texte intégral

Identifiants

Collections

Citation

H. Van Ditmarsch, D. J. N. Van Eijck, Ignacio Hernández-Antón, F. A. G. Sietsma, S. E. Simon, et al.. Modelling Cryptographic Keys In Dynamic Epistemic Logic With DEMO. Perez, J. B. and et al. PAAMS 2012 - 10th International Conference on Practical Applications of Agents and Multi-Agent Systems, Mar 2012, Salamanca, Spain. Springer, Advances in Intelligent and Soft Computing, 156, pp.155-162, 2012, Highlights on Practical Applications of Agents and Multi-Agent Systems. 〈10.1007/978-3-642-28762-6_19〉. 〈hal-00756869〉

Partager

Métriques

Consultations de la notice

103