<meta http-equiv="content-type" content="text/html; charset=utf-8"><span class="Apple-style-span" style="border-collapse: collapse; font-family: arial, sans-serif; font-size: 13px; ">Hello everyone,<div><br></div><div>Azer, Andrei and I are beginning to investigate the applicability of formal methods to &quot;model-extension&quot;. 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. </div>
<div><br></div><div>To this end, we&#39;d like to know about any protocols or systems you&#39;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&#39;re most interested in security-related breaks, any domain is potentially of interest.</div>
<div><br></div><div> If you know of anything, please send us a pointer to the relevant paper and a brief description of the protocol and break.</div><div><br></div><div>Thank you,</div><div><br></div><div>Rick Skowyra</div>
</span>