Relaxed Conditions for Secrecy in a Role-Based Specification
This work addresses protocol verification for security applications, but appears incremental as it relaxes existing conditions without major breakthroughs.
The paper tackles the problem of verifying secrecy in role-based protocols by introducing relaxed conditions on security estimation functions and protocols, proving that an increasing protocol is correct under these conditions.
In this paper, we look at the property of secrecy through the growth of the protocol. Intuitively, an increasing protocol preserves the secret. For that, we need functions to estimate the security of messages. Here, we give relaxed conditions on the functions and on the protocol and we prove that an increasing protocol is correct when analyzed with functions that meet these conditions.