Primitives for authentication in process algebras