Formal Methods Meet Mobile Code Obfuscation