cascremers / scyther

The Scyther Tool for the symbolic analysis of security protocols
https://cispa.saarland/group/cremers/scyther/index.html
96 stars 38 forks source link

One role per agent does not work #38

Closed Mofo50C closed 9 months ago

Mofo50C commented 9 months ago

Describe the bug The backend option --one-role-per-agent does nothing.

To Reproduce Steps to reproduce the behavior:

  1. Open GUI
  2. Go to settings
  3. Paste in --one-role-per-agent for backend arguments
  4. Run verify on protocol
  5. Attacks still show agents assuming multiple roles

Expected behavior Use this protocol and verify the claim(I, Commit, R, Kir) https://gist.github.com/Mofo50C/31246287024580ab24283c559f7887fd

Scyther version used:

Platform information (please complete the following information):

cascremers commented 9 months ago

Please add a picture here of the attacks. (When I try this, none of the generated attacks contain an agent that executes multiple roles.)

Mofo50C commented 9 months ago

Hi there, this is what i get for I's claim on commit R image image

Mofo50C commented 9 months ago

I've tried it with option "--one-role-per-agent"; in the actual protocol and --one-role-per-agent in the backend arguments. With 5 runs and best attack.

cascremers commented 9 months ago

In your image, there are two agents, and they each perform a different role. This is matches the requirements for the "one role per agent" switch.

Perhaps your concern is that Alice (when executing the I role), upon receiving the message, assumes that Alice is also performing the R role -- but this is only a variable instantiation, and does not imply Alice plays both roles. If the protocol has no explicit checks to exclude this behavior, then this is typically possible.

In any case, I think this is not a bug report, but rather a misunderstanding of the "one role per agent" restriction, which is met here.

Mofo50C commented 9 months ago

Oh I see, after playing around with the settings, i came across the following attack that is what i thought would be shown with the "one role per agent" argument. image