On Session Key Construction in Provably-Secure Key Establishment Protocols