Formalising theories of trust for authentication protocols

This paper discusses a formal approach for establishing theories of trust for authentication systems which can be used to reason about how agent beliefs evolve through time. The goal of an authentication system is to verify and authorise users in order to protect restricted data and information, so trust is a critical issue for authentication systems. After authentication, two principals (people, computers, services) should be entitled to believe that they are communicating with each other and not with intruders. So, it is important to express such beliefs precisely and to capture the reasoning that leads to them. In this paper, we focus on analysis of agent beliefs in dynamic environments using a temporalised belief logic, obtained by adding a temporal logic onto a belief logic. Working through a well-known authentication protocol, namely Kerberos, we discuss how to express principal beliefs involved in authentication protocols and the evolution of those beliefs based on a series of observations of agents as a consequence of communication. Our approach could be used for designing, verifying and implementing authentication protocols.