A2_coq.tex 6.83 KB
Newer Older
Benoit Viguier's avatar
Benoit Viguier committed
1
2
3
4
5
\subsection{Coq definitions}
\label{appendix:coq}

\subsubsection{Montgomery Ladder}
\label{subsubsec:coq-ladder}
6
~
Benoit Viguier's avatar
Benoit Viguier committed
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
Generic definition of the ladder:

\begin{lstlisting}[language=Coq]
(* Typeclass to encapsulate the operations *)
Class Ops (T T': Type) (Mod: T -> T):=
{
  +   : T -> T -> T;           (* Add           *)
  *   : T -> T -> T;           (* Mult          *)
  -   : T -> T -> T;           (* Sub           *)
  x^2  : T -> T;                (* Square        *)
  C_0 : T;                     (* Constant 0    *)
  C_1 : T;                     (* Constant 1    *)
  C_121665: T;                 (* const (a-2)/4 *)
  Sel25519: Z -> T -> T -> T; (* CSWAP         *)
  Getbit: Z -> T' -> Z;       (* ith bit       *)
}.

Fixpoint montgomery_rec (m : nat) (z : T')
(a: T) (b: T) (c: T) (d: T) (e: T) (f: T) (x: T) :
(* a: x2              *)
(* b: x3              *)
(* c: z2              *)
(* d: z3              *)
(* e: temporary  var  *)
(* f: temporary  var  *)
(* x: x1              *)
(T * T * T * T * T * T) :=
match m with
| 0%nat => (a,b,c,d,e,f)
| S n =>
  let r := Getbit (Z.of_nat n) z in
    (* k_t = (k >> t) & 1                       *)
    (* swap <- k_t                              *)
  let (a, b) := (Sel25519 r a b, Sel25519 r b a) in
    (* (x_2, x_3) = cswap(swap, x_2, x_3)            *)
  let (c, d) := (Sel25519 r c d, Sel25519 r d c) in
    (* (z_2, z_3) = cswap(swap, z_2, z_3)            *)
  let e := a + c in  (* A = x_2 + z_2              *)
  let a := a - c in  (* B = x_2 - z_2              *)
  let c := b + d in  (* C = x_3 + z_3              *)
  let b := b - d in  (* D = x_3 - z_3              *)
  let d := e ^2 in    (* AA = A^2                  *)
  let f := a ^2 in    (* BB = B^2                  *)
  let a := c * a in  (* CB = C * B               *)
  let c := b * e in  (* DA = D * A               *)
  let e := a + c in  (* x_3 = (DA + CB)^2          *)
  let a := a - c in  (* z_3 = x_1 * (DA - CB)^2     *)
  let b := a ^2 in    (* z_3 = x_1 * (DA - CB)^2     *)
  let c := d - f in  (* E = AA - BB             *)
  let a := c * C_121665 in
                     (* z_2 = E * (AA + a24 * E) *)
  let a := a + d in  (* z_2 = E * (AA + a24 * E) *)
  let c := c * a in  (* z_2 = E * (AA + a24 * E) *)
  let a := d * f in  (* x_2 = AA * BB            *)
  let d := b * x in  (* z_3 = x_1 * (DA - CB)^2    *)
  let b := e ^2 in    (* x_3 = (DA + CB)^2         *)
  let (a, b) := (Sel25519 r a b, Sel25519 r b a) in
    (* (x_2, x_3) = cswap(swap, x_2, x_3)           *)
  let (c, d) := (Sel25519 r c d, Sel25519 r d c) in
    (* (z_2, z_3) = cswap(swap, z_2, z_3)           *)
  montgomery_rec n z a b c d e f x
end.

Definition get_a (t:(T * T * T * T * T * T)) : T :=
match t with
  (a,b,c,d,e,f) => a
end.
Definition get_c (t:(T * T * T * T * T * T)) : T :=
match t with
  (a,b,c,d,e,f) => c
end.
\end{lstlisting}

Benoit Viguier's avatar
Benoit Viguier committed
80
81
\subsubsection{RFC in Coq}
\label{subsubsec:RFC-Coq}
82
~
Benoit Viguier's avatar
Benoit Viguier committed
83
Instantiation of the Class \Coqe{Ops} with operations over \Z and modulo \p.
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
\begin{lstlisting}[language=Coq]
Definition modP (x:Z) : Z :=
  Z.modulo x (Z.pow 2 255 - 19).

(* Encapsulate in a module. *)
Module Mid.
  (* shift to the right by n bits *)
  Definition getCarry (n:Z) (m:Z) : Z :=
    Z.shiftr m n.

  (* logical and with n ones *)
  Definition getResidue (n:Z)  (m:Z) : Z :=
    Z.land n (Z.ones n).

  Definition car25519 (n:Z) : Z  :=
    38 * getCarry 256 n +  getResidue 256 n.
  (* The carry operation is invariant under modulo *)
  Lemma Zcar25519_correct:
    forall (n:Z), n:GF = (Mid.car25519 n) :GF.

  (* Define Mid.A, Mid.M ... *)
  Definition A a b := Z.add a b.
  Definition M a b :=
    car25519 (car25519 (Z.mul a b)).
  Definition Zub a b := Z.sub a b.
  Definition Sq a := M a a.
  Definition C_0 := 0.
  Definition C_1 := 1.
  Definition C_121665 := 121665.
  Definition Sel25519 (b p q:Z) :=
    if (Z.eqb b 0) then p else q.

  Definition getbit (i:Z) (a: Z) :=
    if (Z.ltb a 0) then
      0
    else if (Z.ltb i 0) then
        Z.land a 1
    else
        Z.land (Z.shiftr a i) 1.
End Mid.

(* Packing is applying a modulo p *)
Definition ZPack25519 n :=
  Z.modulo n (Z.pow 2 255 - 19).

(* And with 255 ones *)
(* unset last 3 bits *)
(* set bit 254       *)
Definition Zclamp (n : Z) : Z :=
  (Z.lor
    (Z.land n (Z.land (Z.ones 255) (-8)))
    (Z.shiftl 64 (31 * 8))).

(* x^{p - 2} *)
Definition ZInv25519 (x:Z) : Z :=
  Z.pow x (Z.pow 2 255 - 21).

Benoit Viguier's avatar
Benoit Viguier committed
141
(* instantiate over Z *)
142
143
Instance Z_Ops : (Ops Z Z modP) := {}.
Proof.
Benoit Viguier's avatar
aspell    
Benoit Viguier committed
144
145
146
147
148
149
150
151
152
  apply Mid.A.        (* instantiate +       *)
  apply Mid.M.        (* instantiate *       *)
  apply Mid.Zub.      (* instantiate -       *)
  apply Mid.Sq.       (* instantiate x^2      *)
  apply Mid.C_0.      (* instantiate Const 0 *)
  apply Mid.C_1.      (* instantiate Const 1 *)
  apply Mid.C_121665. (* instantiate (a-2)/4 *)
  apply Mid.Sel25519. (* instantiate CSWAP   *)
  apply Mid.getbit.   (* instantiate ith bit *)
153
154
Defined.

Benoit Viguier's avatar
Benoit Viguier committed
155
156
157
158
159
160
161
162
163
Definition decodeScalar25519 (l: list Z) : Z :=
  ZofList 8 (clamp l).

Definition decodeUCoordinate (l: list Z) : Z :=
  ZofList 16 (Unpack25519 l).

Definition encodeUCoordinate (x: Z) : list Z :=
  ListofZ32 8 x.

Benoit Viguier's avatar
Benoit Viguier committed
164
(* instantiate montgomery_rec with Z_Ops *)
Benoit Viguier's avatar
Benoit Viguier committed
165
166
167
Definition RFC (n: list Z) (p: list Z) : list Z :=
  let k := decodeScalar25519 n in
  let u := decodeUCoordinate p in
168
  let t := montgomery_rec
Benoit Viguier's avatar
Benoit Viguier committed
169
170
171
172
173
174
175
176
177
    255  (* iterate 255 times *)
    k    (* clamped n         *)
    1    (* x_2                *)
    u    (* x_3                *)
    0    (* z_2                *)
    1    (* z_3                *)
    0    (* dummy             *)
    0    (* dummy             *)
    u    (* x_1                *) in
178
179
  let a := get_a t in
  let c := get_c t in
Benoit Viguier's avatar
Benoit Viguier committed
180
181
  let o := ZPack25519 (Z.mul a (ZInv25519 c))
  in encodeUCoordinate o.
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
\end{lstlisting}

\subsubsection{CSM}
\label{subsubsec:CryptoScalarmult}
~
\begin{lstlisting}[language=Coq]
Definition Crypto_Scalarmult n p :=
let t := montgomery_rec
  255               (* iterate 255 times *)
  (clamp n)         (* clamped n         *)
  Low.C_1           (* x_2                *)
  (Unpack25519 p)   (* x_3                *)
  Low.C_0           (* z_2                *)
  Low.C_1           (* z_3                *)
  Low.C_0           (* dummy             *)
  Low.C_0           (* dummy             *)
  (Unpack25519 p)   (* x_1                *) in
let a := get_a t in
let c := get_c t in
Pack25519 (Low.M a (Inv25519 c)).

Definition CSM := Crypto_Scalarmult.
\end{lstlisting}

Benoit Viguier's avatar
Benoit Viguier committed
206
207
\subsubsection{Equivalence between For Loops}
\label{subsubsec:for}
208
~
Benoit Viguier's avatar
Benoit Viguier committed
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
\begin{lstlisting}[language=Coq]
Variable T: Type.
Variable g: nat -> T -> T.

Fixpoint rec_fn (n:nat) (s:T) :=
  match n with
  | 0 => s
  | S n => rec_fn n (g n s)
  end.

Fixpoint rec_fn_rev_acc (n:nat) (m:nat) (s:T) :=
  match n with
  | 0 => s
  | S n => g (m - n - 1) (rec_fn_rev_acc n m s)
  end.

Definition rec_fn_rev (n:nat) (s:T) :=
  rec_fn_rev_acc n n s.

Lemma Tail_Head_equiv :
  forall (n:nat) (s:T),
  rec_fn n s = rec_fn_rev n s.
\end{lstlisting}