Formal verification of type flaw attacks in security protocols

Security protocols are often modelled at a high level of abstraction, potentially overlooking implementation-dependent vulnerabilities. Here we use the Z specification language´s rich set of data structures to formally model potentially ambiguous messages that may be exploited in a ´type flaw´ attack. We then show how to formally verify whether or not such an attack is actually possible in a particular protocol using Z´s schema calculus.