Formal Verification of Consumer Remote Sim Provisioning Common Mutual Authentication using BAN Logic

Remote Subscriber Identity Module (SIM) Provisioning (RSP) is revolutionizing cellular connectivity management in consumer mobile devices and Internet of Things (IoT) systems through over-the-air SIM profile downloads. This paper presents a formal security verification of the RSP Common Mutual Authentication protocol using Burrows-Abadi-Needham (BAN) logic. The analysis delves into the authentication procedure between the embedded Universal Integrated Circuit Card (eUICC) and the Subscription Manager Data Preparation+ (SM-DP+) server. By rigorously applying BAN logic principles, we show that the protocol meets its mutual authentication goals within stated security assumptions. While our verification confirms the protocol's mathematical correctness, we also identify potential vulnerabilities based on our findings and other relevant literature. This highlights the potential for improving the security architecture of RSP using emerging technologies like blockchain, cloud-based authentication proxies, and automated verification methods. These findings help to advance the development of strong security mechanisms for the increasing embedded SIM ecosystem.