A temporalised belief logic for reasoning about authentication protocols
|Title||A temporalised belief logic for reasoning about authentication protocols|
|Booktitle||Proceedings of the 11th IEEE International Conference on Ubiquitous Computing and Communications (IUCC 2012)|
Trust is a critical issue for communication systems. A theory of trust for a given system consists of a set of rules that describe the trust of agents in the system. In a certain logical framework, the theory is generally established based on the security mechanisms of the system. Such a theory provides a foundation for reasoning about agent beliefs as well as security properties that the system may satisfy. For modelling authentication protocols, many researchers have proposed different logical systems. Since communication systems operate in dynamic environments, it is important to model the temporal aspects of such systems in a systematic way. In this paper, we propose a temporalised belief logic called TBL for formalising and verifying authentication protocols.