Secrecy of cryptographic protocols under equational theory

This paper gives a novel approach to verify the secrecy property of cryptographic protocols under equational theories. Indeed, by using the notion of interpretation functions, this paper presents some sufficient and practical conditions allowing to guarantee the secrecy property of cryptographic protocols under any equational theory. An interpretation function is a safe means by which an agent can estimate the security level of message components that he receives so that he can handle them correctly. Also, this paper proves that polynomials help a lot with the construction of an interpretation function and gives a guideline on how to construct such functions together with an example and how to use it to analyse a cryptographic protocol.