A SHORT INTRODUCTION TO TWO APPROACHES IN FORMAL VERIFICATION OF SECURITY PROTOCOLS: MODEL CHECKING AND THEOREM PROVING

Q: How can I download an article?

To download an article from SID, first log in to the site, search for the article title, and click on the 'Download Article' option.

Q: How can I download an ISI article?

To download an ISI article on SID, enter the keyword or article title in the search bar, view the relevant results, click on the desired article, and select the 'Download Article' option.

Q: How can I access the SID database?

To access the SID database, visit SID.ir, create an account, and log in to access scientific resources.

Q: Is downloading articles from SID free?

Some articles on SID are available for free, while others require payment. Details are specified on the article's page.

POURPOUNEH MOHSEN; Ramezanian Rasoul

مرکز اطلاعات علمی Scientific Information Database (SID) - Trusted Source for Research and Academic Resources

Journal Paper

Paper Information

Journal: THE ISC INTERNATIONAL JOURNAL OF INFORMATION SECURITY Year:2016 | Volume:8 | Issue:1 Page(s): 3-24

Download Full-Text

Persian Verion

View:

699

Download:

248

Cites:

Information Journal Paper

Title

A SHORT INTRODUCTION TO TWO APPROACHES IN FORMAL VERIFICATION OF SECURITY PROTOCOLS: MODEL CHECKING AND THEOREM PROVING

Author(s)

POURPOUNEH MOHSEN | Ramezanian Rasoul | Issue Writer Certificate

Keywords

CRYPTOGRAPHIC PROTOCOLSQ2

FORMAL VERIFICATIONQ2

MODEL CHECKINGQ2

THEOREM PROVINGQ2

Abstract

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 an 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.

Cites

No record.

References

No record.

Cite

APA: Copy

POURPOUNEH, MOHSEN, & Ramezanian, Rasoul. (2016). A SHORT INTRODUCTION TO TWO APPROACHES IN FORMAL VERIFICATION OF SECURITY PROTOCOLS: MODEL CHECKING AND THEOREM PROVING. THE ISC INTERNATIONAL JOURNAL OF INFORMATION SECURITY, 8(1 ), 3-24. SID. https://sid.ir/paper/241795/en

Vancouver: Copy

POURPOUNEH MOHSEN, Ramezanian Rasoul. A SHORT INTRODUCTION TO TWO APPROACHES IN FORMAL VERIFICATION OF SECURITY PROTOCOLS: MODEL CHECKING AND THEOREM PROVING. THE ISC INTERNATIONAL JOURNAL OF INFORMATION SECURITY[Internet]. 2016;8(1 ):3-24. Available from: https://sid.ir/paper/241795/en

IEEE: Copy

MOHSEN POURPOUNEH, and Rasoul Ramezanian, “A SHORT INTRODUCTION TO TWO APPROACHES IN FORMAL VERIFICATION OF SECURITY PROTOCOLS: MODEL CHECKING AND THEOREM PROVING,” THE ISC INTERNATIONAL JOURNAL OF INFORMATION SECURITY, vol. 8, no. 1 , pp. 3–24, 2016, [Online]. Available: https://sid.ir/paper/241795/en

Related Journal Papers