Quantitative model checking of an RSA-based email protocol on mobile devices

The current proliferation of mobile devices has resulted in a large diversity of hardware specifications, each designed for different services and applications (e.g. cell phones, smart phones, PDAs). At the same time, e-mail message delivery has become a vital part of everyday communications. This article provides a cost-aware study of an RSA-based e-mail protocol executed upon the widely used Apple iPhone 1,2 with ARM1176JZF-S, operating in an High Speed Downlink Packet Access (HSDPA) mobile environment. The proposed study employs formal analysis techniques, such as probabilistic model checking, and proceeds to a quantitative analysis of the email protocol, taking into account computational parameters derived by the devices´ specifications. The value of this study is to form a computer-aided framework which balances the tradeoff between gaining in security, using high-length RSA keys, and conserving CPU resources, due to hardware limitations of mobile devices. To the best of our knowledge, this is the first time that probabilistic model checking is utilized towards verifying a secure e-mail protocol under hardware constrains. In fact, the proposed analysis can be widely exploited by protocol designers in order to verify their products in conjunction with specific mobile devices.