[isabelle] Re: Some question about Auth library



Your message puzzles me. Nearly all of the protocols do include Oops, including the two that you mention. Examples are KerberosIV, Kerberos_BAN, NS_Shared, OtwayRees, OtwayRees_AN, OtwayRees_Bad, Recur, TLS, Yahalom, Yahalom2.

Yahalom_Bad omits Oops precisely to demonstrate that a flawed protocol can be "verified" if the model is too abstract. Other protocols, such as Needham-Schroeder, don't need it because they don't use session keys. The SET protocol models omit Oops because they are very complicated already.

Larry Paulson


On 8 Sep 2005, at 08:51, yongjian Li wrote:

In these papers: Key compromise assuption is held for session keys, and Ooops rule are correspondingly introduced for this principle in trace's inductive definition.

In the auth library, the proof script of "yahalm2" and OtwayRees_Bad has this oops rule, but in
yahalm and OtwayRees, there is no such rule.

Do the two former theory think the key compromise assumption holds, while the latter don't?






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.