(* Comparing an abstract MAC primitive to its implementation using
hashes of blocks, as explained in "mobile values", section 6.
This example amounts to a change of signature, with
the implementation signature having additional equations for the
benefit of the attacker. *)
fun mac/2. (* MAC specification, with no equation. *)
private fun impl/2. (* choice of a MAC implementation *)
fun f/2. (* variablelength keyed hash *)
fun h/2. (* keyedhash for a single block *)
(*
The first, broken implementation uses
equation impl(k,x) = f(k,x).
The second, correct implementation uses
equation impl(k,x) = f(k,f(k,x)).
*)
equation impl(k,x) = f(k,f(k,x)).
equation h(f(x,y),z) = f(x,(y,z)).
free c, c1, c2.
process
new k;
(
( !in(c1, x); out(c,(x,choice[mac(k,x),impl(k,x)])))

( in(c,(x,m)); if choice[mac(k,x),impl(k,x)] = m then out(c2,x))
)