Needed functions for security models
To model DiffieHellman-active.pv from Proverif examples, two functions are missing.
First, there is:
const g: bitstring.
fun exp(bitstring, bitstring): bitstring.
equation forall x: bitstring, y: bitstring; exp(exp(g, x), y) = exp(exp(g, y), x).
It is still possible to replace it with DH(pk(x),y) = DH(pk(y),x)
.
And then there is also:
reduc forall m: bitstring, k: bitstring; checksign(sign(m,k), pk(k)) = m.