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 protocol
File 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.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11582/5
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
social impact