Automatic support for verification of secure transactions in distributed environment using symbolic model checking - Di Sciascio, Eugenio (Array, 2001)