NDLI: Computational soundness without protocol restrictions

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

On the foundations of trust in networks of humans and computers

Fides: selectively hardening software application components against kernel-level or process-level malware

The most dangerous code in the world: validating SSL certificates in non-browser software

Enhancing Tor's performance using real-time traffic classification

Adaptive defenses for commodity software through virtual application partitioning

Mobile data charging: new attacks and countermeasures

Self-service cloud computing

Kargus: a highly-scalable software-based intrusion detection system

Operating system framed in case of mistaken identity: measuring the success of web-based spoofing attacks on OS password-entry dialogs

Minimizing private data disclosures in the smart grid

Machine-generated algorithms, proofs and software for the batch verification of digital signature schemes

Provable security of S-BGP and other path vector protocols: model, analysis and extensions

Touching from a distance: website fingerprinting attacks and defenses

Privacy-aware personalization for mobile advertising

Computational soundness without protocol restrictions

You are what you include: large-scale evaluation of remote javascript inclusions

Secure two-party computations in ANSI C

Vanity, cracks and malware: insights into the anti-copy protection ecosystem

On the parameterized complexity of the workflow satisfiability problem

Double-spending fast payments in bitcoin

Verifiable data streaming

Towards measuring warning readability

Hardware enhanced security

Fifth ACM workshop on artificial intelligence and security (AISec 2012)

A software-hardware architecture for self-protecting data

Why eve and mallory love android: an analysis of android SSL (in)security

Routing around decoys

Leveraging "choice" to automate authorization hook placement

New privacy issues in mobile telephony: fix and verification

Hourglass schemes: how to prove that cloud files are encrypted

Populated IP addresses: classification and applications

The devil is in the (implementation) details: an empirical analysis of OAuth SSO systems

How secure are power network signature based time stamps?

Full proof cryptography: verifiable compilation of efficient zero-knowledge protocols

Towards a bayesian network game framework for evaluating DDoS attacks and defense

Protecting location privacy: optimal strategy against localization attacks

Knowing your enemy: understanding and detecting malicious web advertising

Computational verification of C protocol implementations by symbolic execution

FlowFox: a web browser with flexible and precise information flow control

Foundations of garbled circuits

Manufacturing compromise: the emergence of exploit-as-a-service

Intransitive noninterference in nondeterministic systems

Revoke and let live: a secure key revocation api for cryptographic devices

Dynamic searchable symmetric encryption

Context-aware web security threat prevention

The state and evolution of privacy by design

STC 2012: the seventh ACM workshop on scalable trusted computing

Vigilare: toward snoop-based kernel integrity monitor

A cross-protocol attack on the TLS protocol

SkypeMorph: protocol obfuscation for Tor bridges

Binary stirring: self-randomizing instruction addresses of legacy x86 binary code

PScout: analyzing the Android permission specification

