In this paper we show how model checking can be used for the verification of security protocols using a logic of belief. We model principals as processes able to have beliefs. The idea underlying the approach is to treat separately the temporal evolution and the belief aspects of principals. Therefore, when we consider the temporal evolution, belief formulate are treated as atomic propositions; while the fact that principal A has beliefs about another principal B si modeled as the fact that A has access to a representation of B as a process. As motivating example, we use the framework proposed to formalize the Andrew protocol
Model Checking Security Protocols Using a Logic of Belief
Giunchiglia, Fausto
2000-01-01
Abstract
In this paper we show how model checking can be used for the verification of security protocols using a logic of belief. We model principals as processes able to have beliefs. The idea underlying the approach is to treat separately the temporal evolution and the belief aspects of principals. Therefore, when we consider the temporal evolution, belief formulate are treated as atomic propositions; while the fact that principal A has beliefs about another principal B si modeled as the fact that A has access to a representation of B as a process. As motivating example, we use the framework proposed to formalize the Andrew protocolFile in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.