[isabelle] Some question about Auth library



Dear sir:
  recently, I check some proof script about auth library.
  My main question is about recency or key compromise.
  I read two  paper:  "Relations between secrets: two formal analyses of the Yahalom protocol"
                                              The inductive approach to verifying cryptographic protocols

  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?

regards






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