问题描述
我在证明手册中找到了以下代码行。
⋮
query event(evCocks) ==> event(evRSA).
⋮
==>
是什么意思?
解决方法
Correspondence properties:
P and Q are predicates.
P(x) ==> Q(x,y)
for all x where P(x) is true,then there exists a y
such that Q(x,y) is true
query event(e1) ==> event(e2).
the query above can be translated to the following question:
Is it true that;
for all executions of event e1 (in the protocol) it is true that
e2 has executed?
在证明手册中说明
query event(evCocks) ==> event(evRSA)
is true if and only if,for all executions of the protocol,if the event
evCocks has been executed,then
event evRSA has also [already] been executed