[Busec] Broken Protocols
rskowyra at bu.edu
Tue Oct 18 10:47:51 EDT 2011
Azer, Andrei and I are beginning to investigate the applicability of formal
methods to "model-extension". Given a simple formal model of a system or
protocol and a set of correctness/security constraints, we would like to
automatically extend the state space to cover certain high-level concepts
such as time, homogeneity, etc. and check if the (possibly extended)
constraints still hold. We are currently trying to identify concepts worth
investigating and making expressible in a formal language.
To this end, we'd like to know about any protocols or systems you're aware
of which have had breaks found in them despite being either provably secure
for a reduced threat model or in widespread use (e.g. Kerberos 4 and the
breaks resulting from an assumption of nonmalleability). While we're most
interested in security-related breaks, any domain is potentially of
If you know of anything, please send us a pointer to the relevant paper and
a brief description of the protocol and break.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Busec