Epistemic Logic Based on Dolev-Yao Model
Abstract
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.
References
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.
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.
Published
2017-07-02
How to Cite
BENEVIDES, Mario R. F.; FERNANDEZ, Luiz C. F.; DE OLIVEIRA, Anna C. C. M..
Epistemic Logic Based on Dolev-Yao Model. In: PROCEEDINGS OF THE THEORY OF COMPUTATION MEETING (ETC), 2. , 2017, São Paulo.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
2017
.
p. 13-16.
ISSN 2595-6116.
DOI: https://doi.org/10.5753/etc.2017.3180.
