Iranian Society of CryptologyThe ISC International Journal of Information Security2008-20458120160117A short introduction to two approaches in formal verification of security protocols: model checking and theorem proving3244067610.22042/isecure.2016.8.1.1ENM. PourpounehDepartment of Mathematical Science, Sharif University of Technology, Tehran, IranR. RamezanianDepartment of Mathematical Science, Ferdowsi University of Mashhad, Mashhad, IranJournal Article20150904In this paper, we shortly review two formal approaches in verification of security protocols; model checking and theorem proving. Model checking is based on studying the behavior of protocols via generating all different behaviors of a protocol and checking whether the desired goals are satisfied in all instances or not. We investigate <em>Scyther</em> operational semantics as n example of this approach and then we model and verify some famous security protocols using <em>Scyther</em>. Theorem proving is based on deriving the desired goals from assumption of protocols via a deduction system. We define a deduction system named <em>Simple Logic for Authentication</em> to formally define the notion of authenticated communication based on the structure of the messages, and then we several famous protocols using our proposed deduction system and compare it with the verification results of <em>Scyther </em>model checking.http://www.isecure-journal.com/article_40676_b04f81eb888f84ee26045d193b349ee0.pdf