# how to mathematically prove a key exchange algorithm [closed]

I want to know the basic methodology that can be used to prove that a key exchange algorithm is secure. I am not asking about any specific algorithm. I want to know what should be proven and how to prove in an abstract way.

-

## closed as too broad by D.W., Ricky Demer, Gilles, e-sushi, B-ConOct 1 '13 at 20:51

There are either too many possible answers, or good answers would be too long for this format. Please add details to narrow the answer set or to isolate an issue that can be answered in a few paragraphs. If this question can be reworded to fit the rules in the help center, please edit the question.

Welcome to Crypto.SE! Unfortunately, this question is probably too broad and open-ended to be a good fit for this site. What have you studied so far? What's the real problem you have in front of you? What's the context and motivation for your problem? Providing a more detailed and narrowly focused question makes it more likely that it will be possible to provide a useful answer, within the constraints of a StackExchange site. –  D.W. Sep 30 '13 at 6:32

## 1 Answer

I guess the best place to begin is with the paper that started it all: Entity authentication and key distribution, by Bellare and Rogaway. In a nutshell, they define a protocol to be a secure mutual authenticated key exchange if it fulfills the following four criteria (I will explain the term "matching conversation" below):

1. Matching conversations $\Rightarrow$ both parties accepts, meaning that both parties believe they are participating in an authentic session. Note that this is criteria is basically a simple "sanity check" of the protocol: if there are no adversaries the protocol should "work".

2. If a party accepts $\Rightarrow$ there should exist some matching conversation out there. This is the first "real" security requirement. What this basically says is that a protocol provides secure mutual authentication if all that an adversary is able to do is act like a wire between the protocol participants. An adversary which faithfully relays all protocol messages between the parties is called a benign adversary.

3. Benign adversary $\Rightarrow$ both parties obtain the same key and in accordance with the distribution chosen for the key space. Again, this is basically a sanity check of the protocol.

4. Session key is protected. This means that if the parties managed to agree on a shared key, the attacker should not be able to learn anything about it. This is formalized by a game between a challenger (one of the parties) and the adversary, where the challenger gives the adversary either the real key or a random string (from the same distribution). If the adversary is not able to distinguish these two settings, we say that the session key is protected.

Thus if you are to prove a key exchange algorithm secure you need to show that it provides the four points above. Usually you do this using a reduction to an underlying assumption, like the existence of secure encryption functions and MAC's. The term matching conversation means that if party A sent out ($\alpha$) and received ($\beta$) the following messages: $(\alpha_1, \beta_1), (\alpha_2, \beta_2) ... (\alpha_n, \beta_n)$ (in that order), then B have a matching conversation if he received ($\alpha$) and sent out ($\beta$): $(\alpha_1, \beta_1), (\alpha_2, \beta_2) ... (\alpha_n, \beta_n)$ (in that order). There are some more technicalities to this definition dealing with who sent the first message and so on, but the gist of it is that A and B have matching conversations if they received what the other party sent out (and in the right order).

Note that this is only one approach to this subject and is by no means the right way of defining a secure key exchange. Another common approach e.g. deals with a simulation framework of interactive turing machines, and proves that a protocol simulates an ideal functionality defined in this model. These are in some sense much more elaborate and complex than the simple approach given by Bellare and Rogaway, but are also much more general.

-
Thank you very much. This is exactly what I looked for. –  deltaaruna Sep 30 '13 at 10:01