NDLI: Securing Multiparty Online Services Via Certification of Symbolic Transactions

Content Provider	IEEE Xplore Digital Library
Author	Chen, E.Y. Shuo Chen Qadeer, S. Rui Wang
Copyright Year	2015
Description	Author affiliation: Microsoft Res., Redmond, WA, USA (Shuo Chen; Qadeer, S.; Rui Wang) \|\| Carnegie Mellon Univ., Moffett Field, CA, USA (Chen, E.Y.)
Abstract	The prevalence of security flaws in multiparty online services (e.g., Single-sign-on, third-party payment, etc.) calls for rigorous engineering supported by formal program verification. However, the adoption of program verification faces several hurdles in the real world: how to formally specify logic properties given that protocol specifications are often informal and vague, how to precisely model the attacker and the runtime platform, how to deal with the unbounded set of all potential transactions. We introduce Certification of Symbolic Transaction (CST), an approach to significantly lower these hurdles. CST tries to verify a protocol-independent safety property jointly defined over all parties, thus avoids the burden of individually specifying every party's property for every protocol, CST invokes static verification at runtime, i.e., It symbolically verifies every transaction on-the-fly, and thus (1) avoids the burden of modeling the attacker and the runtime platform, (2) reduces the proof obligation from considering all possible transactions to considering only the one at hand. We have applied CST on five commercially deployed applications, and show that, with only tens (or 100+) of lines of code changes per party, the original implementations are enhanced to achieve the objective of CST. Our security analysis shows that 12 out of 14 logic flaws reported in the literature will be prevented by CST. We also stress-tested CST by building a gambling system integrating four different services, for which there is no existing protocol to follow. Because transactions are symbolic and cacheable, CST has near-zero amortized runtime overhead. We make the source code of these implementations public, which are ready to be deployed for real-world uses.
Starting Page	833
Ending Page	849
File Size	1136419
Page Count	17
File Format	PDF
ISBN	9781467369497
ISSN	10816011
DOI	10.1109/SP.2015.56
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2015-05-17
Publisher Place	USA
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Protocols Security Runtime Data structures Servers Certification Facebook single-sign-on multiparty protocol symbolic transaction CST verification online payment
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

Securing Multiparty Online Services via Certification of Symbolic Transactions

A security analysis of the OAuth protocol

Formal Analysis of a Single Sign-On Protocol Implementation for Android

Security issues of single sign on web services

Signing Me onto Your Accounts through Facebook and Google: A Traffic-Guided Security Study of Commercially Deployed Single-Sign-On Web Services

Cryptographic Protocol Synthesis and Verification for Multiparty Sessions

Automatic verification of security in payment protocols for electronic commerce.

Biometric Transaction Authentication Protocol

An Improved Scheme of Single Sign-On Protocol Based on Dynamic Double Password

Securing Multiparty Online Services Via Certification of Symbolic Transactions

Similar Documents

Securing Multiparty Online Services via Certification of Symbolic Transactions

A security analysis of the OAuth protocol

Formal Analysis of a Single Sign-On Protocol Implementation for Android

Security issues of single sign on web services

Signing Me onto Your Accounts through Facebook and Google: A Traffic-Guided Security Study of Commercially Deployed Single-Sign-On Web Services

Cryptographic Protocol Synthesis and Verification for Multiparty Sessions

Automatic verification of security in payment protocols for electronic commerce.

Biometric Transaction Authentication Protocol

An Improved Scheme of Single Sign-On Protocol Based on Dynamic Double Password

Securing Multiparty Online Services Via Certification of Symbolic Transactions