• Dec 20, 2018 News!JACN Vol.6, No.2 has been published with online version.   [Click]
  • Sep 17, 2018 News!Welcome to 2019 4th International Conference on Information and Network Technologies (ICINT 2019), which will be held in Kyoto, Japan during May 25-27, 2019.   [Click]
  • Jul 04, 2018 News!JACN Vol.6, No.1 has been published with online version.   [Click]
General Information
    • ISSN: 1793-8244
    • Frequency: Semiyearly
    • DOI: 10.18178/JACN
    • Editor-in-Chief: Dr. Ka Wai Gary Wong
    • Executive Editor: Ms. Nina Lee
    • Abstracting/ Indexing: EI (INSPEC, IET),  Electronic Journals Library, Ulrich's Periodicals Directory, EBSCO, ProQuest, and Google Scholar.
    • E-mail: jacn@ejournal.net
Editor-in-chief
Dr. Ka Wai Gary Wong
Division of Information and Technology Studies, Faculty of Education, The University of Hong Kong.
It's a honor to serve as the editor-in-chief of JACN. I'll work together with the editors and reviewers to help the journal progress
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).

[PDF]

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-2018. Journal of Advances in Computer Networks.  All rights reserved.
E-mail: jacn@ejournal.net