Outil dédié à la modélisation, l'analyse et la simulation de protocoles de sécurité pour les systèmes communicants. Il permet de générer des cas de test automatisés, d'identifier des vulnérabilités potentielles et de valider des propriétés de sécurité via des modèles formels. Utilisé principalement dans le domaine de la cybersécurité et de la vérification de systèmes.