next up previous
Next: Dealing with failed proofs Up: Incorrect Implementation Previous: PVS analysis

Corrected Implementation

The corrected implementation proposed in [RS97] is a very simple extension of the incorrect version. They suggest that the server return certificates of the form

K_{ab} \bigoplus \mathsf{Hash}_{Kb}\{Nb, A\}, K_{bc} \bigoplus \mathsf{Hash}_{Kb}\{Nb, C\}\end{displaymath}

which does indeed provide secure session keys between pairs of honest agents. This has now been proven in PVS for the most general case, when A , B and the server are honest.