345 reputation
bio website
visits member for 1 year, 3 months
seen Dec 6 '13 at 21:40

comment Automated security protocol verification tool for eCK model
Most security models for key exchange protocols, including eCK, are descendants of [Bellare Rogaway 1993][1]. The differences among these variants are subtle and AFAIK there is no agreement on which one you should use. This is still a topic of active research so don't expect a definite answer here. [1]: cseweb.ucsd.edu/~mihir/papers/eakd.pdf
comment Authenticated DH, what protocols are secure?
There has been a lot of debate about the exact relation/improvements of HMQV over MQV, but IMO these discussions do not have significant practical impact. Especially since most standards require that the group element checks are included. This however reduces some of its claimed efficiency gains. These debates mostly concern the provable security claims and/or the precision of the security models.
comment Formal definition of (perfect) forward security/secrecy
If the protocol stores the session key for law enforcement (or, say, encrypts it with the public key of law enforcement agencies and includes this in a transmission) then of course perfect forward secrecy is not satisfied wrt those agencies.
comment Formal definition of (perfect) forward security/secrecy
Possibly they mean shielding the communications from adversaries on the network; but of course on their servers your communication is in plaintext. Legislations for storing data/wiretapping are a very different threat model. I would guess that their statement simply means that they're using SSL/TLS in a Diffie-Hellman mode.
comment Formal definition of (perfect) forward security/secrecy
I agree, and I doubt that the formal definitions you will find will have any relation to the claims made by such companies.