Resource-freeing attacks: improve your cloud performance (at your neighbor's expense)

Blacksheep: detecting compromised hosts in homogeneous crowds

OTO: online trust oracle for user-centric trust establishment

SABOT: specification-based payload generation for programmable logic controllers

Publicly verifiable delegation of large polynomials and matrix computations, with applications

DCast: sustaining collaboration in overlay multicast despite rational collusion

Deanonymizing mobility traces: using social network as a side-channel

Non-tracking web analytics

Verified security of redundancy-free encryption from Rabin and RSA

Scriptless attacks: stealing the pie without touching the sill

Salus: a system for server-aided secure function evaluation

Before we knew it: an empirical study of zero-day attacks in the real world

Precise enforcement of progress-sensitive security

PERM: practical reputation-based blacklisting without TTPS

PrivateFS: a parallel oblivious file system

Understanding new anonymity networks from a user's perspective

Large-scale DNS data analysis

4th cloud computing security workshop (CCSW 2012)

StegoTorus: a camouflage proxy for the Tor anonymity system

Aligot: cryptographic function identification in obfuscated binary programs

CHEX: statically vetting Android apps for component hijacking vulnerabilities

Single round access privacy on outsourced storage

Innocent by association: early recognition of legitimate users

Strengthening user authentication through opportunistic cryptographic identity assertions

GPS software attacks

Secure two-party computation in sublinear (amortized) time

PeerPress: utilizing enemies' P2P strength against them

Differentially private sequential data publication via variable-length n-grams

Priceless: the role of payments in abuse-advertised goods

TreeDroid: a tree automaton based approach to enforcing data processing policies

Measuring vote privacy, revisited

Demonstrating the effectiveness of MOSES for separation of execution modes

CCS'12 co-located workshop summary for SPSM 2012

CensorSpoofer: asymmetric communication using IP spoofing for censorship-resistant web browsing

An historical examination of open source releases and their vulnerabilities

Using probabilistic generative models for ranking risks of Android apps

Cross-VM side channels and their use to extract private keys

Neighborhood watch: security and privacy analysis of automatic meter reading systems

Practical yet universally composable two-server password-authenticated secret sharing

Collaborative TCP sequence number inference attack: how to crack sequence number under a second

On significance of the least significant bits for differential privacy

Protecting access privacy of cached contents in information centric networks

11th workshop on privacy in the electronic society

Network-based intrusion detection systems go active!

Second workshop on building analysis datasets and gathering experience returns for security (BADGERS'12)

Real-time continuous iris recognition for authentication using an eye tracker

ReasONets: a fuzzy-based approach for reasoning on network incidents

How privacy leaks from bluetooth mouse?

Marlin: making it harder to fish for gadgets

Advanced triple-channel botnets: model and implementation

Demonstrating a lightweight data provenance for sensor networks

Location privacy leaking from spectrum utilization information in database-driven cognitive radio network

Authenticated secret key extraction using channel characteristics for body area networks

Privacy preserving boosting in the cloud with secure half-space queries

Detecting money-stealing apps in alternative Android markets

Automatic generation of vaccines for malware immunization

A covert channel construction in a virtualized environment

Robust dynamic remote data checking for public clouds

Model-based context privacy for personal data streams

Query encrypted databases practically

Computational soundness without protocol restrictions

Content Provider	ACM Digital Library
Author	Unruh, Dominique Malik, Ankit Backes, Michael
Abstract	The abstraction of cryptographic operations by term algebras, called Dolev-Yao models, is essential in almost all tool-supported methods for verifying security protocols. Recently significant progress was made in establishing computational soundness results: these results prove that Dolev-Yao style models can be sound with respect to actual cryptographic realizations and security definitions. However, these results came at the cost of imposing various constraints on the set of permitted security protocols: e.g., dishonestly generated keys must not be used, key cycles need to be avoided, and many more. In a nutshell, the cryptographic security definitions did not adequately capture these cases, but were considered carved in stone; in contrast, the symbolic abstractions were bent to reflect cryptographic features and idiosyncrasies, thereby requiring adaptations of existing verification tools. In this paper, we pursue the opposite direction: we consider a symbolic abstraction for public-key encryption and identify two cryptographic definitions called PROG-KDM (programmable key-dependent message) security and MKE (malicious-key extractable) security that we jointly prove to be sufficient for obtaining computational soundness without imposing assumptions on the protocols using this abstraction. In particular, dishonestly generated keys obtained from the adversary can be sent, received, and used. The definitions can be met by existing cryptographic schemes in the random oracle model. This yields the first computational soundness result for trace-properties that holds for arbitrary protocols using this abstraction (in particular permitting to send and receive dishonestly generated keys), and that is accessible to all existing tools for reasoning about Dolev-Yao models without further adaptations.
Starting Page	699
Ending Page	711
Page Count	13
File Format	PDF
ISBN	9781450316514
DOI	10.1145/2382196.2382270
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2012-10-16
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Sending keys Key dependent messages Computational soundness
Content Type	Text
Resource Type	Article

Central Library (ISO-9001:2015 Certified)
Indian Institute of Technology Kharagpur
Kharagpur, West Bengal, India | PIN - 721302

See location in the Map
03222 282435
Mail: support@ndl.gov.in

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