Automatic support for verification of secure transactions in distributed environment using symbolic model checking