[cryptography] Validating cryptographic protocols
I've recently been asked to comment on a key exchange protocol which uses symmetric cryptography and a mutually trusted third party. The obvious recommendation is to copy the Kerberos protocol (perhaps with updated cryptographic primitives), but let's assume that's not feasible for some reason. I'm wondering what's the state of the art here, and if there are any formal methods for deciding if a particular protocol has certain security properties. I know that there have been some advances in this area, but it's sort of difficult to put together the current overall picture. (This assumes that the primitives are themselves secure, and that leakage from improper implementation of the primitives can be contained in some way, e.g. no padding oracles.) ___ cryptography mailing list cryptography@randombit.net http://lists.randombit.net/mailman/listinfo/cryptography
Re: [cryptography] Validating cryptographic protocols
On Wed, May 1, 2013 at 6:50 PM, Florian Weimer f...@deneb.enyo.de wrote: I'm wondering what's the state of the art here, and if there are any formal methods for deciding if a particular protocol has certain security properties. I know that there have been some advances in this area, but it's sort of difficult to put together the current overall picture. There is no such thing as single winner among security protocols symbolic verifiers. As a matter of fact, not every tool provides support for the same set of security properties or adversary models. The state of the art is represented by: - ProVerif (represent protocols by Horn clauses and analyzes them doing over-approximation) http://prosecco.gforge.inria.fr/personal/bblanche/proverif/ - Scyther (symbolic backwards search) http://people.inf.ethz.ch/cremersc/scyther/index.html - Avispa (here protocols are modeled in a common language called HLPSL and fed into four different back-end tools, each with unique features...) http://www.avispa-project.org/ - Casper/FDR (translate protocol models in process algebra CSP and uses FDR model checker to provide an analysis of the translated protocols) http://www.cs.ox.ac.uk/gavin.lowe/Security/Casper/installation.html So far, I've been having positive experiences with Scyther and Avispa. ProVerif and Scyther are generally the fastest (see Comparing State Spaces in Automatic Security Protocol Analysis by Cremers C. et al). Cheers, alfonso ___ cryptography mailing list cryptography@randombit.net http://lists.randombit.net/mailman/listinfo/cryptography
Re: [cryptography] Validating cryptographic protocols
The state of the art is represented by: - ProVerif (represent protocols by Horn clauses and analyzes them doing over-approximation) http://prosecco.gforge.inria.fr/personal/bblanche/proverif/ - Scyther (symbolic backwards search) http://people.inf.ethz.ch/cremersc/scyther/index.html - Avispa (here protocols are modeled in a common language called HLPSL and fed into four different back-end tools, each with unique features...) http://www.avispa-project.org/ - Casper/FDR (translate protocol models in process algebra CSP and uses FDR model checker to provide an analysis of the translated protocols) http://www.cs.ox.ac.uk/gavin.lowe/Security/Casper/installation.html So far, I've been having positive experiences with Scyther and Avispa. I second that. In particular, I have found Avispa to be very useful. There used to be one difference between Scyther and Avispa in terms of the authentication definition, with Scyther's using a stronger one. But I think Cas mentioned he's implemented Avispa's definition now, too. Both are very good model checkers. Avispa might give you some more difficulty, I think, because it's only available as a binary for certain platforms (ia32 linux, I think). Ralph ___ cryptography mailing list cryptography@randombit.net http://lists.randombit.net/mailman/listinfo/cryptography
Re: [cryptography] Validating cryptographic protocols
On Wed, May 1, 2013 at 9:50 AM, Florian Weimer f...@deneb.enyo.de wrote: I've recently been asked to comment on a key exchange protocol which uses symmetric cryptography and a mutually trusted third party. The obvious recommendation is to copy the Kerberos protocol (perhaps with updated cryptographic primitives), but let's assume that's not feasible for some reason. Kerberos has a few flaws, mostly with trivial effects or which have been fixed subsequently. Most, if not all of these flaws are about unauthenticated plaintext: the Ticket in the KDC-REP, for example, but also PA-DATA in KDC-REP, and KRB-ERROR in cases where the error can be authenticated because a session key could be established. FAST (RFC6113) fixes these issues, except for KRB-ERROR in AP exchanges, but it's not as elegant as it could have been if Kerberos had not had these problems from the word go. Another problem is that all of the cross-realm work should preferably be done by the client principal's KDC as an option to keep clients simple. (This at some costs in policy that can be expressed, or how to express and deploy it.) Nico -- ___ cryptography mailing list cryptography@randombit.net http://lists.randombit.net/mailman/listinfo/cryptography
Re: [cryptography] Validating cryptographic protocols
On 5/1/2013 10:50 AM, Florian Weimer wrote: (This assumes that the primitives are themselves secure, and that leakage from improper implementation of the primitives can be contained in some way, e.g. no padding oracles.) It is worth noting that the Kerberos crypto primitives were extracted from the Kerberos protocol in RFC 3961 with the hope that they would be reused in additional protocols. The belief that that there are fewer cryptographers in the world than network security protocol developers and the cryptographer's efforts should not be re-invented for each network security protocol. https://www.ietf.org/rfc/rfc3961.txt Additional encryption and checksum specifications have and can be published in the framework of RFC 3961 without altering 3961. Jeffrey Altman smime.p7s Description: S/MIME Cryptographic Signature ___ cryptography mailing list cryptography@randombit.net http://lists.randombit.net/mailman/listinfo/cryptography
Re: [cryptography] Validating cryptographic protocols
To complete the thought I meant to... don't just copy Kerberos. Copy the fixes, and fold them in better. Regarding crypto primitives, as Jeff Altman points out, the Kerberos ones have been separated out from Kerberos. See RFC 3961 and 3962. Note that for AES in particular Kerberos relies on ciphertext stealing mode, which is actually quite a pain to work with if you have hardware with high operation overhead. Counter-based modes could work equally way, but much care is needed to keep the likelihood of key+counter reuse near or at zero. If you're building a GSS-API mechanism at all just steal the Kerberos mechanism's per-token message protocol (as several mechanisms have done). Nico -- ___ cryptography mailing list cryptography@randombit.net http://lists.randombit.net/mailman/listinfo/cryptography
