Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Benoit Viguier
coq-verif-tweetnacl
Commits
02d38ac7
Commit
02d38ac7
authored
Feb 13, 2020
by
Benoit Viguier
Browse files
change montgomery_rec to montgomery_rec_swap to better match the RFC
parent
2828d993
Changes
3
Hide whitespace changes
Inline
Side-by-side
paper/3-RFC.tex
View file @
02d38ac7
...
...
@@ -12,7 +12,7 @@ More specifically, we formalized X25519 with the following definition:
Definition RFC (n: list Z) (p: list Z) : list Z :=
let k := decodeScalar25519 n in
let u := decodeUCoordinate p in
let t := montgomery
_
rec
let t := montgomery
_
rec
_
swap
255 (* iterate 255 times *)
k (* clamped n *)
1 (* x
_
2 *)
...
...
@@ -21,60 +21,66 @@ Definition RFC (n: list Z) (p: list Z) : list Z :=
1 (* z
_
3 *)
0 (* dummy *)
0 (* dummy *)
u (* x
_
1 *) in
u (* x
_
1 *)
0 (* previous bit = 0 *) in
let a := get
_
a t in
let c := get
_
c t in
let o := ZPack25519 (Z.mul a (ZInv25519 c))
in encodeUCoordinate o.
\end{lstlisting}
In this definition
\coqe
{
montgomery
_
rec
}
is a generic ladder instantiated
In this definition
\coqe
{
montgomery
_
rec
_
swap
}
is a generic ladder instantiated
with integers and defined as follows:
\begin{lstlisting}
[language=Coq]
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 *)
Fixpoint montgomery
_
rec
_
swap (m : nat) (z : T')
(a: T) (b: T) (c: T) (d: T) (e: T) (f: T) (x: T) (swap:Z) :
(* a: x2 *)
(* b: x3 *)
(* c: z2 *)
(* d: z3 *)
(* e: temporary var *)
(* f: temporary var *)
(* x: x1 *)
(* swap: previous bit value *)
(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 *)
(* k
_
t = (k >> t)
&
1 *)
let swap := Z.lxor swap r in
(* swap
^
= k
_
t *)
let (a, b) := (Sel25519 swap a b, Sel25519 swap b a) in
(* (x
_
2, x
_
3) = cswap(swap, x
_
2, x
_
3) *)
let (c, d) := (Sel25519 swap c d, Sel25519 swap 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
(* 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 *)
montgomery
_
rec
_
swap n z a b c d e f x r
(* swap = k
_
t *)
| 0
%nat =>
let (a, b) := (Sel25519 swap a b, Sel25519 swap b a) in
(* (x
_
2, x
_
3) = cswap(swap, x
_
2, x
_
3) *)
let (c, d) := (Sel25519 swap c d, Sel25519 swap d c) in
(* (z
_
2, z
_
3) = cswap(swap, z
_
2, z
_
3) *)
(a,b,c,d,e,f)
end.
\end{lstlisting}
% The definitions of the encoding and decoding functions are detailed later
...
...
paper/5-highlevel.tex
View file @
02d38ac7
...
...
@@ -282,7 +282,7 @@ By taking \aref{alg:montgomery-ladder} and replacing \texttt{xDBL\&ADD} by a
combination of the formulae from
\lref
{
lemma:xADD
}
and
\lref
{
lemma:xDBL
}
,
we define a ladder
\coqe
{
opt
_
montgomery
}
(in which
$
\K
$
has not been fixed yet),
similar to the one used in TweetNaCl.
This definition is closely related to
\coqe
{
montgomery
_
rec
}
that was used
This definition is closely related to
\coqe
{
montgomery
_
rec
_
swap
}
that was used
in the definition of
\coqe
{
RFC
}
, and is easily proved to correspond to it.
In Coq this correspondence proof is hidden in the proof of
\coqe
{
RFC
_
Correct
}
shown above.
...
...
paper/A2_coq.tex
View file @
02d38ac7
...
...
@@ -27,52 +27,58 @@ Local Notation "X * Y" := (M X Y) (only parsing).
Local Notation "X
^
2" := (Sq X) (at level 40,
only parsing, left associativity).
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 *)
Fixpoint montgomery
_
rec
_
swap (m : nat) (z : T')
(a: T) (b: T) (c: T) (d: T) (e: T) (f: T) (x: T) (swap:Z) :
(* a: x2 *)
(* b: x3 *)
(* c: z2 *)
(* d: z3 *)
(* e: temporary var *)
(* f: temporary var *)
(* x: x1 *)
(* swap: previous bit value *)
(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 *)
(* k
_
t = (k >> t)
&
1 *)
let swap := Z.lxor swap r in
(* swap
^
= k
_
t *)
let (a, b) := (Sel25519 swap a b, Sel25519 swap b a) in
(* (x
_
2, x
_
3) = cswap(swap, x
_
2, x
_
3) *)
let (c, d) := (Sel25519 swap c d, Sel25519 swap 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
(* 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 *)
montgomery
_
rec
_
swap n z a b c d e f x r
(* swap = k
_
t *)
| 0
%nat =>
let (a, b) := (Sel25519 swap a b, Sel25519 swap b a) in
(* (x
_
2, x
_
3) = cswap(swap, x
_
2, x
_
3) *)
let (c, d) := (Sel25519 swap c d, Sel25519 swap d c) in
(* (z
_
2, z
_
3) = cswap(swap, z
_
2, z
_
3) *)
(a,b,c,d,e,f)
end.
Definition get
_
a (t:(T * T * T * T * T * T)) : T :=
match t with
(a,b,c,d,e,f) => a
...
...
@@ -172,11 +178,11 @@ Definition decodeUCoordinate (l: list Z) : Z :=
Definition encodeUCoordinate (x: Z) : list Z :=
ListofZ32 8 x.
(* instantiate montgomery
_
rec with Z
_
Ops *)
(* instantiate montgomery
_
rec
_
swap
with Z
_
Ops *)
Definition RFC (n: list Z) (p: list Z) : list Z :=
let k := decodeScalar25519 n in
let u := decodeUCoordinate p in
let t := montgomery
_
rec
let t := montgomery
_
rec
_
swap
255 (* iterate 255 times *)
k (* clamped n *)
1 (* x
_
2 *)
...
...
@@ -185,7 +191,8 @@ Definition RFC (n: list Z) (p: list Z) : list Z :=
1 (* z
_
3 *)
0 (* dummy *)
0 (* dummy *)
u (* x
_
1 *) in
u (* x
_
1 *)
0 (* previous bit = 0 *) in
let a := get
_
a t in
let c := get
_
c t in
let o := ZPack25519 (Z.mul a (ZInv25519 c))
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment