Biblio
Filters: Keyword is composability [Clear All Filters]
A Dynamic Searchable Encryption Scheme for Secure Cloud Server Operation Reserving Multi-Keyword Ranked Search. 2017 4th International Conference on Networking, Systems and Security (NSysS). :1–9.
.
2017. Cloud computing is becoming more and more popular day by day due to its maintenance, multitenancy and performance. Data owners are motivated to outsource their data to the cloud servers for resource pooling and productivity where multiple users can work on the same data concurrently. These servers offer great convenience and reduced cost for the computation, storage and management of data. But concerns can persist for loss of control over certain sensitive information. The complexity of security is largely intensified when data is distributed over a greater number of devices and data is shared among unrelated users. So these sensitive data should be encrypted for solving these security issues that many consumers cannot afford to tackle. In this paper, we present a dynamic searchable encryption scheme whose update operation can be completed by cloud server while reserving the ability to support multi-keyword ranked search. We have designed a scheme where dynamic operations on data like insert, update and delete are performed by cloud server without decrypting the data. Thus this scheme not only ensures dynamic operations on data but also provides a secure technique by performing those tasks without decryption. The state-of-the-art methods let the data users retrieve the data, re-encrypt it under the new policy and then send it again to the cloud. But our proposed method saves this high computational overhead by reducing the burden of performing dynamic operation by the data owners. The secure and widely used TF × IDF model is used along with kNN algorithm for construction of the index and generation of the query. We have used a tree-based index structure, so our proposed scheme can achieve a sub-linear search time. We have conducted experiments on Amazon EC2 cloud server with three datasets by updating a file, appending a file and deleting a file from the document collection and compared our result with the state-of-the-art method. Results show th- t our scheme has an average running time of 42ms which is 75% less than the existing method.
Dynamic Service Chaining with Dysco. Proceedings of the Conference of the ACM Special Interest Group on Data Communication. :57–70.
.
2017. Middleboxes are crucial for improving network security and performance, but only if the right traffic goes through the right middleboxes at the right time. Existing traffic-steering techniques rely on a central controller to install fine-grained forwarding rules in network elements—at the expense of a large number of rules, a central point of failure, challenges in ensuring all packets of a session traverse the same middleboxes, and difficulties with middleboxes that modify the "five tuple." We argue that a session-level protocol is a fundamentally better approach to traffic steering, while naturally supporting host mobility and multihoming in an integrated fashion. In addition, a session-level protocol can enable new capabilities like dynamic service chaining, where the sequence of middleboxes can change during the life of a session, e.g., to remove a load-balancer that is no longer needed, replace a middlebox undergoing maintenance, or add a packet scrubber when traffic looks suspicious. Our Dysco protocol steers the packets of a TCP session through a service chain, and can dynamically reconfigure the chain for an ongoing session. Dysco requires no changes to end-host and middlebox applications, host TCP stacks, or IP routing. Dysco's distributed reconfiguration protocol handles the removal of proxies that terminate TCP connections, middleboxes that change the size of a byte stream, and concurrent requests to reconfigure different parts of a chain. Through formal verification using Spin and experiments with our Linux-based prototype, we show that Dysco is provably correct, highly scalable, and able to reconfigure service chains across a range of middleboxes.
Dynamic Symbolic Execution for Polymorphism. Proceedings of the 26th International Conference on Compiler Construction. :120–130.
.
2017. Symbolic execution is an important program analysis technique that provides auxiliary execution semantics to execute programs with symbolic rather than concrete values. There has been much recent interest in symbolic execution for automatic test case generation and security vulnerability detection, resulting in various tools being deployed in academia and industry. Nevertheless, (subtype or dynamic) polymorphism of object-oriented programs has been neglected: existing symbolic execution techniques can explore different targets of conditional branches but not different targets of method invocations. We address the problem of how this polymorphism can be expressed in a symbolic execution framework. We propose the notion of symbolic types, which make object types symbolic. With symbolic types,[ various targets of a method invocation can be explored systematically by mutating the type of the receiver object of the method during automatic test case generation. To the best of our knowledge, this is the first attempt to address polymorphism in symbolic execution. Mutation of method invocation targets is critical for effectively testing object-oriented programs, especially libraries. Our experimental results show that symbolic types are significantly more effective than existing symbolic execution techniques in achieving test coverage and finding bugs and security vulnerabilities in OpenJDK.
Dynamic Tainting for Automatic Test Case Generation. Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis. :436–439.
.
2017. Dynamic tainting is an important part of modern software engineering research. State-of-the-art tools for debugging, bug detection and program analysis make use of this technique. Nonetheless, the research area based on dynamic tainting still has open questions, among others the automatic generation of program inputs. My proposed work concentrates on the use of dynamic tainting for test case generation. The goal is the generation of complex and valid test inputs from scratch. Therefore, I use byte level taint information enhanced with additional static and dynamic program analysis. This information is used in an evolutionary algorithm to create new offsprings and mutations. Concretely, instead of crossing and mutating the whole input randomly, taint information can be used to define which parts of the input have to be mutated. Furthermore, the taint information may also be used to define evolutionary operators. Eventually, the evolutionary algorithm is able to generate valid inputs for a program. Such inputs can be used together with the taint information for further program analysis, e.g. the generation of input grammars.
An Early Warning System for Suspicious Accounts. Proceedings of the 10th ACM Workshop on Artificial Intelligence and Security. :51–52.
.
2017. In the face of large-scale automated cyber-attacks to large online services, fast detection and remediation of compromised accounts are crucial to limit the spread of new attacks and to mitigate the overall damage to users, companies, and the public at large. We advocate a fully automated approach based on machine learning to enable large-scale online service providers to quickly identify potentially compromised accounts. We develop an early warning system for the detection of suspicious account activity with the goal of quick identification and remediation of compromised accounts. We demonstrate the feasibility and applicability of our proposed system in a four month experiment at a large-scale online service provider using real-world production data encompassing hundreds of millions of users. We show that - even using only login data, features with low computational cost, and a basic model selection approach - around one out of five accounts later flagged as suspicious are correctly predicted a month in advance based on one week's worth of their login activity.
An Effective Immersive Cyber Security Awareness Learning Platform for Businesses in the Hospitality Sector. 2017 IEEE 25th International Requirements Engineering Conference Workshops (REW). :111–117.
.
2017. The rapid digitalisation of the hospitality industry over recent years has brought forth many new points of attack for consideration. The hasty implementation of these systems has created a reality in which businesses are using the technical solutions, but employees have very little awareness when it comes to the threats and implications that they might present. This gap in awareness is further compounded by the existence of preestablished, often rigid, cultures that drive how hospitality businesses operate. Potential attackers are recognising this and the last two years have seen a huge increase in cyber-attacks within the sector.Attempts at addressing the increasing threats have taken the form of technical solutions such as encryption, access control, CCTV, etc. However, a high majority of security breaches can be directly attributed to human error. It is therefore necessary that measures for addressing the rising trend of cyber-attacks go beyond just providing technical solutions and make provision for educating employees about how to address the human elements of security. Inculcating security awareness amongst hospitality employees will provide a foundation upon which a culture of security can be created to promote the seamless and secured interaction of hotel users and technology.One way that the hospitality industry has tried to solve the awareness issue is through their current paper-based training. This is unengaging, expensive and presents limited ways to deploy, monitor and evaluate the impact and effectiveness of the content. This leads to cycles of constant training, making it very hard to initiate awareness, particularly within those on minimum waged, short-term job roles.This paper presents a structured approach for eliciting industry requirement for developing and implementing an immersive Cyber Security Awareness learning platform. It used a series of over 40 interviews and threat analysis of the hospitality industry to identify the requirements fo- designing and implementing cyber security program which encourage engagement through a cycle of reward and recognition. In particular, the need for the use of gamification elements to provide an engaging but gentle way of educating those with little or no desire to learn was identified and implemented. Also presented is a method for guiding and monitoring the impact of their employee's progress through the learning management system whilst monitoring the levels of engagement and positive impact the training is having on the business.
Efficient Approximate Medoids of Temporal Sequences. Proceedings of the 15th International Workshop on Content-Based Multimedia Indexing. :3:1–3:6.
.
2017. In order to compactly represent a set of data, its medoid (the element with minimum summed distance to all other elements) is a useful choice. This has applications in clustering, compression and visualisation of data. In multimedia data, the set of data is often sampled as a sequence in time or space, such as a video shot or views of a scene. The exact calculation of the medoid may be costly, especially if the distance function between elements is not trivial. While approximation methods for medoid selection exist, we show in this work that they do not perform well on sequences of images. We thus propose a novel algorithm for efficiently selecting an approximate medoid of a temporal sequence and assess its performance on two large-scale video data sets.
Efficient distribution of fragmented sensor data for obfuscation. MILCOM 2017 - 2017 IEEE Military Communications Conference (MILCOM). :695–700.
.
2017. The inherent nature of unattended sensors makes these devices most vulnerable to detection, exploitation, and denial in contested environments. Physical access is often cited as the easiest way to compromise any device or network. A new mechanism for mitigating these types of attacks developed under the Assistant Secretary of Defense for Research and Engineering, ASD(R&E) project, “Smoke Screen in Cyberspace”, was previously demonstrated in a live, over-the-air experiment. Smoke Screen encrypts, slices up, and disburses redundant fragments of files throughout the network. This paper describes enhancements to the disbursement of the file fragments routing improving the efficiency and time to completion of fragment distribution by defining the exact route, fragments should take to the destination. This is the first step in defining a custom protocol for the discovery of participating nodes and the efficient distribution of fragments in a mobile network. Future work will focus on the movement of fragments to avoid traffic analysis and avoid the collection of the entire fragment set that would enable an adversary to reconstruct the original piece of data.
Efficient Key-Rotatable and Security-Updatable Homomorphic Encryption. Proceedings of the Fifth ACM International Workshop on Security in Cloud Computing. :35–42.
.
2017. In this paper we presents the notion of key-rotatable and security-updatable homomorphic encryption (KR-SU-HE) scheme, which is a class of public-key homomorphic encryption in which the keys and the security of any ciphertext can be rotated and updated while still keeping the underlying plaintext intact and unrevealed. We formalise syntax and security notions for KR-SU-HE schemes and then build a concrete scheme based on the Learning With Errors assumption. We then perform testing implementation to show that our proposed scheme is efficiently practical.
Efficient tamper-evident logging of distributed systems via concurrent authenticated tree. 2017 IEEE 36th International Performance Computing and Communications Conference (IPCCC). :1–9.
.
2017. Secure logging as an indispensable part of any secure system in practice is well-understood by both academia and industry. However, providing security for audit logs on an untrusted machine in a large distributed system is still a challenging task. The emergence and wide availability of log management tools prompted plenty of work in the security community that allows clients or auditors to verify integrity of the log data. Most recent solutions to this problem focus on the space-efficiency or public verifiability of forward security. Unfortunately, existing secure audit logging schemes have significant performance limitations that make them impractical for realtime large-scale distributed applications: Existing cryptographic hashing is computationally expensive for logging in task intensive or resource-constrained systems especially to prove individual log events, while Merkle-tree approach has fundamental limitations when face with highly concurrent, large-scale log streams due to its serially appending feature. The verification step of Merkle-tree based approach requiring a logarithmic number of hash computations is becoming a bottleneck to improve the overall performance. There is a huge gap between the flux of log streams collected and the computational efficiency of integrity verification in the large-scale distributed systems. In this work, we develop a novel scheme, performance of which favorably compares with the existing solutions. The performance guarantees that we achieve stem from a novel data structure called concurrent authenticated tree, which allows log events concurrently appending and removes the need to wait for append operations to complete sequentially. We implement a prototype using chameleon hashing based on discrete log and Merkle history tree. A comprehensive experimental evaluation of the proposed and existing approaches is used to validate the analytical models and verify our claims. The results demonstrate that our proposed scheme verifying in a concurrent way is significantly more efficient than the previous tree-based approach.
Emotion Influenced Robotic Path Planning. Proceedings of the 2017 International Conference on Intelligent Systems, Metaheuristics & Swarm Intelligence. :130–136.
.
2017. We introduce an emotion influenced robotic path planning solution which offers the possibility of enabling emotions in the robot. The robot can change the speed of the path or learn where it should be and where it should not be. Most existing solutions for robotic path planning have no emotional influences. The most successful emotions were taken and included into the solution of this paper. The results were analyzed with regard to the time and speed it takes for a normal robotic path planning without emotions and with emotions of happiness, fear and novelty.
Empirical Analysis of Volatility Forecasting Model Based on Genetic Programming. Proceedings of the 2017 International Conference on Intelligent Systems, Metaheuristics & Swarm Intelligence. :74–77.
.
2017. In financial markets, the variance of stock returns plays an important role to reduce a risk, and daily volatility is often used as one of its measurement. We in this paper focus on Realized Volatility (RV), which is one of the most well-known volatility index. Traditionally regression models have been widely used to estimate it, but Genetic Programming (GP) approaches have been proposed recent years. While regression models estimate a suitable equation for forecasting RV, GP approaches estimate a tree (individual) that consists of economic information. Through evolution process, effective economic information can survive, so GP approaches can not only estimate RV values, but also extract effective information. However, GP approaches need computational efforts to avoid premature convergence. In this paper, we proposed a mutation-base GP approach for RV estimation, and analyze which economic information is needed to estimate RV accurately.
End Users Can Mitigate Zero Day Attacks Faster. 2017 IEEE 7th International Advance Computing Conference (IACC). :935—938.
.
2017. The past decade has shown us the power of cyber space and we getting dependent on the same. The exponential evolution in the domain has attracted attackers and defenders of technology equally. This inevitable domain has led to the increase in average human awareness and knowledge too. As we see the attack sophistication grow the protectors have always been a step ahead mitigating the attacks. A study of the various Threat Detection, Protection and Mitigation Systems revealed to us a common similarity wherein users have been totally ignored or the systems rely heavily on the user inputs for its correct functioning. Compiling the above we designed a study wherein user inputs were taken in addition to independent Detection and Prevention systems to identify and mitigate the risks. This approach led us to a conclusion that involvement of users exponentially enhances machine learning and segments the data sets faster for a more reliable output.
Ensuring information security by using Haskell's advanced type system. 2017 International Carnahan Conference on Security Technology (ICCST). :1–6.
.
2017. Protecting data confidentiality and integrity has become increasingly important in modern software. Sometimes, access control mechanisms come short and solutions on the application-level are needed. An approach can rely on enforcing information security using some features provided by certain programming languages. Several different solutions addressing this problem have been presented in literature, and entire new languages or libraries have been built from scratch. Some of them use type systems to let the compiler check for vulnerable code. In this way we are able to rule out those implementations which do not meet a certain security requirement. In this paper we use Haskell's type system to enforce three key properties of information security: non-interference and flexible declassification policies, strict input validation, and secure computations on untainted and trusted values. We present a functional lightweight library for applications with data integrity and confidentiality issues. Our contribute relies on a compile time enforcing of the aforementioned properties. Our library is wholly generalized and might be adapted for satisfying almost every security requirement.
Estimation of safe sensor measurements of autonomous system under attack. 2017 54th ACM/EDAC/IEEE Design Automation Conference (DAC). :1–6.
.
2017. The introduction of automation in cyber-physical systems (CPS) has raised major safety and security concerns. One attack vector is the sensing unit whose measurements can be manipulated by an adversary through attacks such as denial of service and delay injection. To secure an autonomous CPS from such attacks, we use a challenge response authentication (CRA) technique for detection of attack in active sensors data and estimate safe measurements using the recursive least square algorithm. For demonstrating effectiveness of our proposed approach, a car-follower model is considered where the follower vehicle's radar sensor measurements are manipulated in an attempt to cause a collision.
Evading Classifiers by Morphing in the Dark. Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security. :119–133.
.
2017. Learning-based systems have been shown to be vulnerable to evasion through adversarial data manipulation. These attacks have been studied under assumptions that the adversary has certain knowledge of either the target model internals, its training dataset or at least classification scores it assigns to input samples. In this paper, we investigate a much more constrained and realistic attack scenario wherein the target classifier is minimally exposed to the adversary, revealing only its final classification decision (e.g., reject or accept an input sample). Moreover, the adversary can only manipulate malicious samples using a blackbox morpher. That is, the adversary has to evade the targeted classifier by morphing malicious samples "in the dark". We present a scoring mechanism that can assign a real-value score which reflects evasion progress to each sample based on the limited information available. Leveraging on such scoring mechanism, we propose an evasion method – EvadeHC? and evaluate it against two PDF malware detectors, namely PDFRate and Hidost. The experimental evaluation demonstrates that the proposed evasion attacks are effective, attaining 100% evasion rate on the evaluation dataset. Interestingly, EvadeHC outperforms the known classifier evasion techniques that operate based on classification scores output by the classifiers. Although our evaluations are conducted on PDF malware classifiers, the proposed approaches are domain agnostic and are of wider application to other learning-based systems.
Evolution of logic locking. 2017 IFIP/IEEE International Conference on Very Large Scale Integration (VLSI-SoC). :1–6.
.
2017. The globalization of integrated circuit (IC) supply chain and the emergence of threats, such as intellectual property (IP) piracy, reverse engineering, and hardware Trojans, have forced semiconductor companies to revisit the trust in the supply chain. Logic locking is emerging as a popular and effective countermeasure against these threats. Over the years, multiple logic techniques have been developed. Moreover, a number of attacks have been proposed that expose the security vulnerabilities of these techniques. This paper highlights the key developments in the logic locking research and presents a comprehensive literature review of logic locking.
A Fast and Verified Software Stack for Secure Function Evaluation. Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security. :1989–2006.
.
2017. We present a high-assurance software stack for secure function evaluation (SFE). Our stack consists of three components: i. a verified compiler (CircGen) that translates C programs into Boolean circuits; ii. a verified implementation of Yao's SFE protocol based on garbled circuits and oblivious transfer; and iii. transparent application integration and communications via FRESCO, an open-source framework for secure multiparty computation (MPC). CircGen is a general purpose tool that builds on CompCert, a verified optimizing compiler for C. It can be used in arbitrary Boolean circuit-based cryptography deployments. The security of our SFE protocol implementation is formally verified using EasyCrypt, a tool-assisted framework for building high-confidence cryptographic proofs, and it leverages a new formalization of garbled circuits based on the framework of Bellare, Hoang, and Rogaway (CCS 2012). We conduct a practical evaluation of our approach, and conclude that it is competitive with state-of-the-art (unverified) approaches. Our work provides concrete evidence of the feasibility of building efficient, verified, implementations of higher-level cryptographic systems. All our development is publicly available.
Fast Searchable Encryption With Tunable Locality. Proceedings of the 2017 ACM International Conference on Management of Data. :1053–1067.
.
2017. Searchable encryption (SE) allows a client to outsource a dataset to an untrusted server while enabling the server to answer keyword queries in a private manner. SE can be used as a building block to support more expressive private queries such as range/point and boolean queries, while providing formal security guarantees. To scale SE to big data using external memory, new schemes with small locality have been proposed, where locality is defined as the number of non-continuous reads that the server makes for each query. Previous space-efficient SE schemes achieve optimal locality by increasing the read efficiency-the number of additional memory locations (false positives) that the server reads per result item. This can hurt practical performance. In this work, we design, formally prove secure, and evaluate the first SE scheme with tunable locality and linear space. Our first scheme has optimal locality and outperforms existing approaches (that have a slightly different leakage profile) by up to 2.5 orders of magnitude in terms of read efficiency, for all practical database sizes. Another version of our construction with the same leakage as previous works can be tuned to have bounded locality, optimal read efficiency and up to 60x more efficient end-to-end search time. We demonstrate that our schemes work fast in in-memory as well, leading to search time savings of up to 1 order of magnitude when compared to the most practical in-memory SE schemes. Finally, our construction can be tuned to achieve trade-offs between space, read efficiency, locality, parallelism and communication overhead.
Feasibility Analysis of Lattice-based Proxy Re-Encryption. Proceedings of the 2017 International Conference on Cryptography, Security and Privacy. :12–16.
.
2017. Proxy Re-encryption (PRE) is a useful cryptographic structure who enables a semi-trusted proxy to convert a ciphertext for Alice into a ciphertext for Bob without seeing the corresponding plaintext. Although there are many PRE schemes in recent years, few of them are set up based on lattice. Not only this, these lattice-based PRE schemes are all more complicated than the traditional PRE schemes. In this paper, through the study of the common lattice problems such as the Small integer solution (SIS) and the Learning with Errors (LWE), we analyze the feasibility of efficient lattice-based PRE scheme combined with the previous results. Finally, we propose an efficient lattice-based PRE scheme L-PRE without losing the hardness of lattice problems.
FlashBack: Immersive Virtual Reality on Mobile Devices via Rendering Memoization. GetMobile: Mobile Comp. and Comm.. 20:23–27.
.
2017. Driven by recent advances in the mobile computing hardware ecosystem, wearable Virtual Reality (VR) is experiencing a boom in popularity, with many offerings becoming available. Modern VR head-mounted displays (HMDs) fall into two device classes: (i) Tethered HMDs: HMDs tethered to powerful, expensive gaming desktops, such as the Oculus Rift, HTC Vive, and Sony PlayStation VR; (ii) Mobile-rendered HMDs: self-contained, untethered HMDs that run on mobile phones slotted into head mounts, e.g., Google Cardboard and Samsung Gear VR.
A Flexible Approach Towards Security Validation. Proceedings of the 2017 Workshop on Automated Decision Making for Active Cyber Defense. :7–13.
.
2017. Validating security properties of complex distributed systems is a challenging problem by itself, let alone when the work needs to be performed under tight budget and time constraints on prototype systems with components at various maturity levels. This paper described a tailored approach to security evaluations involving a strategic combination of model-based quantification, emulation, and logical argumentation. By customizing the evaluation to fit existing budget and timelines, validators can achieve the most appropriate validation process, trading off fidelity with coverage across a number of different defense components and different maturity levels. We successfully applied this process to the validation of an overlay proxy network, analyzing the impact of five different defense attributes (together with combinations thereof) on access path establishment and anonymity.
Formal Synthesis of Stabilizing Controllers for Switched Systems. Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control. :111–120.
.
2017. In this paper, we describe an abstraction-based method for synthesizing a state-based switching control for stabilizing a family of dynamical systems. Given a set of dynamical systems and a set of polyhedral switching surfaces, the algorithm synthesizes a strategy that assigns to every surface the linear dynamics to switch to at the surface. Our algorithm constructs a finite game graph that consists of the switching surfaces as the existential nodes and the choices of the dynamics as the universal nodes. In addition, the edges capture quantitative information about the evolution of the distance of the state from the equilibrium point along the executions. A switching strategy for the family of dynamical systems is extracted by finding a strategy on the game graph which results in plays having a bounded weight. Such a strategy is obtained by reducing the problem to the strategy synthesis for an energy game, which is a well-studied problem in the literature. We have implemented our algorithm for polyhedral inclusion dynamics and linear dynamics. We illustrate our algorithm on examples from these two classes of systems.
Forward and Backward Private Searchable Encryption from Constrained Cryptographic Primitives. Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security. :1465–1482.
.
2017. Using dynamic Searchable Symmetric Encryption, a user with limited storage resources can securely outsource a database to an untrusted server, in such a way that the database can still be searched and updated efficiently. For these schemes, it would be desirable that updates do not reveal any information a priori about the modifications they carry out, and that deleted results remain inaccessible to the server a posteriori. If the first property, called forward privacy, has been the main motivation of recent works, the second one, backward privacy, has been overlooked. In this paper, we study for the first time the notion of backward privacy for searchable encryption. After giving formal definitions for different flavors of backward privacy, we present several schemes achieving both forward and backward privacy, with various efficiency trade-offs. Our constructions crucially rely on primitives such as constrained pseudo-random functions and puncturable encryption schemes. Using these advanced cryptographic primitives allows for a fine-grained control of the power of the adversary, preventing her from evaluating functions on selected inputs, or decrypting specific ciphertexts. In turn, this high degree of control allows our SSE constructions to achieve the stronger forms of privacy outlined above. As an example, we present a framework to construct forward-private schemes from range-constrained pseudo-random functions. Finally, we provide experimental results for implementations of our schemes, and study their practical efficiency.
A Framework for Universally Composable Diffie-Hellman Key Exchange. 2017 IEEE Symposium on Security and Privacy (SP). :881–900.
.
2017. The analysis of real-world protocols, in particular key exchange protocols and protocols building on these protocols, is a very complex, error-prone, and tedious task. Besides the complexity of the protocols itself, one important reason for this is that the security of the protocols has to be reduced to the security of the underlying cryptographic primitives for every protocol time and again. We would therefore like to get rid of reduction proofs for real-world key exchange protocols as much as possible and in many cases altogether, also for higher-level protocols which use the exchanged keys. So far some first steps have been taken in this direction. But existing work is still quite limited, and, for example, does not support Diffie-Hellman (DH) key exchange, a prevalent cryptographic primitive for real-world protocols. In this paper, building on work by Kusters and Tuengerthal, we provide an ideal functionality in the universal composability setting which supports several common cryptographic primitives, including DH key exchange. This functionality helps to avoid reduction proofs in the analysis of real-world protocols and often eliminates them completely. We also propose a new general ideal key exchange functionality which allows higherlevel protocols to use exchanged keys in an ideal way. As a proof of concept, we apply our framework to three practical DH key exchange protocols, namely ISO 9798-3, SIGMA, and OPTLS.