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 - https://www.scopus.com/pages/publications/84870693367
UR - https://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
T3 - ACM International Conference Proceeding Series
SP - 352
EP - 357
BT - Proceedings of the 2nd International Conference on Computational Science, Engineering and Information, CCSEIT 2012
T2 - 2nd International Conference on Computational Science, Engineering and Information, CCSEIT 2012
Y2 - 26 October 2012 through 28 October 2012
ER -