Interpretation Functions-Based Method to Verify Secrecy under Equational Theories

摘要

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 gives a guideline on how to construct an interpretation together with an example and how to use it to analyse a cryptographic protocol.