Question on asymmetric keys and digital signatures.

[terilenard]

Question 1: Is there a correct way to define a digital signature in Scyther?

Question 2: Is there a possibility to define a pair of asymmetric keys between two roles that are different built in ones (e.g., pk(i) and sk(i) for role I)?

The use-case is at follows. Role I stores a pair of asymmetric keys pk'(I) and sk'(i), different from pk(i) and sk(i). A role R knows pk'(i) because the key was pre-installed. If the protocol contains multiple instances of R, I want each R to know that a message came from I, but I doesn't need to know the identity (e.g., pk(r)) of each R.

The problem is that I do not want in my protocol the pk'(i) to be "too public". Using the built-in pki results in an attacker finding out pk(i) and can easily compromise the protocol.

Thank you for your time! Teri

[terilenard]

Follow-up to the question. I found in a paper somewhere on the internet the following possibility to define pk and sk:

fresh pk: Function, 
secret sk: Function, 
inversekeys(pk,sk);

inside I and R.

[cascremers]

Hi Teri,

In Section 10 of the manual ( https://github.com/cascremers/scyther/blob/master/gui/scyther-manual.pdf ) it is suggested to make a new function with a disjoint name. This would still imply the adversary can derive such keys.

Alternatively, you could try to declare pk2 and sk2 both as secret functions, but it is hard to figure out if this is a reasonable model of your actual protocol. In general I would recommend against using "secret" signature verification keys, as it is a non-standard use of the signature primitive that has led to problems in the past, see e.g., https://eprint.iacr.org/2019/779 .

Scyther's model of signatures is a bit coarse, but seems okay if all your verification keys are generated honestly or a strong signature scheme is used; if you want more accurate modeling in general you could consider using Tamarin and the models from the paper cited above.

Best,

Cas

On Thu, May 25, 2023 at 1:52 AM Teri Lenard @.***> wrote:

Follow-up to the question. I found in a paper somewhere on the internet the following possibility to define pk and sk:

fresh pk: Function, secret sk: Function, inversekeys(pk,sk);

inside I and R.

— Reply to this email directly, view it on GitHub https://github.com/cascremers/scyther/issues/34#issuecomment-1562530355, or unsubscribe https://github.com/notifications/unsubscribe-auth/AALJWOHSICKGDMYJ2664BADXH4MVJANCNFSM6AAAAAAYNN53ZM . You are receiving this because you are subscribed to this thread.Message ID: @.***>

[terilenard]

Thank you very much for the help! I will have a look over the links provided. And indeed, my plan is to look on Tamarin as well.

I think we can close the issue.

Best, Teri

[cascremers]

p.s. @terilenard the issue tracker is not the right place for questions like this, I recommend the mailing list in the future.