Authentication primitives for secure protocol specifications