Stream: SSProve

Topic: RSA Signatures in SSProve

Jannik Mähn (May 03 2024 at 09:46):

Dear SSProvers,

I am working with signature schemes in SSProve. My implementation of the signature scheme is done with paramters. For instance:

Parameter SecKey  : finType.
Parameter SecKey_pos : Positive #|SecKey|.

Now, I want to instantiate this implementation with RSA Signatures. To do so, I want to use the mathcomp-extra implementation of RSA (https://github.com/thery/mathcomp-extra/blob/master/rsa.v). They define the RSA parameters as a record:

Record rsa := {
    p : nat;
    q : nat;
   pq : nat;
    e : nat;
    d : nat;
   wf : [&& prime p, prime q, p != q,
            0 < pq, p.-1 %| pq, q.-1 %| pq &
            e * d == 1 %[mod pq]]}.

Now, I defined the SecKey as:

Definition SecKey {r} : finType := [finType of 'Z_(pq r)].

Now I have to define the SecKey_pos parameter as well. How can I do this?
(I am confused because in my Definition of SecKey I have to pass {r}, which I don't have to do in my Parameter SecKey : finType.

Last updated: Oct 13 2024 at 01:02 UTC