• Dec 24, 2021 News!Volume 9 No 1 has been indexed by EI (inspec)!   [Click]
  • Dec 07, 2021 News!JACN has been indexed by EI (inspec)!   [Click]
  • Nov 24, 2021 News!JACN Vol.9, No.2 has been published with online version.   [Click]
General Information
    • ISSN: 1793-8244 (Print)
    • Abbreviated Title:  J. Adv. Comput. Netw.
    • Frequency: Semiyearly
    • DOI: 10.18178/JACN
    • Editor-in-Chief: Dr. Ka Wai Gary Wong
    • Executive Editor: Ms. Shira Lu
    • Abstracting/ Indexing: INSPEC (IET), EBSCO, ProQuest, and Google Scholar.
    • E-mail: jacn@ejournal.net
Professor Haklin Kimm
East Stroudsburg University, USA
I'm happy to take on the position of editor in chief of JACN. We encourage authors to submit papers on all aspects of computer networks.

JACN 2018 Vol.6(2): 77-85 ISSN: 1793-8244
DOI: 10.18178/JACN.2018.6.2.258

Automated Logic-Based Technique for Formal Verification of Security Protocols

Anca D. Jurcut
Abstract—The design of secure protocols is complex and prone to error. Formal verification is an imperative step in the design of security protocols and provides a rigid and thorough means of evaluating the correctness of security protocols. This paper discusses the process of formal verification using a logic-based technique for detecting protocol weaknesses that are exploitable by freshness and interleaving attacks. This technique is realised as a special purpose logic for attack detection that can be used throughout the design stage, i.e. it subjects a draft of a protocol to formal analysis prior to its publication or deployment. For any detected failure the analysis will also reveal reasons for the weaknesses, facilitating design corrections. A summary of the attack detection logic is presented and its ability to detect weaknesses is demonstrated by applying it to a smart-card based authentication protocol. Further, a prototype implementation of the attack detection logic theory is introduced. An empirical study is presented that assesses the effectiveness and efficiency of the proposed automated technique by applying it to a set of protocols, incorporating some with known vulnerabilities and some that are known to be secure. This study confirms the ability of the technique to detect all design weaknesses. Additionally, it establishes the efficiency of the verification technique, in terms of memory requirements (study was carried out on a computing platform of 2GB of RAM) and execution times (milliseconds) required for protocol verification.

Index Terms—Attacks, formal verification, logic-based verification tool security protocols.

A. D. Jurcut is with the School of Computer Science, University College Dublin, Ireland (e-mail: anca.jurcut@ucd.ie).


Cite:Anca D. Jurcut, "Automated Logic-Based Technique for Formal Verification of Security Protocols," Journal of Advances in Computer Networks vol. 6, no. 2, pp. 77-85, 2018.

Copyright © 2008-2021. Journal of Advances in Computer Networks.  All rights reserved.
E-mail: jacn@ejournal.net