An explicit model of belief change for cryptographic protocol verification

Hunter, Aaron (Aaron Hunter (Aaron_Hunter)) (author)
Delgrande, James, P. (author)
(editor)
(translator)

Copyright © 2007 Association for the Advancement of Artificial Intelligence

Proceedings of the 8th International Symposium on Logical Formalizations of Commonsense Reasoning. Stanford, CA, 2007. Cryptographic protocols are structured sequences of messages that are used for exchanging information in a hostile environment. Many protocols have epistemic goals: a successful run of the protocol is intended to cause a participant to hold certain beliefs. As such, epistemic logics have been employed for the verification of cryptographic protocols. Although this approach to verification is explicitly concerned with changing beliefs, formal belief change operators have not been incorporated in previous work. In this preliminary paper, we introduce a new approach to protocol verification by combining a monotonic logic with a non-monotonic belief change operator. In this context, a protocol participant is able to retract beliefs in response to new information and a protocol participant is able to postulate the most plausible event explaining new information. Hence, protocol participants may draw conclusions from received messages in the same manner conclusions are drawn in formalizations of commonsense reasoning. We illustrate that this kind of reasoning is particularly important when protocol participants have incorrect beliefs.

https://ocs.aaai.org/Papers/Symposia/Spring/2007/SS-07-05/SS07-05-012.pdf