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.
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
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
-
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
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
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
