search

tamarin-prover / manual

Tamarin prover manual: source files
https://tamarin-prover.github.io/manual
24 stars 39 forks source link

Fixed secrecy_asym_enc example in section 6 #46

Closed lordqwerty closed 6 years ago

lordqwerty commented 6 years ago

See: https://tamarin-prover.github.io/manual/book/006_property-specification.html#secrecy

From working the example secrecy_asym_enc in this section of chapter 6 I believe it to be wrong and it contains numerous errors resulting in an attack being found, which I believe to be incorrect. it shows the following trace: broken

When fixed it shows the obvious and correct attack: fixed

See the PR for the minimal changes and from reading the manual this has no impact on the text.

rsasse commented 6 years ago

After a quick look, I believe you are absolutely right with both the fix to the informal spec:

  1. A -> B: {A,na}sk(A) to
  2. A -> B: {A,na}pk(B) as this example is supposed to do asymmetric encryption, using the recipient's public key. All the follow-up fixed of the theory look good to me as well. And the attack graphs you present are convincing.

I want to take a more careful look again before accepting the PR, but I do believe this is fine and will accept ASAP next week (or if someone else reviews and agrees, do the PR).

Thanks for finding this problem!

rsasse commented 6 years ago

Your proposal indeed fixes the problem and makes this a useful theory for the reader. Thanks again!