Identity Protection, Secrecy and Authentication in Protocols with compromised Agents

Abstract

The design of security protocols is given an increasing level of academic interest, as an increasing number of important tasks are done over the Internet. Among the fields being researched is formal methods for modeling and verification of security protocols. One such method is developed by Cremers and Mauw. This is the method we have chosen to focus on in this paper. The model by Cremers and Mauw specifies a mathematical way to represent security protocols and their execution. It then defines conditions the protocols can fulfill, which is called security requirements. These typically states that in all possible executions, given a session in which all parties are honest, certain mathematical statements hold. Our aim is to extend the security requirements already defined in the model to allow some parties in the session to be under control of an attacker, and to add a new definition of identity protection. This we have done by slightly extending the model, and stating a new set of security requirements.