如何解决==> 在证明中是什么意思?
我在证明手册中找到了以下代码行。
⋮
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
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。