In this position paper we advocate software model check- ing as a technique suitable for security of analysis mobile apps. Our recommendation is based on promising results that we achieved on analysing app collusion in the context of the Android operating system. To this end we devel- oped the K-Android tool, which provides an encoding of the Android/Smali code semantics within the K framework. K-Android allows for software model checking of Android APK files. Though our experience so far is limited to collusion, we believe the approach to be applicable to further security properties as well as other mobile operating systems.