[Busec] Broken Protocols

Richard Skowyra rskowyra at bu.edu
Tue Oct 18 10:47:51 EDT 2011

Hello everyone,

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.

Thank you,

Rick Skowyra
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://cs-mailman.bu.edu/pipermail/busec/attachments/20111018/19897a36/attachment.html 

More information about the Busec mailing list