CODEWITHSUNDEEP
verificationformal-methodsproverif
August Jelemson
August Jelemson

Reputation: 1218

What does ==> mean in proverif?

I found the following line of code in the proverif manual.

 ⋮ 
query event(evCocks) ==> event(evRSA).
 ⋮

What does ==> mean?

EDIT: I have answered my own question below.

Upvotes: 1

Views: 267

Answers (1)

August Jelemson
August Jelemson

Reputation: 1218

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?

In the proverif manual it is stated that

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

link to proverif manual

Upvotes: 1

Related Questions