Abstract: In today's age much of communication is over Internet. To facilitate this communication, communication protocols are used. To keep information passed over the internet safe from intruders, various security protocols are used. Even a small error in a security protocol design can have disastrous consequences. A good way to have strong guarantees and high confidence in the security protocol design, is to formally verify security protocols. In this thesis we see two currently popular models, namely the symbolic model and computational model. See the relationship between them, and we explore a new model called Bana Comon Model which promises an approach that combines advantages of both models.