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-Con Oct 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.
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):
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.