NDLI: Automated Verification of Equivalence Properties of Cryptographic Protocols

Please wait, while we are loading the content...

Automated Verification of Equivalence Properties of Cryptographic Protocols

Content Provider	ACM Digital Library
Author	Chadha, Rohit Cheval, Vincent Ciobâcă, Ştefan Kremer, Steve
Copyright Year	2016
Description	Author Affiliation: University of Kent(University of missouri, MO, USA (Chadha, Rohit; Inria nancy--grand-est (kremer, Steve); “alexandru ioan cuza” university, Iaşi, Romania (Ciobc, tefan); Cheval, Vincent))
Abstract	Indistinguishability properties are essential in formal verification of cryptographic protocols. They are needed to model anonymity properties, strong versions of confidentiality, and resistance against offline guessing attacks. Indistinguishability properties can be conveniently modeled as equivalence properties. We present a novel procedure to verify equivalence properties for a bounded number of sessions of cryptographic protocols. As in the applied pi calculus, our protocol specification language is parametrized by a first-order sorted term signature and an equational theory that allows formalization of algebraic properties of cryptographic primitives. Our procedure is able to verify trace equivalence for determinate cryptographic protocols. On determinate protocols, trace equivalence coincides with observational equivalence, which can therefore be automatically verified for such processes. When protocols are not determinate, our procedure can be used for both under- and over-approximations of trace equivalence, which proved successful on examples. The procedure can handle a large set of cryptographic primitives, namely those whose equational theory is generated by an optimally reducing convergent rewrite system. The procedure is based on a fully abstract modelling of the traces of a bounded number of sessions of the protocols into first-order Horn clauses on which a dedicated resolution procedure is used to decide equivalence properties. We have shown that our procedure terminates for the class of subterm convergent equational theories. Moreover, the procedure has been implemented in a prototype tool Active Knowledge in Security Protocols and has been effectively tested on examples. Some of the examples were outside the scope of existing tools, including checking anonymity of an electronic voting protocol due to Okamoto.
Starting Page	1
Ending Page	32
Page Count	32
File Format	PDF
ISSN	15293785
e-ISSN	1557945X
DOI	10.1145/2926715
Volume Number	17
Issue Number	4
Journal	ACM Transactions on Computational Logic (TOCL)
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2016-09-20
Publisher Place	New York
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Applied pi calculus Automated verification Process equivalence Security protocols
Content Type	Text
Resource Type	Article
Subject	Theoretical Computer Science Logic Computational Mathematics Computer Science

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

Deciding security properties for cryptographic protocols. application to key cycles

From Security Protocols to Pushdown Automata

A Method for Proving Observational Equivalence

YAPA: A Generic Tool for Computing Intruder Knowledge

Zero-Knowledge in the Applied Pi-calculus and Automated Verification of the Direct Anonymous Attestation Protocol

Automated Verification of Equivalence Properties of Cryptographic Protocols

The concept of layered proving trees and its application to the automation of security protocol verification

Analyzing NSPK with the Applied Pi Calculus

Automatic testing equivalence verification of spi calculus specifications

Automated Verification of Equivalence Properties of Cryptographic Protocols

Similar Documents

Deciding security properties for cryptographic protocols. application to key cycles

From Security Protocols to Pushdown Automata

A Method for Proving Observational Equivalence

YAPA: A Generic Tool for Computing Intruder Knowledge

Zero-Knowledge in the Applied Pi-calculus and Automated Verification of the Direct Anonymous Attestation Protocol

Automated Verification of Equivalence Properties of Cryptographic Protocols

The concept of layered proving trees and its application to the automation of security protocol verification

Analyzing NSPK with the Applied Pi Calculus

Automatic testing equivalence verification of spi calculus specifications

Automated Verification of Equivalence Properties of Cryptographic Protocols