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