Barkhausen-Institut / vRATLS

A formal specification for RATLS (remote attestation embedded into TLS).
0 stars 0 forks source link

Eilliptic Curve Signatures #8

Open sertel opened 1 month ago

sertel commented 1 month ago

The task is to implement signatures based on elliptic curves.

Here is what Jannik wrote so far:

Quick Elliptic Curves heads up

It is literally a curve in a two dimensional space, and points (x,y) on that curve form a group, where addition is the operation on group elements. Furthermore, there is a scalar multiplication. Points on a curve are denoted with capital letters, that is going to be a little confusing given the DH stuff, because the group structure itself is the same. So let's use the following. Say E_n for an elliptic curve of order n . A point P \in E_n is a touple of coordinates, i.e., P=(x,y). We denote G \in E_n as the point of the curve that is the generator of the group (similar to g in DH). The operation is addition, i.e., E_n={ G,2G,3G,4G,5G,...(n-1)G }. Here, for an integer k , we define the scalar multiplication as k*G=G+...+G (adding k times).

Setting

Alice and Bob agree on (curve, G,n). Curve is the curve, so they agree on the coefficients of the curve (E: y^2 = x^3 + ax + b, this is the form, always, so they agree on a and b). G is a point on E and n is a prime number.

Ln := bitlength(n)

Hash function is chosen

KeyGen():
1: sk := d_A <- sample uniform {1,...,n-1}
2: pk := Q_A := d_A * G
Sign(m,sk):
1: e := Hash(m), z := Ln leftmost bits of e
2: k <- sample uniform {1,...,n-1}
3: P := kG = (x_1,y_1). Calculate r = x1 (mod n). If r = 0, redo step 2.
4: s := k^(-1) * (z + r*d_A) (mod n). If s = 0, repeat step 2.
5: ret sig:= (r,s)
VerSign(sig,pk):
1: if r,s \notin {1,...,n-1} return false
2: e = Hash(m), z:=Ln leftmost bits of e.
3: w := s^(-1) (mod n)
4: u_1 := z*w (mod n), u_2 := r*w (mod n)
5: (x_1,y_1) := (u_1*G + u_2 * Q_A)
6: if r=x_1 mod n, ret true. else, return false
sertel commented 1 month ago

mathcomp-extra seems to already define the foundations for elliptic curves.

Based on that, we would need to define encrypt and decrypt and proof its according correctness.