Authentication primitives for protocol specification