Computational Soundness for Standard Assumptions of Formal Cryptography
| Title | Computational Soundness for Standard Assumptions of Formal Cryptography |
| Publication Type | Thesis |
| Year of Publication | 2004 |
| Authors | Herzog, Jonathan |
| Advisor | Rivest, Ron, Silvio Micali, and Nancy Lynch |
| Academic Department | Department of Electrical Engineering and Computer Science |
| Degree | Doctor of Philosophy |
| Date Published | May |
| University | Massachusetts Institute of Technology |
| City | Cambridge, MA |
| Thesis Type | phd |
| Abstract | The Dolev–Yao model is a useful and well-known framework in which to analyze security protocols.
However, it models the messages of the protocol at a very high level and makes extremely strong
assumptions about the power of the adversary. The computational model of cryptography, on the
other hand, takes a much lower-level view of messages and uses much weaker assumptions.
Despite the large differences between these two models, we have been able to show that there
exists a relationship between them. Previous results of ours demonstrate that certain kinds of computational cryptography can result in an equivalence of sorts between the formal and computational
adversary. Specifically:
- We gave an interpretation to the messages of the Dolev–Yao model in terms of computational cryptography,
- We defined a computational security condition, called weak Dolev-Yao non-malleability, that
translates the main assumptions of the Dolev-Yao model into the computational setting, and
- We demonstrated that this condition is satisfied by a standard definition of computational
encryption security called plaintext awareness.
In this work, we consider this result and strengthen it in four ways:
- Firstly, we propose a stronger definition of Dolev-Yao non-malleability which ensures security
against a more adaptive adversary.
- Secondly, the definition of plaintext awareness is considered suspect because it relies on a
trusted third party called the random oracle. Thus, we show that our new notion of Dolev-
Yao non-malleability is satisfied by a weaker and less troublesome definition for computational
encryption called chosen-ciphertext security.
- Thirdly, we propose a new definition of plaintext-awareness that does not use random oracles,
and an implementation. This implementation is conceptually simple, and relies only on general
assumptions. Specifically, it can be thought of as a ‘self-referential’ variation on a well-known
encryption scheme.
- Lastly, we show how the computational soundness of the Dolev-Yao model can be maintained
even as it is extended to include new operators. In particular, we show how the Diffie-Hellman
key-agreement scheme and the computational Diffie-Hellman assumption can be added to the
Dolev-Yao model in a computationally sound way.
|
| URL | http://files.jonathanherzog.com/herzog-phd.pdf |
