NDLI: Formal verification of security protocol with B method

Content Provider	IEEE Xplore Digital Library
Author	Kumar, S. Chandra, G. Yadav, D.
Copyright Year	2014
Description	Author affiliation: Dept. of Comput. Sci., Ambalika Inst. of Mgmt. & Technol. Lucknow, Lucknow, India (Kumar, S.) \|\| Dept. of Comput. Sci., Inst. of Eng. & Technol., Lucknow, India (Chandra, G.; Yadav, D.)
Abstract	Security Protocols are fundamental building block of many important applications. These protocols are used to achieve various security requirements such as confidentially, authentication, integrity etc. of the applications. These protocols must be tested for their functional correctness before they are used. In many of the protocol errors have been detected, in spite of investing lot of time in their design. Modified Needham Schroeder Symmetric Key Protocol is a security protocol that incorporates an exchange of messages between two or more agents, for establishing a cryptographic key, and authenticating the identities of the agents. Authentication protocol has to be designed in such a way that makes it robust against replay attacks by any intruder. In this paper, use of formal methods for verification of correction of modified Needham-Schroeder Symmetric Key Protocol is demonstrated. B method has been used for developing specification of modified Needham-Schroeder Symmetric Key protocol and thereafter specifications are model checked using proB model checker. The specifications are free from deadlock and satisfy the behaviour or properties of the system expressed as invariants. It is verified that specifications leaves no spaces for the replay attack.
Starting Page	161
Ending Page	167
File Size	307431
Page Count	7
File Format	PDF
ISBN	9781479967575
e-ISBN	9781479967582
DOI	10.1109/ICCCT.2014.7001486
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2014-09-26
Publisher Place	India
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Protocols Encryption Formal specifications Niobium Formal verification
Content Type	Text
Resource Type	Article

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Mechanical verification and automatic implementation of communication protocols

Improved Otway Rees protocol and its formal verification

Implementing TLS with Verified Cryptographic Security

Formal modeling and verification of DLK protocol

Formal Verification of Abstract System and Protocol Specifications

Belief-Based Security Protocol Message Block Design Method

The verification of an industrial payment protocol: the SET purchase phase

Using temporal logics of knowledge in the formal verification of security protocols

On the formal specification and verification of a multiparty session protocol

Formal verification of security protocol with B method

Similar Documents

Mechanical verification and automatic implementation of communication protocols

Improved Otway Rees protocol and its formal verification

Implementing TLS with Verified Cryptographic Security

Formal modeling and verification of DLK protocol

Formal Verification of Abstract System and Protocol Specifications

Belief-Based Security Protocol Message Block Design Method

The verification of an industrial payment protocol: the SET purchase phase

Using temporal logics of knowledge in the formal verification of security protocols

On the formal specification and verification of a multiparty session protocol

Formal verification of security protocol with B method