TY - JOUR ID - 40676 TI - A short introduction to two approaches in formal verification of security protocols: model checking and theorem proving JO - The ISC International Journal of Information Security JA - ISECURE LA - en SN - 2008-2045 AU - Pourpouneh, M. AU - Ramezanian, R. AD - Department of Mathematical Science, Sharif University of Technology, Tehran, Iran AD - Department of Mathematical Science, Ferdowsi University of Mashhad, Mashhad, Iran Y1 - 2016 PY - 2016 VL - 8 IS - 1 SP - 3 EP - 24 KW - Cryptographic Protocols KW - Formal KW - Verification KW - Model Checking KW - Theorem Proving DO - 10.22042/isecure.2016.8.1.1 N2 - In 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 Scyther operational semantics as n example of this approach and then we model and verify some famous security protocols using Scyther. Theorem proving is based on deriving the desired goals from assumption of protocols via a deduction system. We define a deduction system named Simple Logic for Authentication 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 Scyther model checking. UR - https://www.isecure-journal.com/article_40676.html L1 - https://www.isecure-journal.com/article_40676_b04f81eb888f84ee26045d193b349ee0.pdf ER -