Analysis of Security Protocols using Finite-State Machines
Journal Title: International Journal of Advanced Research in Artificial Intelligence(IJARAI) - Year 2015, Vol 4, Issue 4
Abstract
This paper demonstrates a comprehensive analysis method using formal methods such as finite-state machine. First, we describe the modified version of our new protocol and briefly explain the encrypt-then-authenticate mechanism, which is regarded as more a secure mechanism than the one used in our protocol. Then, we use a finite-state verification to study the behaviour of each machine created for each phase of the protocol and examine their behaviours together. Modelling with finite-state machines shows that the modified protocol can function correctly and behave properly even with invalid input or time delay.
Authors and Affiliations
Dania Aljeaid, Xiaoqi Ma, Caroline Langensiepen
Keywords
Related Articles
- EP ID EP148064
- DOI 10.14569/IJARAI.2015.040407
- Views 111
- Downloads 0
3D Skeleton model derived from Kinect Depth Sensor Camera and its application to walking style quality evaluations
Feature extraction for gait recognition has been created widely. The ancestor for this task is divided into two parts, model based and free-model based. Model-based approaches obtain a set of static or dynamic skeleton p...
FlexRFID: A Security and Service Control Policy-Based Middleware for Context-Aware Pervasive Computing
Ubiquitous computing targets the provision of seamless services and applications by providing an environment that involves a variety of devices having different capabilities. The design of applications in these env...
FREQUENT PHYSICAL HEALTH MONITORING AS VITAL SIGNS WITH PSYCHOLOGICAL STATUS MONITORING FOR SEARCH AND RESCUE OF HANDICAPPED, DISEASED AND ELDERY PERSONS
Method and system for frequent health monitoring as vital signs with psycholo9gical status monitoring for search and rescue of handicapped person is proposed. Heart beat pulse rate, body temperature, blood pressure...
Enterprise Architecture Model that Enables to Search for Patterns of Statistical Information
Enterprise architecture is the stem from which developing of any departmental information system should grow and around which it should revolve. In the paper, a fragment of an enterprise architecture model is built...
A real time OCSVM Intrusion Detection module with low overhead for SCADA systems
In this paper we present a intrusion detection module capable of detecting malicious network traffic in a SCADA (Supervisory Control and Data Acquisition) system. Malicious data in a SCADA system disrupt its correc...