Authentication primitives for secure protocol specifications

We use two authentication primitives proposed recently as a linguistic support for enforcing authentication. They offer a way of abstracting from various specifications of authentication and of obtaining idealized protocols “secure by construction”. Consequently, they help in proving that a cryptographic protocol correctly implements its corresponding abstract version; when the implementation is incorrect, suggestions on how to fix it may come from reasoning on the abstract specification.