In this paper we propose aspect oriented modeling and verification of a secure account based protocol for mobile payment when the application is under impersonation attack during the purchase phase of the protocol. The proposed work addresses the attack aspect and attack mitigation aspects that are woven inside secure account based protocol for mobile payment. The model proposed in this work gives a better understanding to implementer of secure account based protocol. Eventually the proposed model is verified by Alloy Analyzer to check the security concern at issuer's end. The model is checked for reasonably large scope of Alloy Analyzer without finding any counter example; this verifies the correctness of proposed model.

1. Juniper Research Forecasts Total Mobile Payments to Grow Nearly Ten Fold by 2013. Available from: www. juniperresearch. com.
2. G. Georg, I. Ray, K. Anastasakis, B. Bordbar, M. Toahchoodee, and S. H. Houmb, "An aspect-oriented methodology for designing secure applications," Information and Software Technology, vol. 51, no. 5, pp. 846–864 , May 2009.
3. D. X. Xu, V. Goel, K. E. Nygard, and W. E. Wong, "Aspect-oriented specification of threat-driven security requirements," International Journal of Computer Applications in Technology, vol. 31, no. 1/2, pp. 131-140, March 2008.
4. D. Xu, O. El-Ariss, W. Xu, and L. Wang, "Aspect oriented modeling and verification with finite state machines," Journal of Computer Science and Technology, vol. 24, no. 5 , pp. 949-961, September 2009.
5. Z. J. Zhu and M. Zulkernine, "A model-based aspect-oriented framework for building intrusion-aware software systems," Information and Software Technology, vol. 51, no. 5 , pp. 865–875, May 2009.
6. S. Kungpisdan, B. Srinivasan and P. D. Le, "A secure account based mobile payment protocol," in Proceedings International Conference on Information Technology: Coding and Computing, pp. 35-39, April 5-7 2004.
7. M. Hussein and M. Zulkernine, "UMLIntr: A UML profile for specifying intrusions," in Proceedings IEEE International Symposium and Workshop on Engineering of Computer Based Systems, pp. 279–286, March 27-30 2006.
8. Alloy Analyzer. Available from http://alloy. mit. edu/alloy/
9. D. Xu, M. Tu, M. Sanford, L. Thomas, D. Woodraska, and W. Xu, " Automated Security Test Generation with Formal Threat Models," IEEE Transactions on Dependable and Secure Computing, vol. 9, no. 4, pp. 526-540, July-August 2012.

Impersonation Attack Modeling Mobile Payment Aspect Oriented Model