Modeling & verification of sliding window protocol with data loss and intruder detection using NuSMV

Aditya Sinha, Ajay Ry, Sanjay Singh

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Citation (Scopus)

Abstract

Sliding Window Protocol (SWP) is a feature of packet-based data transmission protocol. SWP is used where reliable in- order delivery of packets are required, such as in the Data Link Layer (OSI model) as well as in the Transmission Control Protocol (TCP). To check the proper working and the ow of the protocol, its modeling is very essential. Intruder detection in sliding window protocol is crucial for the the detection of the attacks. Existing model of the sliding window protocol does not include the intruder at the sender's and receiver's end. In this paper we have modeled the role of an intruder at the sender's as well as the receiver's end along with the modeling of the sliding window protocol. We have used NuSMV as a model checking tool to model the Sliding Window Protocol along with Intruder. Intruder detection and property verification of the protocol is done through respective Computational Tree Logic (CTL) formulas on the model. From the model checking it has been shown that the model satisfies all the specification of the sliding win dow protocol. Also it detects the presence of an intruder in the system.

Original languageEnglish
Title of host publicationProceedings of the 2nd International Conference on Computational Science, Engineering and Information, CCSEIT 2012
Pages352-357
Number of pages6
DOIs
Publication statusPublished - 12-12-2012
Event2nd International Conference on Computational Science, Engineering and Information, CCSEIT 2012 - Coimbatore, India
Duration: 26-10-201228-10-2012

Conference

Conference2nd International Conference on Computational Science, Engineering and Information, CCSEIT 2012
CountryIndia
CityCoimbatore
Period26-10-1228-10-12

Fingerprint

Network protocols
Model checking
OSI model
Transmission control protocol
Data communication systems
Specifications

All Science Journal Classification (ASJC) codes

  • Software
  • Human-Computer Interaction
  • Computer Vision and Pattern Recognition
  • Computer Networks and Communications

Cite this

Sinha, A., Ry, A., & Singh, S. (2012). Modeling & verification of sliding window protocol with data loss and intruder detection using NuSMV. In Proceedings of the 2nd International Conference on Computational Science, Engineering and Information, CCSEIT 2012 (pp. 352-357) https://doi.org/10.1145/2393216.2393276
Sinha, Aditya ; Ry, Ajay ; Singh, Sanjay. / Modeling & verification of sliding window protocol with data loss and intruder detection using NuSMV. Proceedings of the 2nd International Conference on Computational Science, Engineering and Information, CCSEIT 2012. 2012. pp. 352-357
@inproceedings{f94b006f08114da68e376dd2a4c9b34c,
title = "Modeling & verification of sliding window protocol with data loss and intruder detection using NuSMV",
abstract = "Sliding Window Protocol (SWP) is a feature of packet-based data transmission protocol. SWP is used where reliable in- order delivery of packets are required, such as in the Data Link Layer (OSI model) as well as in the Transmission Control Protocol (TCP). To check the proper working and the ow of the protocol, its modeling is very essential. Intruder detection in sliding window protocol is crucial for the the detection of the attacks. Existing model of the sliding window protocol does not include the intruder at the sender's and receiver's end. In this paper we have modeled the role of an intruder at the sender's as well as the receiver's end along with the modeling of the sliding window protocol. We have used NuSMV as a model checking tool to model the Sliding Window Protocol along with Intruder. Intruder detection and property verification of the protocol is done through respective Computational Tree Logic (CTL) formulas on the model. From the model checking it has been shown that the model satisfies all the specification of the sliding win dow protocol. Also it detects the presence of an intruder in the system.",
author = "Aditya Sinha and Ajay Ry and Sanjay Singh",
year = "2012",
month = "12",
day = "12",
doi = "10.1145/2393216.2393276",
language = "English",
isbn = "9781450313100",
pages = "352--357",
booktitle = "Proceedings of the 2nd International Conference on Computational Science, Engineering and Information, CCSEIT 2012",

}

Sinha, A, Ry, A & Singh, S 2012, Modeling & verification of sliding window protocol with data loss and intruder detection using NuSMV. in Proceedings of the 2nd International Conference on Computational Science, Engineering and Information, CCSEIT 2012. pp. 352-357, 2nd International Conference on Computational Science, Engineering and Information, CCSEIT 2012, Coimbatore, India, 26-10-12. https://doi.org/10.1145/2393216.2393276

Modeling & verification of sliding window protocol with data loss and intruder detection using NuSMV. / Sinha, Aditya; Ry, Ajay; Singh, Sanjay.

Proceedings of the 2nd International Conference on Computational Science, Engineering and Information, CCSEIT 2012. 2012. p. 352-357.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

TY - GEN

T1 - Modeling & verification of sliding window protocol with data loss and intruder detection using NuSMV

AU - Sinha, Aditya

AU - Ry, Ajay

AU - Singh, Sanjay

PY - 2012/12/12

Y1 - 2012/12/12

N2 - Sliding Window Protocol (SWP) is a feature of packet-based data transmission protocol. SWP is used where reliable in- order delivery of packets are required, such as in the Data Link Layer (OSI model) as well as in the Transmission Control Protocol (TCP). To check the proper working and the ow of the protocol, its modeling is very essential. Intruder detection in sliding window protocol is crucial for the the detection of the attacks. Existing model of the sliding window protocol does not include the intruder at the sender's and receiver's end. In this paper we have modeled the role of an intruder at the sender's as well as the receiver's end along with the modeling of the sliding window protocol. We have used NuSMV as a model checking tool to model the Sliding Window Protocol along with Intruder. Intruder detection and property verification of the protocol is done through respective Computational Tree Logic (CTL) formulas on the model. From the model checking it has been shown that the model satisfies all the specification of the sliding win dow protocol. Also it detects the presence of an intruder in the system.

AB - Sliding Window Protocol (SWP) is a feature of packet-based data transmission protocol. SWP is used where reliable in- order delivery of packets are required, such as in the Data Link Layer (OSI model) as well as in the Transmission Control Protocol (TCP). To check the proper working and the ow of the protocol, its modeling is very essential. Intruder detection in sliding window protocol is crucial for the the detection of the attacks. Existing model of the sliding window protocol does not include the intruder at the sender's and receiver's end. In this paper we have modeled the role of an intruder at the sender's as well as the receiver's end along with the modeling of the sliding window protocol. We have used NuSMV as a model checking tool to model the Sliding Window Protocol along with Intruder. Intruder detection and property verification of the protocol is done through respective Computational Tree Logic (CTL) formulas on the model. From the model checking it has been shown that the model satisfies all the specification of the sliding win dow protocol. Also it detects the presence of an intruder in the system.

UR - http://www.scopus.com/inward/record.url?scp=84870693367&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84870693367&partnerID=8YFLogxK

U2 - 10.1145/2393216.2393276

DO - 10.1145/2393216.2393276

M3 - Conference contribution

AN - SCOPUS:84870693367

SN - 9781450313100

SP - 352

EP - 357

BT - Proceedings of the 2nd International Conference on Computational Science, Engineering and Information, CCSEIT 2012

ER -

Sinha A, Ry A, Singh S. Modeling & verification of sliding window protocol with data loss and intruder detection using NuSMV. In Proceedings of the 2nd International Conference on Computational Science, Engineering and Information, CCSEIT 2012. 2012. p. 352-357 https://doi.org/10.1145/2393216.2393276