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 paper provides a cost-aware study of an RSA-based e-mail protocol executed upon the widely used Apple iPhone1,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.