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