Modular proofs for key exchange: rigorous optimizations in the Canetti–Krawczyk model

Various optimizations in the Canetti–Krawczyk model for secure protocol design are proven to preserve security. In particular it is shown that multiple authenticators may be safely used together; that certain message components generated by authenticators may be reordered (to be sent at a different time) or replaced with other values with certain precautions; and that protocols may be defined in the ideal world with session identifiers constructed during protocol runs. Consequently protocol designers now have a set of clear rules to optimize and customize their designs without fear of breaking the security proof. In order to obtain the required proofs, we find it necessary to slightly revise the authenticated links part of the Canetti–Krawczyk model. Research funded by Australian Research Council through Discovery Project DP0345775