We present a tool for checking automatically the correctness of cryptographic protocols with finite behaviour. The underlying
the- ory has been proposed in [13] and borrows some compositional analysis concepts for process algebras (see [3],[8]). Here we extend the theory by showing an interesting relation among security properties.
Work partially supported by CNR, Progetto Strategico "Modelli e Metodi per la Matematica e l’Ingegneria and by MURST Progetto
“Tecniche Formali per la Specifica, l’Analisi, la Verifica e la Trasformazione dei Sistemi Software”.