Formal verification of the FDO protocol

Fido Device Onboarding (FDO) by the FIDO Alliance is expected to become the leading standard protocol for device secure onboarding. It is automatic, plug&play and it enables late binding. It overcomes the problems related to both proprietary zero-touch protocols and the traditional manual approach. Being automatic, this protocol must enforce a large number of security properties. In this paper, for the first time, we formally verify whether it satisfies some of its expected properties. Authentication and confidentiality of exchanged secrets are checked using a symbolic model and the Proverif tool. The verification confirms a weakness in the way the transfer of the device ownership is handled, which was already guessed by other authors and similar to another one already reported by FIDO.