[isabelle] Some question about Auth library
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and