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\}$$

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.