Formalizing and Evaluating mAuth: SecureAuthorization and Authentication Protocol for Native Apps

Abstract

OAuth was designed for the browser: its canonical authorisation-code flow assumes a redirect through a system user-agent, an assumption that fits poorly with native mobile applications, where every redirect crosses an OS boundary and breaks the in app experience. In 2024, Hamrefors and Törnkvist proposed mAuth, a redirect-less, mobile-native protocol that preserves OAuth’s authorisation guarantees while relo cating user authentication into the device’s own secure hardware. mAuth supports three authentication ceremonies: a CIBA-style backchannel, a FIDO2 challenge response and ROPC fallback. Every issued token is bound to a hardware-backed instance key, by means of platform attestation and DPoP. Its original presentation, however, argued for security informally and left several mechanisms underspecified. This thesis formalizes mAuth against a set of normative standards based around the OAuth architecture, and tightens the underspecified parts. A symbolic model of mAuth using the protocol verification tool Tamarin is also constructed. The three theories with authentication variants CIBA, FIDO2 and ROPC are built, with a set of lemmas establishing relevant normative security properties within the sym bolic model. The results therefore provide assurance relative to the abstractions and adversary model encoded in Tamarin, rather than a guarantee of security in deployment.