Abstract Formal analysis techniques have proved successful in finding flaws in secu - rity protocols Such techniques typically assume the presence of perfect encryp - tion, an assumption that is clearly not true in practice When we aim to prove the correctness of a protocol, we must be more careful in assuming bounds on the capabilities of the intruder: a real intruder can, and will, exploit properties of the underlying cryptosystem The Diffie - Hellman key agreement scheme ex - hibits a rich set of algebraic properties, and this report suggests how the existing CSP approach can be extended to incorporate these properties in a rank function verification The utility of the approach is established by performing an analysis of a key agreement protocol from the CLIQUES suite