Position within the page tree

Start
Research
The iUC Framework

The iUC Framework

Flexible Universal Composability Made Simple

About the iUC Framework

The iUC framework is an expressive and user friendly universal composability model for the formal security analysis of protocols in a modular way. Universal composability is an important tool for taming the complexity of protocols by allowing for analyzing small parts of a protocol in isolation, which then directly implies security of the combined protocol. The iUC framework provides the so far best combination of expressiveness and ease of use in a universal composability model: it offers modeling conventions, including a template for specifying arbitrary protocols, and comes with a clear and simple syntax as well as sensible default values for many optional parts. At the same time, the iUC framework is highly customizable and includes only very minimal technical requirements, which allows for capturing a wide range of protocols and settings in natural and intuitive ways.

Features of the iUC Framework

The iUC framework provides full and seamless support for, besides others, all of the following:

All types of protocols considered in the universal composability literature, such as real, ideal, hybrid, joint-state, and global state protocols
Many interesting protocol features such as:
- flexible protocol structures that allow for connecting individual protocol components in arbitrary ways
- protocols with and without disjoint sessions
- state that can be shared arbitrarily, even across sessions
- locally chosen and/or globally managed session identifiers
- protocols with and without runtime exhaustion
- arbitrary combinations of all of the above
All composition types from the universal composability literature, including composition of protocols with/without disjoint sessions, composition with joint-state, composition with global state.
Composition types that have not been considered in the literature so far, such as a new type of joint-state composition for multiple protocols as well as combinations of the above composition types.

All of the above is supported via just a single template and a single main composition theorem, which is in contrast to many other universal composability models and is an important property that makes iUC more user friendly.

History

The iUC framework was created as an instantiation of the IITM model and published at [AsiaCrypt2019]. The IITM model, published at [CSFW06] with a full and revised version to appear in the Journal of Cryptology (see [eprint13] for the technical report), is a general model for universal composability that was developed by our institute. While the IITM model is very expressive, it, however, does not provide any modeling tools and hence requires some effort to model a protocol. These tools and conventions are added by the iUC framework to create the most expressive yet user friendly universal composability model to date. Both the IITM model and its instantiation the iUC framework have already been used successfully to model and analyze a wide range of protocols in a modular way (see literature below).

Literature and Publications

