La plataforma Android es actualmente un objetivo para escritores maliciosos, que se centran continuamente en el desarrollo de nuevos tipos de ataques para extraer información sensible y privada de nuestros dispositivos móviles. En este panorama, una tendencia reciente está representada por el ataque de colusión. En resumen, este ataque requiere que se instalen dos o más aplicaciones para perpetrar el comportamiento malicioso que se divide en más de una sola aplicación: por esta razón, los programas anti-malware no pueden detectar este ataque, considerando que analizan solo una aplicación a la vez y que la única aplicación coludida no exhibe ninguna acción maliciosa. En este documento se propone un enfoque que explota la verificación de modelos para detectar automáticamente si dos aplicaciones exhiben la capacidad de realizar una colusión a través del mecanismo de comunicación SharedPreferences. Formulamos una serie de fórmulas de lógica temporal para detectar el ataque de colusión a partir de un modelo obtenido al seleccionar automáticamente las clases candidatas para la colusión, obtenidas mediante dos heurísticas que proponemos. Los resultados experimentales demuestran que el enfoque propuesto es prometedor en la detección de aplicaciones de colusión: de hecho, se obtiene una precisión igual a 0.99 al evaluar 993 aplicaciones de Android.