Authentication Primitives for Protocol Specifications