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 - http://www.isecure-journal.com/article_40676.html
L1 - http://www.isecure-journal.com/article_40676_b04f81eb888f84ee26045d193b349ee0.pdf
ER -