Epistemic Logic Based on Dolev-Yao Model

• Mario R. F. Benevides UFRJ
• Luiz C. F. Fernandez UFRJ
• Anna C. C. M. de Oliveira UFRJ

DOI: https://doi.org/10.5753/etc.2017.3180

Resumo

In this work, we extend multi-agent epistemic logic for reasoning about properties in protocols. It is based on Dolev-Yao model and uses structured propositions, a new technique to deal with messages, keys and properties in security protocols in an uniform manner, keeping the logic propositional. In order to illustrate the applicability of this new logic, an example is presented.

Referências

Boureanu, I., Cohen, M., and Lomuscio, A. (2009). Automatic verification of temporalepistemic properties of cryptographic protocols. Journal of Applied Non-Classical Logics, 19(4):463–487.

Cohen, M. and Dam, M. (2007). A complete axiomatization of knowledge and cryptography. In 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 10-12 July 2007, Wroclaw, Poland, Proceedings, pages 77–88.

Dolev, D. and Yao, A. C. (1983). On the security of public key protocols. Information Theory, IEEE Transactions on, 29(2):198–208.

Fagin, R., Halpern, J. Y., Moses, Y., and Vardi, M. Y. (1995). Reasoning About Knowledge. MIT Press, Cambridge, Massachusetts.

Kramer, S. (2008). Cryptographic Protocol Logic: Satisfaction for (timed) Dolev-Yao cryptography. Journal of Logic and Algebraic Programming, 77(1–2).

Lamport, L. (1978). Time, clocks, and the ordering of events in a distributed system. Commun. ACM, 21(7):558–565.