2023
1. Mike Graf, Ralf Küsters, and Daniel Rausch, “AUC: Accountable Universal Composability,” in IEEE Symposium on Security and Privacy (S&P 2023), IEEE, 2023, pp. 1148--1167.
  Abstract
  Accountability is a well-established and widely used security concept that allows for obtaining undeniable cryptographic proof of misbehavior, thereby incentivizing honest behavior. There already exist several general purpose accountability frameworks for formal game-based security analyses. Unfortunately, such game-based frameworks do not support modular security analyses, which is an important tool to handle the complexity of modern protocols. Universal composability (UC) models provide native support for modular analyses, including re-use and composition of security results. So far, accountability has mainly been modeled and analyzed in UC models for the special case of MPC protocols, with a general purpose accountability framework for UC still missing. That is, a framework that among others supports arbitrary protocols, a wide range of accountability properties, handling and mixing of accountable and non-accountable security properties, and modular analysis of accountable protocols. To close this gap, we propose AUC, the first general purpose accountability framework for UC models, which supports all of the above, based on several new concepts. We exemplify AUC in three case studies not covered by existing works. In particular, AUC unifies existing UC accountability approaches within a single framework.
  BibTeX
  @inproceedings{GrafKuestersRausch-SP-2023, abstract = {Accountability is a well-established and widely used security concept that allows for obtaining undeniable cryptographic proof of misbehavior, thereby incentivizing honest behavior. There already exist several general purpose accountability frameworks for formal game-based security analyses. Unfortunately, such game-based frameworks do not support modular security analyses, which is an important tool to handle the complexity of modern protocols. Universal composability (UC) models provide native support for modular analyses, including re-use and composition of security results. So far, accountability has mainly been modeled and analyzed in UC models for the special case of MPC protocols, with a general purpose accountability framework for UC still missing. That is, a framework that among others supports arbitrary protocols, a wide range of accountability properties, handling and mixing of accountable and non-accountable security properties, and modular analysis of accountable protocols. To close this gap, we propose AUC, the first general purpose accountability framework for UC models, which supports all of the above, based on several new concepts. We exemplify AUC in three case studies not covered by existing works. In particular, AUC unifies existing UC accountability approaches within a single framework.}, author = {Graf, Mike and K{\"u}sters, Ralf and Rausch, Daniel}, booktitle = {{IEEE} Symposium on Security and Privacy (S{\&}P 2023)}, doi = {10.1109/SP46215.2023.10179384}, pages = {1148--1167}, publisher = {{IEEE}}, title = {{AUC: Accountable Universal Composability}}, url = {https://publ.sec.uni-stuttgart.de/grafkuestersrausch-sp-2023.pdf}, year = 2023 }
  Link
  https://publ.sec.uni-stuttgart.de/grafkuestersrausch-sp-2023.pdf
  DOI
  10.1109/SP46215.2023.10179384
2022
1. Mike Graf, Ralf Küsters, and Daniel Rausch, “AUC: Accountable Universal Composability,” Cryptology ePrint Archive, Technical Report 2022/1606, 2022.
  Abstract
  Accountability is a well-established and widely used security concept that allows for obtaining undeniable cryptographic proof of misbehavior, thereby incentivizing honest behavior. There already exist several general purpose accountability frameworks for formal game-based security analyses. Unfortunately, such game-based frameworks do not support modular security analyses, which is an important tool to handle the complexity of modern protocols. Universal composability (UC) models provide native support for modular analyses, including re-use and composition of security results. So far, accountability has mainly been modeled and analyzed in UC models for the special case of MPC protocols, with a general purpose accountability framework for UC still missing. That is, a framework that among others supports arbitrary protocols, a wide range of accountability properties, handling and mixing of accountable and non-accountable security properties, and modular analysis of accountable protocols. To close this gap, we propose AUC, the first general purpose accountability framework for UC models, which supports all of the above, based on several new concepts. We exemplify AUC in three case studies not covered by existing works. In particular, AUC unifies existing UC accountability approaches within a single framework.
  BibTeX
  @techreport{GrafKuestersRausch-IACR-2022, abstract = {Accountability is a well-established and widely used security concept that allows for obtaining undeniable cryptographic proof of misbehavior, thereby incentivizing honest behavior. There already exist several general purpose accountability frameworks for formal game-based security analyses. Unfortunately, such game-based frameworks do not support modular security analyses, which is an important tool to handle the complexity of modern protocols. Universal composability (UC) models provide native support for modular analyses, including re-use and composition of security results. So far, accountability has mainly been modeled and analyzed in UC models for the special case of MPC protocols, with a general purpose accountability framework for UC still missing. That is, a framework that among others supports arbitrary protocols, a wide range of accountability properties, handling and mixing of accountable and non-accountable security properties, and modular analysis of accountable protocols. To close this gap, we propose AUC, the first general purpose accountability framework for UC models, which supports all of the above, based on several new concepts. We exemplify AUC in three case studies not covered by existing works. In particular, AUC unifies existing UC accountability approaches within a single framework.}, author = {Graf, Mike and K{\"u}sters, Ralf and Rausch, Daniel}, institution = {Cryptology ePrint Archive}, number = {2022/1606}, title = {{AUC: Accountable Universal Composability}}, type = {Technical Report}, url = {https://publ.sec.uni-stuttgart.de/grafkuestersrausch-iacr-2022.pdf}, year = 2022 }
  Link
  https://publ.sec.uni-stuttgart.de/grafkuestersrausch-iacr-2022.pdf
2. Daniel Rausch, Ralf Küsters, and Céline Chevalier, “Embedding the UC Model into the IITM Model,” in Advances in Cryptology - EUROCRYPT 2022, O. Dunkelman and S. Dziembowski (Eds.), Springer, 2022, pp. 242--272.
  Abstract
  Universal Composability is a widely used concept for the design and analysis of protocols. Since Canetti's original UC model and the model by Pfitzmann and Waidner several different models for universal composability have been proposed, including, for example, the IITM model, GNUC, CC, but also extensions and restrictions of the UC model, such as JUC, GUC, and SUC. These were motivated by the lack of expressivity of existing models, ease of use, or flaws in previous models. Cryptographers choose between these models based on their needs at hand (e.g., support for joint state and global state) or simply their familiarity with a specific model. While all models follow the same basic idea, there are huge conceptually differences, which raises fundamental and practical questions: (How) do the concepts and results proven in one model relate to those in another model? Do the different models and the security notions formulated therein capture the same classes of attacks? Most importantly, can cryptographers re-use results proven in one model in another model, and if so, how? In this paper, we initiate a line of research with the aim to address this lack of understanding, consolidate the space of models, and enable cryptographers to re-use results proven in other models. As a start, here we focus on Canetti's prominent UC model and the IITM model proposed by Kuesters et al. The latter is an interesting candidate for comparison with the UC model since it has been used to analyze a wide variety of protocols, supports a very general protocol class and provides, among others, seamless treatment of protocols with shared state, including joint and global state. Our main technical contribution is an embedding of the UC model into the IITM model showing that all UC protocols, security and composition results carry over to the IITM model. Hence, protocol designers can profit from the features of the IITM model while being able to use all their results proven in the UC model. We also show that, in general, one cannot embed the full IITM model into the UC model.
  BibTeX
  @inproceedings{RauschKuestersChevalier-EUROCRYPT-2022, abstract = {Universal Composability is a widely used concept for the design and analysis of protocols. Since Canetti's original UC model and the model by Pfitzmann and Waidner several different models for universal composability have been proposed, including, for example, the IITM model, GNUC, CC, but also extensions and restrictions of the UC model, such as JUC, GUC, and SUC. These were motivated by the lack of expressivity of existing models, ease of use, or flaws in previous models. Cryptographers choose between these models based on their needs at hand (e.g., support for joint state and global state) or simply their familiarity with a specific model. While all models follow the same basic idea, there are huge conceptually differences, which raises fundamental and practical questions: (How) do the concepts and results proven in one model relate to those in another model? Do the different models and the security notions formulated therein capture the same classes of attacks? Most importantly, can cryptographers re-use results proven in one model in another model, and if so, how? In this paper, we initiate a line of research with the aim to address this lack of understanding, consolidate the space of models, and enable cryptographers to re-use results proven in other models. As a start, here we focus on Canetti's prominent UC model and the IITM model proposed by Kuesters et al. The latter is an interesting candidate for comparison with the UC model since it has been used to analyze a wide variety of protocols, supports a very general protocol class and provides, among others, seamless treatment of protocols with shared state, including joint and global state. Our main technical contribution is an embedding of the UC model into the IITM model showing that all UC protocols, security and composition results carry over to the IITM model. Hence, protocol designers can profit from the features of the IITM model while being able to use all their results proven in the UC model. We also show that, in general, one cannot embed the full IITM model into the UC model.}, author = {Rausch, Daniel and K{\"{u}}sters, Ralf and Chevalier, C{\'{e}}line}, booktitle = {{Advances in Cryptology - EUROCRYPT 2022}}, doi = {10.1007/978-3-031-07085-3_9}, editor = {Dunkelman, Orr and Dziembowski, Stefan}, pages = {242--272}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {{Embedding the UC Model into the IITM Model}}, url = {https://publ.sec.uni-stuttgart.de/rauschkuesterschevalier-eurocrypt-2022.pdf}, volume = 13276, year = 2022 }
  Link
  https://publ.sec.uni-stuttgart.de/rauschkuesterschevalier-eurocrypt-2022.pdf
  DOI
  10.1007/978-3-031-07085-3_9
3. Daniel Rausch, Ralf Küsters, and Céline Chevalier, “Embedding the UC Model into the IITM Model,” Cryptology ePrint Archive, Technical Report 2022/224, 2022.
  Abstract
  Universal Composability is a widely used concept for the design and analysis of protocols. Since Canetti's original UC model and the model by Pfitzmann and Waidner several different models for universal composability have been proposed, including, for example, the IITM model, GNUC, CC, but also extensions and restrictions of the UC model, such as JUC, GUC, and SUC. These were motivated by the lack of expressivity of existing models, ease of use, or flaws in previous models. Cryptographers choose between these models based on their needs at hand (e.g., support for joint state and global state) or simply their familiarity with a specific model. While all models follow the same basic idea, there are huge conceptually differences, which raises fundamental and practical questions: (How) do the concepts and results proven in one model relate to those in another model? Do the different models and the security notions formulated therein capture the same classes of attacks? Most importantly, can cryptographers re-use results proven in one model in another model, and if so, how? In this paper, we initiate a line of research with the aim to address this lack of understanding, consolidate the space of models, and enable cryptographers to re-use results proven in other models. As a start, here we focus on Canetti's prominent UC model and the IITM model proposed by Kuesters et al. The latter is an interesting candidate for comparison with the UC model since it has been used to analyze a wide variety of protocols, supports a very general protocol class and provides, among others, seamless treatment of protocols with shared state, including joint and global state. Our main technical contribution is an embedding of the UC model into the IITM model showing that all UC protocols, security and composition results carry over to the IITM model. Hence, protocol designers can profit from the features of the IITM model while being able to use all their results proven in the UC model. We also show that, in general, one cannot embed the full IITM model into the UC model.
  BibTeX
  @techreport{RauschKuestersChevalier-IACR-2022-224, abstract = {Universal Composability is a widely used concept for the design and analysis of protocols. Since Canetti's original UC model and the model by Pfitzmann and Waidner several different models for universal composability have been proposed, including, for example, the IITM model, GNUC, CC, but also extensions and restrictions of the UC model, such as JUC, GUC, and SUC. These were motivated by the lack of expressivity of existing models, ease of use, or flaws in previous models. Cryptographers choose between these models based on their needs at hand (e.g., support for joint state and global state) or simply their familiarity with a specific model. While all models follow the same basic idea, there are huge conceptually differences, which raises fundamental and practical questions: (How) do the concepts and results proven in one model relate to those in another model? Do the different models and the security notions formulated therein capture the same classes of attacks? Most importantly, can cryptographers re-use results proven in one model in another model, and if so, how? In this paper, we initiate a line of research with the aim to address this lack of understanding, consolidate the space of models, and enable cryptographers to re-use results proven in other models. As a start, here we focus on Canetti's prominent UC model and the IITM model proposed by Kuesters et al. The latter is an interesting candidate for comparison with the UC model since it has been used to analyze a wide variety of protocols, supports a very general protocol class and provides, among others, seamless treatment of protocols with shared state, including joint and global state. Our main technical contribution is an embedding of the UC model into the IITM model showing that all UC protocols, security and composition results carry over to the IITM model. Hence, protocol designers can profit from the features of the IITM model while being able to use all their results proven in the UC model. We also show that, in general, one cannot embed the full IITM model into the UC model.}, author = {Rausch, Daniel and K{\"{u}}sters, Ralf and Chevalier, C{\'{e}}line}, institution = {Cryptology ePrint Archive}, number = {2022/224}, title = {{Embedding the UC Model into the IITM Model}}, type = {Technical Report}, url = {https://publ.sec.uni-stuttgart.de/rauschkuesterschevalier-iacr-2022-224.pdf}, year = 2022 }
  Link
  https://publ.sec.uni-stuttgart.de/rauschkuesterschevalier-iacr-2022-224.pdf
2021
1. Mike Graf, Daniel Rausch, Viktoria Ronge, Christoph Egger, Ralf Küsters, and Dominique Schröder, “A Security Framework for Distributed Ledgers,” in ACM Conference on Computer and Communications Security (CCS 2021), ACM, 2021, pp. 1043--1064.
  Abstract
  In the past few years blockchains have been a major focus for security research, resulting in significant progress in the design, formalization, and analysis of blockchain protocols. However, the more general class of distributed ledgers, which includes not just blockchains but also prominent non-blockchain protocols, such as Corda and OmniLedger, cannot be covered by the state-of-the-art in the security literature yet. These distributed ledgers often break with traditional blockchain paradigms, such as block structures to store data, system-wide consensus, or global consistency. In this paper, we close this gap by proposing the first framework for defining and analyzing the security of general distributed ledgers, with an ideal distributed ledger functionality at the core of our contribution. This functionality covers not only classical blockchains but also non-blockchain distributed ledgers in a unified way. To illustrate our ledger functionality, we first show that the prominent ideal blockchain functionalities from Badertscher et al. and its privacy preserving derivative from Kerber et al. realize (suitable instantiations of) our functionality, which precisely captures their security properties. This immediately implies that their respective implementations, including Bitcoin, Ouroboros Genesis, and Ouroboros Crypsinous, realize our ideal ledger functionality as well. Secondly, we demonstrate that our ideal ledger functionality is capable of precisely modeling also non-blockchain distributed ledgers by performing the first formal security analysis of such a distributed ledger, namely the prominent Corda protocol. Due to the wide spread use of Corda in the industry, in particular the financial sector, this analysis is of independent interest. These results also illustrate that our ideal ledger functionality not just generalizes the modular treatment of blockchains to distributed ledgers, but moreover helps to unify existing results.
  BibTeX
  @inproceedings{GrafRauschRongeEggerKuestersSchroeder-CCS-2021, abstract = {In the past few years blockchains have been a major focus for security research, resulting in significant progress in the design, formalization, and analysis of blockchain protocols. However, the more general class of distributed ledgers, which includes not just blockchains but also prominent non-blockchain protocols, such as Corda and OmniLedger, cannot be covered by the state-of-the-art in the security literature yet. These distributed ledgers often break with traditional blockchain paradigms, such as block structures to store data, system-wide consensus, or global consistency. In this paper, we close this gap by proposing the first framework for defining and analyzing the security of general distributed ledgers, with an ideal distributed ledger functionality at the core of our contribution. This functionality covers not only classical blockchains but also non-blockchain distributed ledgers in a unified way. To illustrate our ledger functionality, we first show that the prominent ideal blockchain functionalities from Badertscher et al. and its privacy preserving derivative from Kerber et al. realize (suitable instantiations of) our functionality, which precisely captures their security properties. This immediately implies that their respective implementations, including Bitcoin, Ouroboros Genesis, and Ouroboros Crypsinous, realize our ideal ledger functionality as well. Secondly, we demonstrate that our ideal ledger functionality is capable of precisely modeling also non-blockchain distributed ledgers by performing the first formal security analysis of such a distributed ledger, namely the prominent Corda protocol. Due to the wide spread use of Corda in the industry, in particular the financial sector, this analysis is of independent interest. These results also illustrate that our ideal ledger functionality not just generalizes the modular treatment of blockchains to distributed ledgers, but moreover helps to unify existing results.}, author = {Graf, Mike and Rausch, Daniel and Ronge, Viktoria and Egger, Christoph and K{\"u}sters, Ralf and Schr{\"o}der, Dominique}, booktitle = {{ACM Conference on Computer and Communications Security (CCS 2021)}}, doi = {10.1145/3460120.3485362}, pages = {1043--1064}, publisher = {{ACM}}, title = {{A Security Framework for Distributed Ledgers}}, url = {https://publ.sec.uni-stuttgart.de/grafrauschrongeeggerkuestersschroeder-ccs-2021.pdf}, year = 2021 }
  Link
  https://publ.sec.uni-stuttgart.de/grafrauschrongeeggerkuestersschroeder-ccs-2021.pdf
  DOI
  10.1145/3460120.3485362
2. Mike Graf, Daniel Rausch, Viktoria Ronge, Christoph Egger, Ralf Küsters, and Dominique Schröder, “A Security Framework for Distributed Ledgers,” Cryptology ePrint Archive, Technical Report 2021/145, 2021.
  Abstract
  In the past few years blockchains have been a major focus for security research, resulting in significant progress in the design, formalization, and analysis of blockchain protocols. However, the more general class of distributed ledgers, which includes not just blockchains but also prominent non-blockchain protocols, such as Corda and OmniLedger, cannot be covered by the state-of-the-art in the security literature yet. These distributed ledgers often break with traditional blockchain paradigms, such as block structures to store data, system-wide consensus, or global consistency. In this paper, we close this gap by proposing the first framework for defining and analyzing the security of general distributed ledgers, with an ideal distributed ledger functionality at the core of our contribution. This functionality covers not only classical blockchains but also non-blockchain distributed ledgers in a unified way. To illustrate our ledger functionality, we first show that the prominent ideal blockchain functionalities from Badertscher et al. and its privacy preserving derivative from Kerber et al. realize (suitable instantiations of) our functionality, which precisely captures their security properties. This immediately implies that their respective implementations, including Bitcoin, Ouroboros Genesis, and Ouroboros Crypsinous, realize our ideal ledger functionality as well. Secondly, we demonstrate that our ideal ledger functionality is capable of precisely modeling also non-blockchain distributed ledgers by performing the first formal security analysis of such a distributed ledger, namely the prominent Corda protocol. Due to the wide spread use of Corda in the industry, in particular the financial sector, this analysis is of independent interest. These results also illustrate that our ideal ledger functionality not just generalizes the modular treatment of blockchains to distributed ledgers, but moreover helps to unify existing results.
  BibTeX
  @techreport{GrafRauschRongeEggerKuestersSchroeder-IACR-2021, abstract = {In the past few years blockchains have been a major focus for security research, resulting in significant progress in the design, formalization, and analysis of blockchain protocols. However, the more general class of distributed ledgers, which includes not just blockchains but also prominent non-blockchain protocols, such as Corda and OmniLedger, cannot be covered by the state-of-the-art in the security literature yet. These distributed ledgers often break with traditional blockchain paradigms, such as block structures to store data, system-wide consensus, or global consistency. In this paper, we close this gap by proposing the first framework for defining and analyzing the security of general distributed ledgers, with an ideal distributed ledger functionality at the core of our contribution. This functionality covers not only classical blockchains but also non-blockchain distributed ledgers in a unified way. To illustrate our ledger functionality, we first show that the prominent ideal blockchain functionalities from Badertscher et al. and its privacy preserving derivative from Kerber et al. realize (suitable instantiations of) our functionality, which precisely captures their security properties. This immediately implies that their respective implementations, including Bitcoin, Ouroboros Genesis, and Ouroboros Crypsinous, realize our ideal ledger functionality as well. Secondly, we demonstrate that our ideal ledger functionality is capable of precisely modeling also non-blockchain distributed ledgers by performing the first formal security analysis of such a distributed ledger, namely the prominent Corda protocol. Due to the wide spread use of Corda in the industry, in particular the financial sector, this analysis is of independent interest. These results also illustrate that our ideal ledger functionality not just generalizes the modular treatment of blockchains to distributed ledgers, but moreover helps to unify existing results.}, author = {Graf, Mike and Rausch, Daniel and Ronge, Viktoria and Egger, Christoph and K{\"u}sters, Ralf and Schr{\"o}der, Dominique}, institution = {Cryptology ePrint Archive}, number = {2021/145}, title = {{A Security Framework for Distributed Ledgers}}, type = {Technical Report}, url = {https://publ.sec.uni-stuttgart.de/grafrauschrongeeggerkuestersschroeder-iacr-2021.pdf}, year = 2021 }
  Link
  https://publ.sec.uni-stuttgart.de/grafrauschrongeeggerkuestersschroeder-iacr-2021.pdf
2020
1. Daniel Rausch, “Simple and flexible universal composability: definition of a framework and applications,” PhD thesis. University of Stuttgart, Germany, 2020.
  - Abstract
  - BibTeX
  Abstract
  Security protocols, such as TLS, SSH, IEEE 802.11, and DNSSEC, have become crucial tools in modern society to protect people, data, and infrastructure. They are used throughout virtually all electronic devices to achieve a wide range of different security goals, such as confidentiality, authentication, and integrity. As the long history of attacks on security protocols illustrates, it is indispensable to perform a formal security analysis of such protocols. A central tool in cryptography for taming the complexity of the design and the analysis of modern protocols is modularity, provided by security models for universal composability. Such models allow for designing and analyzing small parts of a protocol in isolation and then reusing these security results in the context of the overall protocol. This is not just easier than analyzing the whole protocol as a monolithic block but also reduces the overall effort required in building and analyzing multiple different protocols based on the same underlying components, such as cryptographic primitives. Ideally, a model for universal composability should support a protocol designer in easily creating full, precise, and detailed specifications as well as sound security proofs of various protocols for various types of adversarial models, instead of being an additional obstacle one has to overcome during a security analysis. In particular, such a model should be sound, flexible/expressive, and easy to use. Unfortunately, despite the wide spread use of models for universal composability, existing models and frameworks are still unsatisfying in these respects as none combines all of these requirements simultaneously. In this thesis we therefore develop a model for universal composability, called the iUC framework, which combines soundness, usability, and flexibility in a so far unmatched way, and hence constitutes a solid framework for designing and analyzing essentially any protocol and application in a modular, universally composable, and sound manner. We use our model in a case study to analyze multiple different key exchange protocols precisely as they are deployed in practice. This illustrates the combination of both flexibility and usability of our model. This case study is also an important independent contribution as this is the first faithful security analysis of these unmodified protocols in a universal composability setting.
  BibTeX
  @phdthesis{Rausch-Phd-2020, abstract = {Security protocols, such as TLS, SSH, IEEE 802.11, and DNSSEC, have become crucial tools in modern society to protect people, data, and infrastructure. They are used throughout virtually all electronic devices to achieve a wide range of different security goals, such as confidentiality, authentication, and integrity. As the long history of attacks on security protocols illustrates, it is indispensable to perform a formal security analysis of such protocols. A central tool in cryptography for taming the complexity of the design and the analysis of modern protocols is modularity, provided by security models for universal composability. Such models allow for designing and analyzing small parts of a protocol in isolation and then reusing these security results in the context of the overall protocol. This is not just easier than analyzing the whole protocol as a monolithic block but also reduces the overall effort required in building and analyzing multiple different protocols based on the same underlying components, such as cryptographic primitives. Ideally, a model for universal composability should support a protocol designer in easily creating full, precise, and detailed specifications as well as sound security proofs of various protocols for various types of adversarial models, instead of being an additional obstacle one has to overcome during a security analysis. In particular, such a model should be sound, flexible/expressive, and easy to use. Unfortunately, despite the wide spread use of models for universal composability, existing models and frameworks are still unsatisfying in these respects as none combines all of these requirements simultaneously. In this thesis we therefore develop a model for universal composability, called the iUC framework, which combines soundness, usability, and flexibility in a so far unmatched way, and hence constitutes a solid framework for designing and analyzing essentially any protocol and application in a modular, universally composable, and sound manner. We use our model in a case study to analyze multiple different key exchange protocols precisely as they are deployed in practice. This illustrates the combination of both flexibility and usability of our model. This case study is also an important independent contribution as this is the first faithful security analysis of these unmodified protocols in a universal composability setting.}, author = {Rausch, Daniel}, school = {University of Stuttgart, Germany}, title = {{Simple and flexible universal composability: definition of a framework and applications}}, type = {PhD thesis}, year = 2020 }
2. Ralf Küsters, Max Tuengerthal, and Daniel Rausch, “Joint State Theorems for Public-Key Encryption and Digital Signature Functionalities with Local Computation,” Journal of Cryptology, vol. 33, no. 4, pp. 1585--1658, 2020.
  Abstract
  Composition theorems in simulation-based approaches allow to build complex protocols from sub-protocols in a modular way. However, as first pointed out and studied by Canetti and Rabin, this modular approach often leads to impractical implementations. For example, when using a functionality for digital signatures within a more complex protocol, parties have to generate new verification and signing keys for every session of the protocol. This motivates to generalize composition theorems to so-called joint state theorems, where different copies of a functionality may share some state, e.g., the same verification and signing keys. In this paper, we present a joint state theorem which is more general than the original theorem of Canetti and Rabin, for which several problems and limitations are pointed out. We apply our theorem to obtain joint state realizations for three functionalities: public-key encryption, replayable public-key encryption, and digital signatures. Unlike most other formulations, our functionalities model that ciphertexts and signatures are computed locally, rather than being provided by the adversary. To obtain the joint state realizations, the functionalities have to be designed carefully. Other formulations are shown to be unsuitable. Our work is based on a recently proposed, rigorous model for simulation-based security by Küsters, called the IITM model. Our definitions and results demonstrate the expressivity and simplicity of this model. For example, unlike Canetti's UC model, in the IITM model no explicit joint state operator needs to be defined and the joint state theorem follows immediately from the composition theorem in the IITM model.
  BibTeX
  @article{KuestersTuengerthalRausch-JointState-JOC-2020, abstract = {Composition theorems in simulation-based approaches allow to build complex protocols from sub-protocols in a modular way. However, as first pointed out and studied by Canetti and Rabin, this modular approach often leads to impractical implementations. For example, when using a functionality for digital signatures within a more complex protocol, parties have to generate new verification and signing keys for every session of the protocol. This motivates to generalize composition theorems to so-called joint state theorems, where different copies of a functionality may share some state, e.g., the same verification and signing keys. In this paper, we present a joint state theorem which is more general than the original theorem of Canetti and Rabin, for which several problems and limitations are pointed out. We apply our theorem to obtain joint state realizations for three functionalities: public-key encryption, replayable public-key encryption, and digital signatures. Unlike most other formulations, our functionalities model that ciphertexts and signatures are computed locally, rather than being provided by the adversary. To obtain the joint state realizations, the functionalities have to be designed carefully. Other formulations are shown to be unsuitable. Our work is based on a recently proposed, rigorous model for simulation-based security by K{\"u}sters, called the IITM model. Our definitions and results demonstrate the expressivity and simplicity of this model. For example, unlike Canetti's UC model, in the IITM model no explicit joint state operator needs to be defined and the joint state theorem follows immediately from the composition theorem in the IITM model.}, author = {K{\"u}sters, Ralf and Tuengerthal, Max and Rausch, Daniel}, doi = {10.1007/s00145-020-09353-0}, journal = {{Journal of Cryptology}}, number = 4, pages = {1585--1658}, title = {{Joint State Theorems for Public-Key Encryption and Digital Signature Functionalities with Local Computation}}, url = {https://publ.sec.uni-stuttgart.de/kuesterstuengerthalrausch-jointstate-joc-2020.pdf}, volume = 33, year = 2020 }
  Link
  https://publ.sec.uni-stuttgart.de/kuesterstuengerthalrausch-jointstate-joc-2020.pdf
  DOI
  10.1007/s00145-020-09353-0
3. Ralf Küsters, Max Tuengerthal, and Daniel Rausch, “The IITM Model: a Simple and Expressive Model for Universal Composability,” Journal of Cryptology, vol. 33, no. 4, pp. 1461--1584, 2020.
  Abstract
  The universal composability paradigm allows for the modular design and analysis of cryptographic protocols. It has been widely and successfully used in cryptography. However, devising a coherent yet simple and expressive model for universal composability is, as the history of such models shows, highly non-trivial. For example, several partly severe problems have been pointed out in the literature for the UC model. In this work, we propose a coherent model for universal composability, called the IITM model (``Inexhaustible Interactive Turing Machine''). A main feature of the model is that it is stated without a priori fixing irrelevant details, such as a specific way of addressing of machines by session and party identifiers, a specific modeling of corruption, or a specific protocol hierarchy. In addition, we employ a very general notion of runtime. All reasonable protocols and ideal functionalities should be expressible based on this notion in a direct and natural way, and without tweaks, such as (artificial) padding of messages or (artificially) adding extra messages. Not least because of these features, the model is simple and expressive. Also the general results that we prove, such as composition theorems, hold independently of how such details are fixed for concrete applications. Being inspired by other models for universal composability, in particular the UC model and because of the flexibility and expressivity of the IITM model, conceptually, results formulated in these models directly carry over to the IITM model.
  BibTeX
  @article{KuestersTuengerthalRausch-IITM-JOC-2020, abstract = {The universal composability paradigm allows for the modular design and analysis of cryptographic protocols. It has been widely and successfully used in cryptography. However, devising a coherent yet simple and expressive model for universal composability is, as the history of such models shows, highly non-trivial. For example, several partly severe problems have been pointed out in the literature for the UC model. In this work, we propose a coherent model for universal composability, called the IITM model (``Inexhaustible Interactive Turing Machine''). A main feature of the model is that it is stated without a priori fixing irrelevant details, such as a specific way of addressing of machines by session and party identifiers, a specific modeling of corruption, or a specific protocol hierarchy. In addition, we employ a very general notion of runtime. All reasonable protocols and ideal functionalities should be expressible based on this notion in a direct and natural way, and without tweaks, such as (artificial) padding of messages or (artificially) adding extra messages. Not least because of these features, the model is simple and expressive. Also the general results that we prove, such as composition theorems, hold independently of how such details are fixed for concrete applications. Being inspired by other models for universal composability, in particular the UC model and because of the flexibility and expressivity of the IITM model, conceptually, results formulated in these models directly carry over to the IITM model.}, author = {K{\"u}sters, Ralf and Tuengerthal, Max and Rausch, Daniel}, doi = {10.1007/s00145-020-09352-1}, journal = {{Journal of Cryptology}}, number = 4, pages = {1461--1584}, title = {{The IITM Model: a Simple and Expressive Model for Universal Composability}}, url = {https://publ.sec.uni-stuttgart.de/kuesterstuengerthalrausch-iitm-joc-2020.pdf}, volume = 33, year = 2020 }
  Link
  https://publ.sec.uni-stuttgart.de/kuesterstuengerthalrausch-iitm-joc-2020.pdf
  DOI
  10.1007/s00145-020-09352-1
2019
1. Jan Camenisch, Stephan Krenn, Ralf Küsters, and Daniel Rausch, “iUC: Flexible Universal Composability Made Simple,” in Advances in Cryptology - ASIACRYPT 2019, S. D. Galbraith and S. Moriai (Eds.), Springer, 2019, pp. 191--221.
  Abstract
  Proving the security of complex protocols is a crucial and very challenging task. A widely used ap- proach for reasoning about such protocols in a modular way is universal composability. Several models for this approach exist, including the UC, GNUC, and IITM models. Despite the wide spread use of the universal composability approach, none of the existing models are fully satisfying. They all lack either soundness, flexibility, or usability. As a result, proofs in the litera- ture are very often formally incorrect, protocols cannot be modeled faithfully, and/or using these models is a burden rather than a help. Given this dire state of affairs, the goal of this work is to provide a framework for universal composability which combines soundness, flexibility, and usability. Developing such a security framework is a very difficult and delicate task, as the long history of frameworks for universal composability shows. As the IITM model appears to be closest to this goal in terms of soundness and flexibility, we build our framework, called iUC, on top of the IITM model. At the core of iUC is a single simple template for spec- ifying essentially arbitrary protocols in a convenient, formally precise, and flexible way, which allows protocol designers to concentrate on the core logic of a protocol. We illustrate the main features of our framework with example functionalities and realizations.
  BibTeX
  @inproceedings{CamenischKrennKuestersRausch-ASIACRYPT-2019, abstract = {Proving the security of complex protocols is a crucial and very challenging task. A widely used ap- proach for reasoning about such protocols in a modular way is universal composability. Several models for this approach exist, including the UC, GNUC, and IITM models. Despite the wide spread use of the universal composability approach, none of the existing models are fully satisfying. They all lack either soundness, flexibility, or usability. As a result, proofs in the litera- ture are very often formally incorrect, protocols cannot be modeled faithfully, and/or using these models is a burden rather than a help. Given this dire state of affairs, the goal of this work is to provide a framework for universal composability which combines soundness, flexibility, and usability. Developing such a security framework is a very difficult and delicate task, as the long history of frameworks for universal composability shows. As the IITM model appears to be closest to this goal in terms of soundness and flexibility, we build our framework, called iUC, on top of the IITM model. At the core of iUC is a single simple template for spec- ifying essentially arbitrary protocols in a convenient, formally precise, and flexible way, which allows protocol designers to concentrate on the core logic of a protocol. We illustrate the main features of our framework with example functionalities and realizations.}, author = {Camenisch, Jan and Krenn, Stephan and K{\"{u}}sters, Ralf and Rausch, Daniel}, booktitle = {{Advances in Cryptology - ASIACRYPT 2019}}, doi = {10.1007/978-3-030-34618-8\_7}, editor = {Galbraith, Steven D. and Moriai, Shiho}, pages = {191--221}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {{iUC: Flexible Universal Composability Made Simple}}, url = {https://publ.sec.uni-stuttgart.de/camenischkrennkuestersrausch-asiacrypt-2019.pdf}, volume = 11923, year = 2019 }
  Link
  https://publ.sec.uni-stuttgart.de/camenischkrennkuestersrausch-asiacrypt-2019.pdf
  DOI
  10.1007/978-3-030-34618-8\_7
2. Jan Camenisch, Stephan Krenn, Ralf Küsters, and Daniel Rausch, “iUC: Flexible Universal Composability Made Simple,” Cryptology ePrint Archive, Technical Report 2019/1073, 2019.
  - Abstract
  - BibTeX
  Abstract
  Proving the security of complex protocols is a crucial and very challenging task. A widely used ap- proach for reasoning about such protocols in a modular way is universal composability. Several models for this approach exist, including the UC, GNUC, and IITM models. Despite the wide spread use of the universal composability approach, none of the existing models are fully satisfying. They all lack either soundness, flexibility, or usability. As a result, proofs in the litera- ture are very often formally incorrect, protocols cannot be modeled faithfully, and/or using these models is a burden rather than a help. Given this dire state of affairs, the goal of this work is to provide a framework for universal composability which combines soundness, flexibility, and usability. Developing such a security framework is a very difficult and delicate task, as the long history of frameworks for universal composability shows. As the IITM model appears to be closest to this goal in terms of soundness and flexibility, we build our framework, called iUC, on top of the IITM model. At the core of iUC is a single simple template for spec- ifying essentially arbitrary protocols in a convenient, formally precise, and flexible way, which allows protocol designers to concentrate on the core logic of a protocol. We illustrate the main features of our framework with example functionalities and realizations.
  BibTeX
  @techreport{CamenischKrennKuestersRausch-IACR-2019-1073, abstract = {Proving the security of complex protocols is a crucial and very challenging task. A widely used ap- proach for reasoning about such protocols in a modular way is universal composability. Several models for this approach exist, including the UC, GNUC, and IITM models. Despite the wide spread use of the universal composability approach, none of the existing models are fully satisfying. They all lack either soundness, flexibility, or usability. As a result, proofs in the litera- ture are very often formally incorrect, protocols cannot be modeled faithfully, and/or using these models is a burden rather than a help. Given this dire state of affairs, the goal of this work is to provide a framework for universal composability which combines soundness, flexibility, and usability. Developing such a security framework is a very difficult and delicate task, as the long history of frameworks for universal composability shows. As the IITM model appears to be closest to this goal in terms of soundness and flexibility, we build our framework, called iUC, on top of the IITM model. At the core of iUC is a single simple template for spec- ifying essentially arbitrary protocols in a convenient, formally precise, and flexible way, which allows protocol designers to concentrate on the core logic of a protocol. We illustrate the main features of our framework with example functionalities and realizations.}, author = {Camenisch, Jan and Krenn, Stephan and K{\"{u}}sters, Ralf and Rausch, Daniel}, institution = {Cryptology ePrint Archive}, number = {2019/1073}, title = {{iUC: Flexible Universal Composability Made Simple}}, type = {Technical Report}, year = 2019 }
2018
1. Ralf Küsters, Max Tuengerthal, and Daniel Rausch, “The IITM Model: a Simple and Expressive Model for Universal Composability,” Cryptology ePrint Archive, Technical Report 2013/025, 2018.
  Abstract
  The universal composability paradigm allows for the modular design and analysis of cryptographic protocols. It has been widely and successfully used in cryptography. However, devising a coherent yet simple and expressive model for universal composability is, as the history of such models shows, highly non-trivial. For example, several partly severe problems have been pointed out in the literature for the UC model. In this work, we propose a coherent model for universal composability, called the IITM model (``Inexhaustible Interactive Turing Machine''). A main feature of the model is that it is stated without a priori fixing irrelevant details, such as a specific way of addressing of machines by session and party identifiers, a specific modeling of corruption, or a specific protocol hierarchy. In addition, we employ a very general notion of runtime. All reasonable protocols and ideal functionalities should be expressible based on this notion in a direct and natural way, and without tweaks, such as (artificial) padding of messages or (artificially) adding extra messages. Not least because of these features, the model is simple and expressive. Also the general results that we prove, such as composition theorems, hold independently of how such details are fixed for concrete applications. Being inspired by other models for universal composability, in particular the UC model and because of the flexibility and expressivity of the IITM model, conceptually, results formulated in these models directly carry over to the IITM model.
  BibTeX
  @techreport{KuestersTuengerthalRausch-IACR-2013-025, abstract = {The universal composability paradigm allows for the modular design and analysis of cryptographic protocols. It has been widely and successfully used in cryptography. However, devising a coherent yet simple and expressive model for universal composability is, as the history of such models shows, highly non-trivial. For example, several partly severe problems have been pointed out in the literature for the UC model. In this work, we propose a coherent model for universal composability, called the IITM model (``Inexhaustible Interactive Turing Machine''). A main feature of the model is that it is stated without a priori fixing irrelevant details, such as a specific way of addressing of machines by session and party identifiers, a specific modeling of corruption, or a specific protocol hierarchy. In addition, we employ a very general notion of runtime. All reasonable protocols and ideal functionalities should be expressible based on this notion in a direct and natural way, and without tweaks, such as (artificial) padding of messages or (artificially) adding extra messages. Not least because of these features, the model is simple and expressive. Also the general results that we prove, such as composition theorems, hold independently of how such details are fixed for concrete applications. Being inspired by other models for universal composability, in particular the UC model and because of the flexibility and expressivity of the IITM model, conceptually, results formulated in these models directly carry over to the IITM model.}, author = {K{\"u}sters, Ralf and Tuengerthal, Max and Rausch, Daniel}, institution = {Cryptology ePrint Archive}, number = {2013/025}, title = {{The IITM Model: a Simple and Expressive Model for Universal Composability}}, type = {Technical Report}, url = {https://publ.sec.uni-stuttgart.de/kuesterstuengerthalrausch-iacr-2013-025.pdf}, year = 2018 }
  Link
  https://publ.sec.uni-stuttgart.de/kuesterstuengerthalrausch-iacr-2013-025.pdf
2017
1. Ralf Küsters and Daniel Rausch, “A Framework for Universally Composable Diffie-Hellman Key Exchange,” in 38th IEEE Symposium on Security and Privacy (S&P 2017), IEEE, 2017, pp. 881--900.
  Abstract
  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 Küsters 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 higher-level 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.
  BibTeX
  @inproceedings{KuestersRausch-SP-2017, abstract = {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 K{\"u}sters 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 higher-level 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.}, author = {K{\"u}sters, Ralf and Rausch, Daniel}, booktitle = {{38th IEEE Symposium on Security and Privacy (S{\&}P 2017)}}, doi = {10.1109/SP.2017.63}, pages = {881--900}, publisher = {{IEEE}}, title = {{A Framework for Universally Composable Diffie-Hellman Key Exchange}}, url = {https://publ.sec.uni-stuttgart.de/kuestersrausch-sp-2017.pdf}, year = 2017 }
  Link
  https://publ.sec.uni-stuttgart.de/kuestersrausch-sp-2017.pdf
  DOI
  10.1109/SP.2017.63
2. Ralf Küsters and Daniel Rausch, “A Framework for Universally Composable Diffie-Hellman Key Exchange,” Cryptology ePrint Archive, Technical Report 2017/256, 2017.
  Abstract
  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 Küsters 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 higher-level 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.
  BibTeX
  @techreport{KuestersRausch-IACR-2017-256, abstract = {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 K{\"u}sters 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 higher-level 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.}, author = {K{\"u}sters, Ralf and Rausch, Daniel}, institution = {Cryptology ePrint Archive}, number = {2017/256}, title = {{A Framework for Universally Composable Diffie-Hellman Key Exchange}}, type = {Technical Report}, url = {https://publ.sec.uni-stuttgart.de/kuestersrausch-iacr-2017-256.pdf}, year = 2017 }
  Link
  https://publ.sec.uni-stuttgart.de/kuestersrausch-iacr-2017-256.pdf
2016
1. Jan Camenisch, Robert R. Enderlein, Stephan Krenn, Ralf Küsters, and Daniel Rausch, “Universal Composition with Responsive Environments,” in Advances in Cryptology - ASIACRYPT 2016, J. H. Cheon and T. Takagi (Eds.), Springer, 2016, pp. 807--840.
  Abstract
  In universal composability frameworks, adversaries (or environments) and protocols/ideal functionalities often have to exchange meta-information on the network interface, such as algorithms, keys, signatures, ciphertexts, signaling information, corruption-related messages. For these purely modeling-related messages, which do not reflect actual network communication, it would often be very reasonable and natural to expect that adversaries/environments provide the requested information immediately or give control back to the protocol/functionality immediately after having received some information. However, in none of the existing models for universal composability this is guaranteed. We call this the non-responsiveness problem. As discussed in the paper, while formally non-responsiveness does not invalidate any of the universal composability models, it has many disadvantages, such as unnecessarily complex specifications and less expressivity. Also, this problem has often been ignored in the literature, leading to ill-defined and flawed specifications. Protocol designers really should not have to care about this problem at all, but currently they have to: giving the adversary/environment the option to not respond immediately to modeling-related requests does not translate to any real attack scenario. This paper solves the non-responsiveness problem and its negative consequences completely, by avoiding this artificial modeling problem altogether. We propose the new concepts of responsive environments and adversaries. Such environments and adversaries must provide a valid response to modeling-related requests before any other protocol/functionality is activated. Hence, protocol designers do not have to worry any longer about artifacts resulting from such requests not being answered promptly. Our concepts apply to all existing models for universal composability, as exemplified for the UC, GNUC, and IITM models, with full definitions and proofs (simulation relations, transitivity, equivalence of various simulation notions, composition theorems) provided for the IITM model.
  BibTeX
  @inproceedings{CamenischEnderleinKrennKuestersRausch-ASIACRYPT-2016, abstract = {In universal composability frameworks, adversaries (or environments) and protocols/ideal functionalities often have to exchange meta-information on the network interface, such as algorithms, keys, signatures, ciphertexts, signaling information, corruption-related messages. For these purely modeling-related messages, which do not reflect actual network communication, it would often be very reasonable and natural to expect that adversaries/environments provide the requested information immediately or give control back to the protocol/functionality immediately after having received some information. However, in none of the existing models for universal composability this is guaranteed. We call this the \emph{non-responsiveness problem}. As discussed in the paper, while formally non-responsiveness does not invalidate any of the universal composability models, it has many disadvantages, such as unnecessarily complex specifications and less expressivity. Also, this problem has often been ignored in the literature, leading to ill-defined and flawed specifications. Protocol designers really should not have to care about this problem at all, but currently they have to: giving the adversary/environment the option to not respond immediately to modeling-related requests does not translate to any real attack scenario. This paper solves the non-responsiveness problem and its negative consequences completely, by avoiding this artificial modeling problem altogether. We propose the new concepts of responsive environments and adversaries. Such environments and adversaries must provide a valid response to modeling-related requests before any other protocol/functionality is activated. Hence, protocol designers do not have to worry any longer about artifacts resulting from such requests not being answered promptly. Our concepts apply to all existing models for universal composability, as exemplified for the UC, GNUC, and IITM models, with full definitions and proofs (simulation relations, transitivity, equivalence of various simulation notions, composition theorems) provided for the IITM model.}, author = {Camenisch, Jan and Enderlein, Robert R. and Krenn, Stephan and K{\"u}sters, Ralf and Rausch, Daniel}, booktitle = {{Advances in Cryptology - ASIACRYPT 2016}}, doi = {10.1007/978-3-662-53890-6\_27}, editor = {Cheon, Jung Hee and Takagi, Tsuyoshi}, pages = {807--840}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {{Universal Composition with Responsive Environments}}, url = {https://publ.sec.uni-stuttgart.de/camenischenderleinkrennkuestersrausch-asiacrypt-2016.pdf}, volume = 10032, year = 2016 }
  Link
  https://publ.sec.uni-stuttgart.de/camenischenderleinkrennkuestersrausch-asiacrypt-2016.pdf
  DOI
  10.1007/978-3-662-53890-6\_27
2. Jan Camenisch, Robert R. Enderlein, Stephan Krenn, Ralf Küsters, and Daniel Rausch, “Universal Composition with Responsive Environments,” Cryptology ePrint Archive, Technical Report 2016/034, 2016.
  Abstract
  In universal composability frameworks, adversaries (or environments) and protocols/ideal functionalities often have to exchange meta-information on the network interface, such as algorithms, keys, signatures, ciphertexts, signaling information, corruption-related messages. For these purely modeling-related messages, which do not reflect actual network communication, it would often be very reasonable and natural to expect that adversaries/environments provide the requested information immediately or give control back to the protocol/functionality immediately after having received some information. However, in none of the existing models for universal composability this is guaranteed. We call this the non-responsiveness problem. As discussed in the paper, while formally non-responsiveness does not invalidate any of the universal composability models, it has many disadvantages, such as unnecessarily complex specifications and less expressivity. Also, this problem has often been ignored in the literature, leading to ill-defined and flawed specifications. Protocol designers really should not have to care about this problem at all, but currently they have to: giving the adversary/environment the option to not respond immediately to modeling-related requests does not translate to any real attack scenario. This paper solves the non-responsiveness problem and its negative consequences completely, by avoiding this artificial modeling problem altogether. We propose the new concepts of responsive environments and adversaries. Such environments and adversaries must provide a valid response to modeling-related requests before any other protocol/functionality is activated. Hence, protocol designers do not have to worry any longer about artifacts resulting from such requests not being answered promptly. Our concepts apply to all existing models for universal composability, as exemplified for the UC, GNUC, and IITM models, with full definitions and proofs (simulation relations, transitivity, equivalence of various simulation notions, composition theorems) provided for the IITM model.
  BibTeX
  @techreport{CamenischEnderleinKrennKuestersRausch-IACR-2016-034, abstract = {In universal composability frameworks, adversaries (or environments) and protocols/ideal functionalities often have to exchange meta-information on the network interface, such as algorithms, keys, signatures, ciphertexts, signaling information, corruption-related messages. For these purely modeling-related messages, which do not reflect actual network communication, it would often be very reasonable and natural to expect that adversaries/environments provide the requested information immediately or give control back to the protocol/functionality immediately after having received some information. However, in none of the existing models for universal composability this is guaranteed. We call this the \emph{non-responsiveness problem}. As discussed in the paper, while formally non-responsiveness does not invalidate any of the universal composability models, it has many disadvantages, such as unnecessarily complex specifications and less expressivity. Also, this problem has often been ignored in the literature, leading to ill-defined and flawed specifications. Protocol designers really should not have to care about this problem at all, but currently they have to: giving the adversary/environment the option to not respond immediately to modeling-related requests does not translate to any real attack scenario. This paper solves the non-responsiveness problem and its negative consequences completely, by avoiding this artificial modeling problem altogether. We propose the new concepts of responsive environments and adversaries. Such environments and adversaries must provide a valid response to modeling-related requests before any other protocol/functionality is activated. Hence, protocol designers do not have to worry any longer about artifacts resulting from such requests not being answered promptly. Our concepts apply to all existing models for universal composability, as exemplified for the UC, GNUC, and IITM models, with full definitions and proofs (simulation relations, transitivity, equivalence of various simulation notions, composition theorems) provided for the IITM model.}, author = {Camenisch, Jan and Enderlein, Robert R. and Krenn, Stephan and K{\"u}sters, Ralf and Rausch, Daniel}, institution = {Cryptology ePrint Archive}, number = {2016/034}, title = {{Universal Composition with Responsive Environments}}, type = {Technical Report}, url = {https://publ.sec.uni-stuttgart.de/camenischenderleinkrennkuestersrausch-iacr-2016-034.pdf}, year = 2016 }
  Link
  https://publ.sec.uni-stuttgart.de/camenischenderleinkrennkuestersrausch-iacr-2016-034.pdf
2013
1. Max Tuengerthal, “Analysis of real-world security protocols in a universal composability framework,” University of Trier, 2013.
  - BibTeX
  - Link
  BibTeX
  @phdthesis{Tuengerthal-PhdThesis-2013, author = {Tuengerthal, Max}, school = {University of Trier}, title = {{Analysis of real-world security protocols in a universal composability framework}}, url = {https://publ.sec.uni-stuttgart.de/tuengerthal-phdthesis-2013.pdf}, year = 2013 }
  Link
  https://publ.sec.uni-stuttgart.de/tuengerthal-phdthesis-2013.pdf
2. Ralf Küsters and Max Tuengerthal, “The IITM Model: a Simple and Expressive Model for Universal Composability,” Cryptology ePrint Archive, 2013/025, 2013.
  Abstract
  The universal composability paradigm allows for the modular design and analysis of cryptographic protocols. It has been widely and successfully used in cryptography. However, devising a coherent yet simple and expressive model for universal composability is, as the history of such models shows, highly non-trivial. For example, several partly severe problems have been pointed out in the literature for the UC model. In this work, we propose a coherent model for universal composability, called the IITM model (``Inexhaustible Interactive Turing Machine''). A main feature of the model is that it is stated without a priori fixing irrelevant details, such as a specific way of addressing of machines by session and party identifiers, a specific modeling of corruption, or a specific protocol hierarchy. In addition, we employ a very general notion of runtime. All reasonable protocols and ideal functionalities should be expressible based on this notion in a direct and natural way, and without tweaks, such as (artificial) padding of messages or (artificially) adding extra messages. Not least because of these features, the model is simple and expressive. Also the general results that we prove, such as composition theorems, hold independently of how such details are fixed for concrete applications. Being inspired by other models for universal composability, in particular the UC model and because of the flexibility and expressivity of the IITM model, conceptually, results formulated in these models directly carry over to the IITM model.
  BibTeX
  @techreport{KuestersTuengerthal-eprint-025-2013, abstract = {The universal composability paradigm allows for the modular design and analysis of cryptographic protocols. It has been widely and successfully used in cryptography. However, devising a coherent yet simple and expressive model for universal composability is, as the history of such models shows, highly non-trivial. For example, several partly severe problems have been pointed out in the literature for the UC model. In this work, we propose a coherent model for universal composability, called the IITM model (``Inexhaustible Interactive Turing Machine''). A main feature of the model is that it is stated without a priori fixing irrelevant details, such as a specific way of addressing of machines by session and party identifiers, a specific modeling of corruption, or a specific protocol hierarchy. In addition, we employ a very general notion of runtime. All reasonable protocols and ideal functionalities should be expressible based on this notion in a direct and natural way, and without tweaks, such as (artificial) padding of messages or (artificially) adding extra messages. Not least because of these features, the model is simple and expressive. Also the general results that we prove, such as composition theorems, hold independently of how such details are fixed for concrete applications. Being inspired by other models for universal composability, in particular the UC model and because of the flexibility and expressivity of the IITM model, conceptually, results formulated in these models directly carry over to the IITM model.}, author = {K{\"u}sters, Ralf and Tuengerthal, Max}, institution = {Cryptology ePrint Archive}, note = {\url{http://eprint.iacr.org/2013/025/}}, number = {2013/025}, title = {{The IITM Model: a Simple and Expressive Model for Universal Composability}}, url = {https://publ.sec.uni-stuttgart.de/kuesterstuengerthal-eprint-025-2013.pdf}, year = 2013 }
  Link
  https://publ.sec.uni-stuttgart.de/kuesterstuengerthal-eprint-025-2013.pdf
2011
1. Ralf Küsters and Max Tuengerthal, “Composition Theorems Without Pre-Established Session Identifiers,” in Proceedings of the 18th ACM Conference on Computer and Communications Security (CCS 2011), Y. Chen, G. Danezis, and V. Shmatikov (Eds.), ACM Press, 2011, pp. 41–50.
  Abstract
  Canetti's universal composition theorem and the joint state composition theorems by Canetti and Rabin are useful and widely employed tools for the modular design and analysis of cryptographic protocols. However, these theorems assume that parties participating in a protocol session have pre-established a unique session ID (SID). While the use of such SIDs is a good design principle, existing protocols, in particular real-world security protocols, typically do not use pre-established SIDs, at least not explicitly and not in the particular way stipulated by the theorems. As a result, the composition theorems cannot be applied for analyzing such protocols in a modular and faithful way. In this paper, we therefore present universal and joint state composition theorems which do not assume pre-established SIDs. In our joint state composition theorem, the joint state is an ideal functionality which supports several cryptographic operations, including public-key encryption, (authenticated and unauthenticated) symmetric encryption, MACs, digital signatures, and key derivation. This functionality has recently been proposed by Küsters and Tuengerthal and has been shown to be realizable under standard cryptographic assumptions and for a reasonable class of environments. We demonstrate the usefulness of our composition theorems by several case studies on real-world security protocols, including IEEE 802.11i, SSL/TLS, SSH, IPsec, and EAP-PSK. While our applications focus on real-world security protocols, our theorems, models, and techniques should be useful beyond this domain.
  BibTeX
  @inproceedings{KuestersTuengerthal-CCS-2011, abstract = {Canetti's universal composition theorem and the joint state composition theorems by Canetti and Rabin are useful and widely employed tools for the modular design and analysis of cryptographic protocols. However, these theorems assume that parties participating in a protocol session have pre-established a unique session ID (SID). While the use of such SIDs is a good design principle, existing protocols, in particular real-world security protocols, typically do not use pre-established SIDs, at least not explicitly and not in the particular way stipulated by the theorems. As a result, the composition theorems cannot be applied for analyzing such protocols in a modular and faithful way. In this paper, we therefore present universal and joint state composition theorems which do not assume pre-established SIDs. In our joint state composition theorem, the joint state is an ideal functionality which supports several cryptographic operations, including public-key encryption, (authenticated and unauthenticated) symmetric encryption, MACs, digital signatures, and key derivation. This functionality has recently been proposed by K{\"u}sters and Tuengerthal and has been shown to be realizable under standard cryptographic assumptions and for a reasonable class of environments. We demonstrate the usefulness of our composition theorems by several case studies on real-world security protocols, including IEEE 802.11i, SSL/TLS, SSH, IPsec, and EAP-PSK. While our applications focus on real-world security protocols, our theorems, models, and techniques should be useful beyond this domain.}, author = {K{\"u}sters, Ralf and Tuengerthal, Max}, booktitle = {{Proceedings of the 18th ACM Conference on Computer and Communications Security (CCS 2011)}}, editor = {Chen, Y. and Danezis, G. and Shmatikov, V.}, pages = {41-50}, publisher = {ACM Press}, title = {{Composition Theorems Without Pre-Established Session Identifiers}}, url = {https://publ.sec.uni-stuttgart.de/kuesterstuengerthal-ccs-2011.pdf}, year = 2011 }
  Link
  https://publ.sec.uni-stuttgart.de/kuesterstuengerthal-ccs-2011.pdf
2. Ralf Küsters and Max Tuengerthal, “Composition Theorems Without Pre-Established Session Identifiers,” Cryptology ePrint Archive, 2011/406, 2011.
  Abstract
  Canetti's universal composition theorem and the joint state composition theorems by Canetti and Rabin are useful and widely employed tools for the modular design and analysis of cryptographic protocols. However, these theorems assume that parties participating in a protocol session have pre-established a unique session ID (SID). While the use of such SIDs is a good design principle, existing protocols, in particular real-world security protocols, typically do not use pre-established SIDs, at least not explicitly and not in the particular way stipulated by the theorems. As a result, the composition theorems cannot be applied for analyzing such protocols in a modular and faithful way. In this paper, we therefore present universal and joint state composition theorems which do not assume pre-established SIDs. In our joint state composition theorem, the joint state is an ideal functionality which supports several cryptographic operations, including public-key encryption, (authenticated and unauthenticated) symmetric encryption, MACs, digital signatures, and key derivation. This functionality has recently been proposed by Küsters and Tuengerthal and has been shown to be realizable under standard cryptographic assumptions and for a reasonable class of environments. We demonstrate the usefulness of our composition theorems by several case studies on real-world security protocols, including IEEE 802.11i, SSL/TLS, SSH, IPsec, and EAP-PSK. While our applications focus on real-world security protocols, our theorems, models, and techniques should be useful beyond this domain.
  BibTeX
  @techreport{KuestersTuengerthal-eprint-406-2011, abstract = {Canetti's universal composition theorem and the joint state composition theorems by Canetti and Rabin are useful and widely employed tools for the modular design and analysis of cryptographic protocols. However, these theorems assume that parties participating in a protocol session have pre-established a unique session ID (SID). While the use of such SIDs is a good design principle, existing protocols, in particular real-world security protocols, typically do not use pre-established SIDs, at least not explicitly and not in the particular way stipulated by the theorems. As a result, the composition theorems cannot be applied for analyzing such protocols in a modular and faithful way. In this paper, we therefore present universal and joint state composition theorems which do not assume pre-established SIDs. In our joint state composition theorem, the joint state is an ideal functionality which supports several cryptographic operations, including public-key encryption, (authenticated and unauthenticated) symmetric encryption, MACs, digital signatures, and key derivation. This functionality has recently been proposed by K{\"u}sters and Tuengerthal and has been shown to be realizable under standard cryptographic assumptions and for a reasonable class of environments. We demonstrate the usefulness of our composition theorems by several case studies on real-world security protocols, including IEEE 802.11i, SSL/TLS, SSH, IPsec, and EAP-PSK. While our applications focus on real-world security protocols, our theorems, models, and techniques should be useful beyond this domain.}, author = {K{\"u}sters, Ralf and Tuengerthal, Max}, institution = {Cryptology ePrint Archive}, note = {\url{http://eprint.iacr.org/2011/406/}}, number = {2011/406}, title = {{Composition Theorems Without Pre-Established Session Identifiers}}, url = {https://publ.sec.uni-stuttgart.de/kuesterstuengerthal-eprint-406-2011.pdf}, year = 2011 }
  Link
  https://publ.sec.uni-stuttgart.de/kuesterstuengerthal-eprint-406-2011.pdf
3. Ralf Küsters and Max Tuengerthal, “Ideal Key Derivation and Encryption in Simulation-Based Security,” in Topics in Cryptology - CT-RSA 2011, The Cryptographers’ Track at the RSA Conference 2011, Proceedings, A. Kiayias (Ed.), Springer, 2011, pp. 161–179.
  Abstract
  Many real-world protocols, such as SSL/TLS, SSH, IPsec, DNSSEC, IEEE 802.11i, and Kerberos, derive new keys from other keys. To be able to analyze such protocols in a composable way, in this paper we extend an ideal functionality for symmetric and public-key encryption proposed in previous work by a mechanism for key derivation. We also equip this functionality with message authentication codes (MACs), digital signatures, and ideal nonce generation. We show that the resulting ideal functionality can be realized based on standard cryptographic assumptions and constructions, hence, providing a solid foundation for faithful, composable cryptographic analysis of real-world security protocols. Based on this new functionality, we identify sufficient criteria for protocols to provide universally composable key exchange and secure channels. Since these criteria are based on the new ideal functionality, checking the criteria requires merely information-theoretic or even only syntactical arguments, rather than involved reduction arguments. As a case study, we use our method to analyze two central protocols of the IEEE 802.11i standard, namely the 4-Way Handshake Protocol and the CCM Protocol, proving composable security properties. As to the best of our knowledge, this constitutes the first rigorous cryptographic analysis of these protocols.
  BibTeX
  @inproceedings{KuestersTuengerthal-CTRSA-2011, abstract = {Many real-world protocols, such as SSL/TLS, SSH, IPsec, DNSSEC, IEEE 802.11i, and Kerberos, derive new keys from other keys. To be able to analyze such protocols in a composable way, in this paper we extend an ideal functionality for symmetric and public-key encryption proposed in previous work by a mechanism for key derivation. We also equip this functionality with message authentication codes (MACs), digital signatures, and ideal nonce generation. We show that the resulting ideal functionality can be realized based on standard cryptographic assumptions and constructions, hence, providing a solid foundation for faithful, composable cryptographic analysis of real-world security protocols. Based on this new functionality, we identify sufficient criteria for protocols to provide universally composable key exchange and secure channels. Since these criteria are based on the new ideal functionality, checking the criteria requires merely information-theoretic or even only syntactical arguments, rather than involved reduction arguments. As a case study, we use our method to analyze two central protocols of the IEEE 802.11i standard, namely the 4-Way Handshake Protocol and the CCM Protocol, proving composable security properties. As to the best of our knowledge, this constitutes the first rigorous cryptographic analysis of these protocols.}, author = {K{\"u}sters, Ralf and Tuengerthal, Max}, booktitle = {{Topics in Cryptology - CT-RSA 2011, The Cryptographers' Track at the RSA Conference 2011, Proceedings}}, editor = {Kiayias, Aggelos}, pages = {161-179}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {{Ideal Key Derivation and Encryption in Simulation-Based Security}}, url = {https://publ.sec.uni-stuttgart.de/kuesterstuengerthal-ctrsa-2011.pdf}, volume = 6558, year = 2011 }
  Link
  https://publ.sec.uni-stuttgart.de/kuesterstuengerthal-ctrsa-2011.pdf
2010
1. Ralf Küsters and Max Tuengerthal, “Ideal Key Derivation and Encryption in Simulation-based Security,” Cryptology ePrint Archive, 2010/295, 2010.
  Abstract
  Many real-world protocols, such as SSL/TLS, SSH, IPsec, IEEE 802.11i, DNSSEC, and Kerberos, derive new keys from other keys. To be able to analyze such protocols in a composable way, in this paper we extend our ideal functionality for symmetric and public-key encryption proposed in previous work by a mechanism for key derivation. We also equip our functionality with message authentication codes (MACs) and ideal nonce generation. We show that our ideal functionality can be realized based on standard cryptographic assumptions and constructions, hence, providing a solid foundation for faithful, composable cryptographic analysis of real-world security protocols. Based on our functionality, we identify sufficient criteria for protocols to provide universally composable key exchange and secure channels. Since these criteria are based on our ideal functionality, checking the criteria requires merely information-theoretic or even only syntactical arguments, rather than involved reduction arguments. As a case study, we use our method to analyze two central protocols of the IEEE 802.11i standard, namely the 4-Way Handshake Protocol and the CCM Protocol, proving composable security properties. As to the best of our knowledge, this constitutes the first rigorous cryptographic analysis of these protocols.
  BibTeX
  @techreport{KuestersTuengerthal-eprint-295-2010, abstract = {Many real-world protocols, such as SSL/TLS, SSH, IPsec, IEEE 802.11i, DNSSEC, and Kerberos, derive new keys from other keys. To be able to analyze such protocols in a composable way, in this paper we extend our ideal functionality for symmetric and public-key encryption proposed in previous work by a mechanism for key derivation. We also equip our functionality with message authentication codes (MACs) and ideal nonce generation. We show that our ideal functionality can be realized based on standard cryptographic assumptions and constructions, hence, providing a solid foundation for faithful, composable cryptographic analysis of real-world security protocols. Based on our functionality, we identify sufficient criteria for protocols to provide universally composable key exchange and secure channels. Since these criteria are based on our ideal functionality, checking the criteria requires merely information-theoretic or even only syntactical arguments, rather than involved reduction arguments. As a case study, we use our method to analyze two central protocols of the IEEE 802.11i standard, namely the 4-Way Handshake Protocol and the CCM Protocol, proving composable security properties. As to the best of our knowledge, this constitutes the first rigorous cryptographic analysis of these protocols.}, author = {K{\"u}sters, Ralf and Tuengerthal, Max}, institution = {Cryptology ePrint Archive}, note = {\url{http://eprint.iacr.org/2010/295/}}, number = {2010/295}, title = {{Ideal Key Derivation and Encryption in Simulation-based Security}}, url = {https://publ.sec.uni-stuttgart.de/kuesterstuengerthal-eprint-295-2010.pdf}, year = 2010 }
  Link
  https://publ.sec.uni-stuttgart.de/kuesterstuengerthal-eprint-295-2010.pdf
2009
1. Ralf Küsters and Max Tuengerthal, “Universally Composable Symmetric Encryption,” in Proceedings of the 22nd IEEE Computer Security Foundations Symposium (CSF 2009), IEEE Computer Society, 2009, pp. 293--307.
  Abstract
  For most basic cryptographic tasks, such as public-key encryption, digital signatures, authentication, key exchange, and many other more sophisticated tasks, ideal functionalities have been formulated in the simulation-based security approach, along with their realizations. Surprisingly, however, no such functionality exists for symmetric encryption, except for a more abstract Dolev-Yao style functionality. In this paper, we fill this gap. We propose two functionalities for symmetric encryption, an unauthenticated and an authenticated version, and show that they can be implemented based on standard cryptographic assumptions for symmetric encryption schemes, namely IND-CCA security and authenticated encryption, respectively, provided that the environment does not create key cycles or cause the so-called commitment problem. We also illustrate the usefulness of our functionalities in applications, both in simulation-based and game-based security settings.
  BibTeX
  @inproceedings{KuestersTuengerthal-CSF-2009, abstract = {For most basic cryptographic tasks, such as public-key encryption, digital signatures, authentication, key exchange, and many other more sophisticated tasks, ideal functionalities have been formulated in the simulation-based security approach, along with their realizations. Surprisingly, however, no such functionality exists for symmetric encryption, except for a more abstract Dolev-Yao style functionality. In this paper, we fill this gap. We propose two functionalities for symmetric encryption, an unauthenticated and an authenticated version, and show that they can be implemented based on standard cryptographic assumptions for symmetric encryption schemes, namely IND-CCA security and authenticated encryption, respectively, provided that the environment does not create key cycles or cause the so-called commitment problem. We also illustrate the usefulness of our functionalities in applications, both in simulation-based and game-based security settings.}, author = {K{\"u}sters, Ralf and Tuengerthal, Max}, booktitle = {{Proceedings of the 22nd IEEE Computer Security Foundations Symposium (CSF 2009)}}, pages = {293--307}, publisher = {IEEE Computer Society}, title = {{Universally Composable Symmetric Encryption}}, url = {https://publ.sec.uni-stuttgart.de/kuesterstuengerthal-csf-2009.pdf}, year = 2009 }
  Link
  https://publ.sec.uni-stuttgart.de/kuesterstuengerthal-csf-2009.pdf
2. Ralf Küsters and Max Tuengerthal, “Universally Composable Symmetric Encryption,” Cryptology ePrint Archive, 2009/055, 2009.
  Abstract
  For most basic cryptographic tasks, such as public key encryption, digital signatures, authentication, key exchange, and many other more sophisticated tasks, ideal functionalities have been formulated in the simulation-based security approach, along with their realizations. Surprisingly, however, no such functionality exists for symmetric encryption, except for a more abstract Dolev-Yao style functionality. In this paper, we fill this gap. We propose two functionalities for symmetric encryption, an unauthenticated and an authenticated version, and show that they can be implemented based on standard cryptographic assumptions for symmetric encryption schemes, namely IND-CCA security and authenticated encryption, respectively. We also illustrate the usefulness of our functionalities in applications, both in simulation-based and game-based security settings.
  BibTeX
  @techreport{KuestersTuengerthal-eprint-055-2009, abstract = {For most basic cryptographic tasks, such as public key encryption, digital signatures, authentication, key exchange, and many other more sophisticated tasks, ideal functionalities have been formulated in the simulation-based security approach, along with their realizations. Surprisingly, however, no such functionality exists for symmetric encryption, except for a more abstract Dolev-Yao style functionality. In this paper, we fill this gap. We propose two functionalities for symmetric encryption, an unauthenticated and an authenticated version, and show that they can be implemented based on standard cryptographic assumptions for symmetric encryption schemes, namely IND-CCA security and authenticated encryption, respectively. We also illustrate the usefulness of our functionalities in applications, both in simulation-based and game-based security settings.}, author = {K{\"u}sters, Ralf and Tuengerthal, Max}, institution = {Cryptology ePrint Archive}, note = {\url{http://eprint.iacr.org/2009/055/}}, number = {2009/055}, title = {{Universally Composable Symmetric Encryption}}, url = {https://publ.sec.uni-stuttgart.de/kuesterstuengerthal-eprint-055-2009.pdf}, year = 2009 }
  Link
  https://publ.sec.uni-stuttgart.de/kuesterstuengerthal-eprint-055-2009.pdf
2008
1. Ralf Küsters and Max Tuengerthal, “Joint State Theorems for Public-Key Encryption and Digital Signature Functionalities with Local Computation,” in Proceedings of the 21st IEEE Computer Security Foundations Symposium (CSF 2008), IEEE Computer Society, 2008, pp. 270–284.
  Abstract
  Composition theorems in simulation-based approaches allow to build complex protocols from sub-protocols in a modular way. However, as first pointed out and studied by Canetti and Rabin, this modular approach often leads to impractical implementations. For example, when using a functionality for digital signatures within a more complex protocol, parties have to generate new verification and signing keys for every session of the protocol. This motivates to generalize composition theorems to so-called joint state theorems, where different copies of a functionality may share some state, e.g., the same verification and signing keys. In this paper, we present a joint state theorem which is more general than the original theorem of Canetti and Rabin, for which several problems and limitations are pointed out. We apply our theorem to obtain joint state realizations for three functionalities: public-key encryption, replayable public-key encryption, and digital signatures. Unlike most other formulations, our functionalities model that ciphertexts and signatures are computed locally, rather than being provided by the adversary. To obtain the joint state realizations, the functionalities have to be designed carefully. Other formulations are shown to be unsuitable. Our work is based on a recently proposed, rigorous model for simulation-based security by Küsters, called the IITM model. Our definitions and results demonstrate the expressivity and simplicity of this model. For example, unlike Canetti's UC model, in the IITM model no explicit joint state operator needs to be defined and the joint state theorem follows immediately from the composition theorem in the IITM model.
  BibTeX
  @inproceedings{KuestersTuengerthal-CSF-2008, abstract = {Composition theorems in simulation-based approaches allow to build complex protocols from sub-protocols in a modular way. However, as first pointed out and studied by Canetti and Rabin, this modular approach often leads to impractical implementations. For example, when using a functionality for digital signatures within a more complex protocol, parties have to generate new verification and signing keys for every session of the protocol. This motivates to generalize composition theorems to so-called joint state theorems, where different copies of a functionality may share some state, e.g., the same verification and signing keys. In this paper, we present a joint state theorem which is more general than the original theorem of Canetti and Rabin, for which several problems and limitations are pointed out. We apply our theorem to obtain joint state realizations for three functionalities: public-key encryption, replayable public-key encryption, and digital signatures. Unlike most other formulations, our functionalities model that ciphertexts and signatures are computed locally, rather than being provided by the adversary. To obtain the joint state realizations, the functionalities have to be designed carefully. Other formulations are shown to be unsuitable. Our work is based on a recently proposed, rigorous model for simulation-based security by K{\"u}sters, called the IITM model. Our definitions and results demonstrate the expressivity and simplicity of this model. For example, unlike Canetti's UC model, in the IITM model no explicit joint state operator needs to be defined and the joint state theorem follows immediately from the composition theorem in the IITM model.}, author = {K{\"u}sters, Ralf and Tuengerthal, Max}, booktitle = {{Proceedings of the 21st IEEE Computer Security Foundations Symposium (CSF 2008)}}, pages = {270-284}, publisher = {IEEE Computer Society}, title = {{Joint State Theorems for Public-Key Encryption and Digital Signature Functionalities with Local Computation}}, url = {https://publ.sec.uni-stuttgart.de/kuesterstuengerthal-csf-2008.pdf}, year = 2008 }
  Link
  https://publ.sec.uni-stuttgart.de/kuesterstuengerthal-csf-2008.pdf
2. Ralf Küsters and Max Tuengerthal, “Joint State Theorems for Public-Key Encryption and Digital Signature Functionalities with Local Computation,” Cryptology ePrint Archive, 2008/006, 2008.
  Abstract
  Composition theorems in simulation-based approaches allow to build complex protocols from sub-protocols in a modular way. However, as first pointed out and studied by Canetti and Rabin, this modular approach often leads to impractical implementations. For example, when using a functionality for digital signatures within a more complex protocol, parties have to generate new verification and signing keys for every session of the protocol. This motivates to generalize composition theorems to so-called joint state theorems, where different copies of a functionality may share some state, e.g., the same verification and signing keys. In this paper, we present a joint state theorem which is more general than the original theorem of Canetti and Rabin, for which several problems and limitations are pointed out. We apply our theorem to obtain joint state realizations for three functionalities: public-key encryption, replayable public-key encryption, and digital signatures. Unlike most other formulations, our functionalities model that ciphertexts and signatures are computed locally, rather than being provided by the adversary. To obtain the joint state realizations, the functionalities have to be designed carefully. Other formulations are shown to be unsuitable. Our work is based on a recently proposed, rigorous model for simulation-based security by Küsters, called the IITM model. Our definitions and results demonstrate the expressivity and simplicity of this model. For example, unlike Canetti's UC model, in the IITM model no explicit joint state operator needs to be defined and the joint state theorem follows immediately from the composition theorem in the IITM model.
  BibTeX
  @techreport{KuestersTuengerthal-eprint-006-2008, abstract = {Composition theorems in simulation-based approaches allow to build complex protocols from sub-protocols in a modular way. However, as first pointed out and studied by Canetti and Rabin, this modular approach often leads to impractical implementations. For example, when using a functionality for digital signatures within a more complex protocol, parties have to generate new verification and signing keys for every session of the protocol. This motivates to generalize composition theorems to so-called joint state theorems, where different copies of a functionality may share some state, e.g., the same verification and signing keys. In this paper, we present a joint state theorem which is more general than the original theorem of Canetti and Rabin, for which several problems and limitations are pointed out. We apply our theorem to obtain joint state realizations for three functionalities: public-key encryption, replayable public-key encryption, and digital signatures. Unlike most other formulations, our functionalities model that ciphertexts and signatures are computed locally, rather than being provided by the adversary. To obtain the joint state realizations, the functionalities have to be designed carefully. Other formulations are shown to be unsuitable. Our work is based on a recently proposed, rigorous model for simulation-based security by K{\"u}sters, called the IITM model. Our definitions and results demonstrate the expressivity and simplicity of this model. For example, unlike Canetti's UC model, in the IITM model no explicit joint state operator needs to be defined and the joint state theorem follows immediately from the composition theorem in the IITM model.}, author = {K{\"u}sters, Ralf and Tuengerthal, Max}, institution = {Cryptology ePrint Archive}, month = {4}, note = {\url{http://eprint.iacr.org/2008/006/}}, number = {2008/006}, title = {{Joint State Theorems for Public-Key Encryption and Digital Signature Functionalities with Local Computation}}, url = {https://publ.sec.uni-stuttgart.de/kuesterstuengerthal-eprint-006-2008.pdf}, year = 2008 }
  Link
  https://publ.sec.uni-stuttgart.de/kuesterstuengerthal-eprint-006-2008.pdf
2006
1. Ralf Küsters, “Simulation-Based Security with Inexhaustible Interactive Turing Machines,” in Proceedings of the 19th IEEE Computer Security Foundations Workshop (CSFW-19 2006), IEEE Computer Society, 2006, pp. 309--320.
  Abstract
  Recently, there has been much interest in extending models for simulation-based security in such a way that the runtime of protocols may depend on the length of their input. Finding such extensions has turned out to be a non-trivial task. In this work, we propose a simple, yet expressive general computational model for systems of Interactive Turing Machines (ITMs) where the runtime of the ITMs may be polynomial per activation and may depend on the length of the input received. One distinguishing feature of our model is that the systems of ITMs that we consider involve a generic mechanism for addressing dynamically generated copies of ITMs. We study properties of such systems and, in particular, show that systems satisfying a certain acyclicity condition run in polynomial time. Based on our general computational model, we state different notions of simulation-based security in a uniform and concise way, study their relationships, and prove a general composition theorem for composing a polynomial number of copies of protocols, where the polynomial is determined by the environment. The simplicity of our model is demonstrated by the fact that many of our results can be proved by mere equational reasoning based on a few equational principles on systems.
  BibTeX
  @inproceedings{Kuesters-CSFW-2006, abstract = {Recently, there has been much interest in extending models for simulation-based security in such a way that the runtime of protocols may depend on the length of their input. Finding such extensions has turned out to be a non-trivial task. In this work, we propose a simple, yet expressive general computational model for systems of Interactive Turing Machines (ITMs) where the runtime of the ITMs may be polynomial per activation and may depend on the length of the input received. One distinguishing feature of our model is that the systems of ITMs that we consider involve a generic mechanism for addressing dynamically generated copies of ITMs. We study properties of such systems and, in particular, show that systems satisfying a certain acyclicity condition run in polynomial time. Based on our general computational model, we state different notions of simulation-based security in a uniform and concise way, study their relationships, and prove a general composition theorem for composing a polynomial number of copies of protocols, where the polynomial is determined by the environment. The simplicity of our model is demonstrated by the fact that many of our results can be proved by mere equational reasoning based on a few equational principles on systems.}, author = {K{\"u}sters, Ralf}, booktitle = {{Proceedings of the 19th IEEE Computer Security Foundations Workshop (CSFW-19 2006)}}, pages = {309--320}, publisher = {IEEE Computer Society}, title = {{Simulation-Based Security with Inexhaustible Interactive Turing Machines}}, url = {https://publ.sec.uni-stuttgart.de/kuesters-csfw-2006.pdf}, year = 2006 }
  Link
  https://publ.sec.uni-stuttgart.de/kuesters-csfw-2006.pdf
2. Ralf Küsters, “Simulation-Based Security with Inexhaustible Interactive Turing Machines,” Cryptology ePrint Archive, 2006/151, 2006.
  Abstract
  Recently, there has been much interest in extending models for simulation-based security in such a way that the runtime of protocols may depend on the length of their input. Finding such extensions has turned out to be a non-trivial task. In this work, we propose a simple, yet expressive general computational model for systems of Interactive Turing Machines (ITMs) where the runtime of the ITMs may be polynomial per activation and may depend on the length of the input received. One distinguishing feature of our model is that the systems of ITMs that we consider involve a generic mechanism for addressing dynamically generated copies of ITMs. We study properties of such systems and, in particular, show that systems satisfying a certain acyclicity condition run in polynomial time. Based on our general computational model, we state different notions of simulation-based security in a uniform and concise way, study their relationships, and prove a general composition theorem for composing a polynomial number of copies of protocols, where the polynomial is determined by the environment. The simplicity of our model is demonstrated by the fact that many of our results can be proved by mere equational reasoning based on a few equational principles on systems.
  BibTeX
  @techreport{Kuesters-eprint-151-2006, abstract = {Recently, there has been much interest in extending models for simulation-based security in such a way that the runtime of protocols may depend on the length of their input. Finding such extensions has turned out to be a non-trivial task. In this work, we propose a simple, yet expressive general computational model for systems of Interactive Turing Machines (ITMs) where the runtime of the ITMs may be polynomial per activation and may depend on the length of the input received. One distinguishing feature of our model is that the systems of ITMs that we consider involve a generic mechanism for addressing dynamically generated copies of ITMs. We study properties of such systems and, in particular, show that systems satisfying a certain acyclicity condition run in polynomial time. Based on our general computational model, we state different notions of simulation-based security in a uniform and concise way, study their relationships, and prove a general composition theorem for composing a polynomial number of copies of protocols, where the polynomial is determined by the environment. The simplicity of our model is demonstrated by the fact that many of our results can be proved by mere equational reasoning based on a few equational principles on systems.}, author = {K{\"u}sters, Ralf}, institution = {Cryptology ePrint Archive}, note = {\url{http://eprint.iacr.org/2006/151/}}, number = {2006/151}, title = {{Simulation-Based Security with Inexhaustible Interactive Turing Machines}}, url = {https://publ.sec.uni-stuttgart.de/kuesters-eprint-151-2006.pdf}, year = 2006 }
  Link
  https://publ.sec.uni-stuttgart.de/kuesters-eprint-151-2006.pdf

Acknowledgements

This work has been supported by Deutsche Forschungsgemeinschaft (DFG).

The iUC Framework

About the iUC Framework

Features of the iUC Framework

History

Literature and Publications

2023

Abstract

BibTeX

Link

DOI

2022

Abstract

BibTeX

Link

Abstract

BibTeX

Link

DOI

Abstract

BibTeX

Link

2021

Abstract

BibTeX

Link

DOI

Abstract

BibTeX

Link

2020

Abstract

BibTeX

Abstract

BibTeX

Link

DOI

Abstract

BibTeX

Link

DOI

2019

Abstract

BibTeX

Link

DOI

Abstract

BibTeX

2018

Abstract

BibTeX

Link

2017

Abstract

BibTeX

Link

DOI

Abstract

BibTeX

Link

2016

Abstract

BibTeX

Link

DOI

Abstract

BibTeX

Link

2013

BibTeX

Link

Abstract

BibTeX

Link

2011

Abstract

BibTeX

Link

Abstract

BibTeX

Link