Skip to content
GitLab
Menu
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
6aef7107
Commit
6aef7107
authored
Sep 18, 2020
by
benoit
Browse files
wip
parent
d33cbd71
Changes
6
Hide whitespace changes
Inline
Side-by-side
paper/4.1-VST.tex
View file @
6aef7107
...
...
@@ -2,14 +2,16 @@
\label
{
subsec:with-VST
}
\begin{sloppypar}
We now turn our focus to the formal specification of
\TNaCle
{
crypto
_
scalarmult
}
.
We use our definition of X25519 from the RFC in the Hoare triple and prove
its correctness.
We now turn our focus to the formal specification of
\TNaCle
{
crypto
_
scalarmult
}
.
We use our definition of X25519 from the RFC in the Hoare triple and prove
its correctness.
\end{sloppypar}
\subheading
{
Specifications.
}
We show the soundness of TweetNaCl by proving a correspondence between
the C version of TweetNaCl and the same code as a pure Coq function.
\todo
{
same code => to fix
}
% why "pure" ?
% A pure function is a function where the return value is only determined by its
% input values, without observable side effects (Side effect are e.g. printing)
...
...
@@ -52,36 +54,36 @@ SEP (sh [{ v_q }] <<(uch32)-- mVI (RFC n p);
In this specification we state preconditions like:
\begin{itemize}
\item
[]
\VSTe
{
PRE
}
:
\VSTe
{_
p OF (tptr tuchar)
}
\\
The function
\TNaCle
{
crypto
_
scalarmult
}
takes as input three pointers to
arrays of unsigned bytes (
\VSTe
{
tptr tuchar
}
)
\VSTe
{_
p
}
,
\VSTe
{_
q
}
and
\VSTe
{_
n
}
.
The function
\TNaCle
{
crypto
_
scalarmult
}
takes as input three pointers to
arrays of unsigned bytes (
\VSTe
{
tptr tuchar
}
)
\VSTe
{_
p
}
,
\VSTe
{_
q
}
and
\VSTe
{_
n
}
.
\item
[]
\VSTe
{
LOCAL
}
:
\VSTe
{
temp
_
p v
_
p
}
\\
Each pointer represent an address
\VSTe
{
v
_
p
}
,
\VSTe
{
v
_
q
}
and
\VSTe
{
v
_
n
}
.
Each pointer represent an address
\VSTe
{
v
_
p
}
,
\VSTe
{
v
_
q
}
and
\VSTe
{
v
_
n
}
.
\item
[]
\VSTe
{
SEP
}
:
\VSTe
{
sh [
{
v
_
p
$
\!\!\}\!\!
]
\!\!\!
$
<<(uch32)-- mVI p
}
\\
In the memory share
\texttt
{
sh
}
, the address
\VSTe
{
v
_
p
}
points
to a list of integer values
\VSTe
{
mVI p
}
.
In the memory share
\texttt
{
sh
}
, the address
\VSTe
{
v
_
p
}
points
to a list of integer values
\VSTe
{
mVI p
}
.
\item
[]
\VSTe
{
PROP
}
:
\VSTe
{
Forall (fun x => 0 <= x < 2
^
8) p
}
\\
In order to consider all the possible inputs, we assume each
element of the list
\texttt
{
p
}
to be bounded by
$
0
$
included and
$
2
^
8
$
excluded.
In order to consider all the possible inputs, we assume each
element of the list
\texttt
{
p
}
to be bounded by
$
0
$
included and
$
2
^
8
$
excluded.
\item
[]
\VSTe
{
PROP
}
:
\VSTe
{
Zlength p = 32
}
\\
We also assume that the length of the list
\texttt
{
p
}
is 32. This defines the
complete representation of
\TNaCle
{
u8[32]
}
.
We also assume that the length of the list
\texttt
{
p
}
is 32. This defines the
complete representation of
\TNaCle
{
u8[32]
}
.
\end{itemize}
As postcondition we have conditions like:
\begin{itemize}
\item
[]
\VSTe
{
POST
}
:
\VSTe
{
tint
}
\\
The function
\TNaCle
{
crypto
_
scalarmult
}
returns an integer.
The function
\TNaCle
{
crypto
_
scalarmult
}
returns an integer.
\item
[]
\VSTe
{
LOCAL
}
:
\VSTe
{
temp ret
_
temp (Vint Int.zero)
}
\\
The returned integer has value
$
0
$
.
The returned integer has value
$
0
$
.
\item
[]
\VSTe
{
SEP
}
:
\VSTe
{
sh [
{
v
_
q
$
\!\!\}\!\!
]
\!\!\!
$
<<(uch32)-- mVI (RFC n p)
}
\\
In the memory share
\texttt
{
sh
}
, the address
\VSTe
{
v
_
q
}
points
to a list of integer values
\VSTe
{
mVI (RFC n p)
}
where
\VSTe
{
RFC n p
}
is the
result of the
\TNaCle
{
crypto
_
scalarmult
}
of
\VSTe
{
n
}
and
\VSTe
{
p
}
.
In the memory share
\texttt
{
sh
}
, the address
\VSTe
{
v
_
q
}
points
to a list of integer values
\VSTe
{
mVI (RFC n p)
}
where
\VSTe
{
RFC n p
}
is the
result of the
\TNaCle
{
crypto
_
scalarmult
}
of
\VSTe
{
n
}
and
\VSTe
{
p
}
.
\item
[]
\VSTe
{
PROP
}
:
\VSTe
{
Forall (fun x => 0 <= x < 2
^
8) (RFC n p)
}
\\
\VSTe
{
PROP
}
:
\VSTe
{
Zlength (RFC n p) = 32
}
\\
We show that the computation for
\VSTe
{
RFC
}
fits in
\TNaCle
{
u8[32]
}
.
\VSTe
{
PROP
}
:
\VSTe
{
Zlength (RFC n p) = 32
}
\\
We show that the computation for
\VSTe
{
RFC
}
fits in
\TNaCle
{
u8[32]
}
.
\end{itemize}
\TNaCle
{
crypto
_
scalarmult
}
computes the same result as
\VSTe
{
RFC
}
...
...
paper/5-highlevel.tex
View file @
6aef7107
...
...
@@ -4,9 +4,9 @@
In this section we prove the following informal theorem:
\begin{informaltheorem}
The implementation of X25519 in TweetNaCl computes the
$
\F
{
p
}$
-restricted
\xcoord
scalar multiplication on
$
E
(
\F
{
p
^
2
}
)
$
where
$
p
$
is
$
\p
$
and
$
E
$
is the elliptic curve
$
y
^
2
=
x
^
3
+
486662
x
^
2
+
x
$
.
The implementation of X25519 in TweetNaCl computes the
$
\F
{
p
}$
-restricted
\xcoord
scalar multiplication on
$
E
(
\F
{
p
^
2
}
)
$
where
$
p
$
is
$
\p
$
and
$
E
$
is the elliptic curve
$
y
^
2
=
x
^
3
+
486662
x
^
2
+
x
$
.
\end{informaltheorem}
More precisely, we prove that our formalization of the RFC matches the definitions of Curve25519 by Bernstein:
...
...
@@ -46,15 +46,15 @@ We consider elliptic curves over a field $\K$. We assume that the
characteristic of
$
\K
$
is neither 2 or 3.
\begin{dfn}
Given a field
$
\K
$
,
using an appropriate choice of coordinates,
an elliptic curve
$
E
$
is a plane cubic algebraic curve defined by an equation
$
E
(
x,y
)
$
of the form:
$$
E : y
^
2
+
a
_
1
xy
+
a
_
3
y
=
x
^
3
+
a
_
2
x
^
2
+
a
_
4
x
+
a
_
6
$$
where the
$
a
_
i
$
's are in
\K\
and the curve has no singular point (
\ie
no cusps
or self-intersections). The set of points defined over
\K
, written
$
E
(
\K
)
$
, is formed by the
solutions
$
(
x,y
)
$
of
$
E
$
together with a distinguished point
$
\Oinf
$
called point at infinity:
$$
E
(
\K
)
=
\{
(
x,y
)
\in
\K
\times
\K
~|~E
(
x,y
)
\}
\cup
\{\Oinf\}
$$
Given a field
$
\K
$
,
using an appropriate choice of coordinates,
an elliptic curve
$
E
$
is a plane cubic algebraic curve defined by an equation
$
E
(
x,y
)
$
of the form:
$$
E : y
^
2
+
a
_
1
xy
+
a
_
3
y
=
x
^
3
+
a
_
2
x
^
2
+
a
_
4
x
+
a
_
6
$$
where the
$
a
_
i
$
's are in
\K\
and the curve has no singular point (
\ie
no cusps
or self-intersections). The set of points defined over
\K
, written
$
E
(
\K
)
$
, is formed by the
solutions
$
(
x,y
)
$
of
$
E
$
together with a distinguished point
$
\Oinf
$
called point at infinity:
$$
E
(
\K
)
=
\{
(
x,y
)
\in
\K
\times
\K
~|~E
(
x,y
)
\}
\cup
\{\Oinf\}
$$
\end{dfn}
\subsubsection
{
Short Weierstra
{
\ss
}
curves
}
...
...
@@ -63,16 +63,16 @@ $$E(\K) = \{ (x,y) \in \K \times \K ~|~E(x,y)\} \cup \{\Oinf\}$$
This equation
$
E
(
x,y
)
$
can be reduced into its short Weierstra
{
\ss
}
form.
\begin{dfn}
Let
$
a
\in
\K
$
and
$
b
\in
\K
$
such that
$$
\Delta
(
a,b
)
=
-
16
(
4
a
^
3
+
27
b
^
2
)
\neq
0
.
$$
The
\textit
{
elliptic curve
}
$
E
_{
a,b
}$
is defined by the equation:
$$
y
^
2
=
x
^
3
+
ax
+
b.
$$
$
E
_{
a,b
}
(
\K
)
$
is the set of all points
$
(
x,y
)
\in
\K
^
2
$
satisfying the
$
E
_{
a,b
}$
along with an additional formal point
$
\Oinf
$
, ``at infinity''. Such a curve does not have any singularity.
Let
$
a
\in
\K
$
and
$
b
\in
\K
$
such that
$$
\Delta
(
a,b
)
=
-
16
(
4
a
^
3
+
27
b
^
2
)
\neq
0
.
$$
The
\textit
{
elliptic curve
}
$
E
_{
a,b
}$
is defined by the equation:
$$
y
^
2
=
x
^
3
+
ax
+
b.
$$
$
E
_{
a,b
}
(
\K
)
$
is the set of all points
$
(
x,y
)
\in
\K
^
2
$
satisfying the
$
E
_{
a,b
}$
along with an additional formal point
$
\Oinf
$
, ``at infinity''. Such a curve does not have any singularity.
\end{dfn}
In this setting, Bartzia and Strub defined the parametric type
\texttt
{
ec
}
which
represent the points on a specific curve. It is parameterized by
a
\texttt
{
K : ecuFieldType
}
--- the type of fields wh
ich
characteristic is not 2 or 3 ---
a
\texttt
{
K : ecuFieldType
}
--- the type of fields wh
ose
characteristic is not 2 or 3 ---
and
\texttt
{
E : ecuType
}
--- a record that packs the curve parameters
$
a
$
and
$
b
$
along with the proof that
$
\Delta
(
a,b
)
\neq
0
$
.
\begin{lstlisting}
[language=Coq]
...
...
@@ -93,7 +93,7 @@ Points on an elliptic curve are equipped with the structure of an abelian group.
\begin{itemize}
\item
The negation of a point
$
P
=
(
x,y
)
$
is defined by reflection over the
$
x
$
axis
$
-
P
=
(
x,
-
y
)
$
.
\item
The addition of two points
$
P
$
and
$
Q
$
is defined as the negation of the third intersection point
of the line passing through
$
P
$
and
$
Q
$
, or tangent to
$
P
$
if
$
P
=
Q
$
.
of the line passing through
$
P
$
and
$
Q
$
, or tangent to
$
P
$
if
$
P
=
Q
$
.
\item
$
\Oinf
$
is the neutral element under this law: if 3 points are collinear, their sum is equal to
$
\Oinf
$
.
\end{itemize}
These operations are defined in Coq as follows (where we omit the code for the tangent case):
...
...
@@ -112,7 +112,7 @@ Definition add (p1 p2 : point) :=
(| xs, - s * (xs - x1 ) - y1 |)
end.
\end{lstlisting}
The value of
\texttt
{
add
}
is proven to be on the curve
(
with coercion
)
:
The value of
\texttt
{
add
}
is proven to be on the curve with coercion:
\begin{lstlisting}
[language=Coq]
Lemma addO (p q : ec): oncurve (add p q).
...
...
@@ -136,7 +136,7 @@ than the Weierstra{\ss} form. We consider the Montgomery form \cite{MontgomerySp
Similar to the definition of
\texttt
{
ec
}
, we defined the parametric type
\texttt
{
mc
}
which
represents the points on a specific Montgomery curve.
It is parameterized by
a
\texttt
{
K : ecuFieldType
}
--- the type of fields wh
ich
characteristic is not
a
\texttt
{
K : ecuFieldType
}
--- the type of fields wh
ose
characteristic is not
2 or 3 --- and
\texttt
{
M : mcuType
}
--- a record that packs the curve
parameters
$
a
$
and
$
b
$
along with the proofs that
$
b
\neq
0
$
and
$
a
^
2
\neq
4
$
.
\begin{lstlisting}
[language=Coq,belowskip=-0.1
\baselineskip
]
...
...
@@ -182,8 +182,8 @@ corresponding property for Weierstra{\ss} curves.
then
$
E
_{
a',b'
}$
is an elliptic curve, and the mapping
$
\varphi
: M
_{
a,b
}
\mapsto
E
_{
a',b'
}$
defined as:
\begin{align*}
\varphi
(
\Oinf
_
M)
&
=
\Oinf
_
E
\\
\varphi
( (x , y) )
&
=
\left
(
\frac
{
x
}{
b
}
+
\frac
{
a
}{
3b
}
,
\frac
{
y
}{
b
}
\right
)
\varphi
(
\Oinf
_
M)
&
=
\Oinf
_
E
\\
\varphi
( (x , y) )
&
=
\left
(
\frac
{
x
}{
b
}
+
\frac
{
a
}{
3b
}
,
\frac
{
y
}{
b
}
\right
)
\end{align*}
is an isomorphism between elliptic curves.
\end{lemma}
...
...
@@ -226,8 +226,8 @@ setting $Z=0$, we derive $X=0$, giving us the ``infinite point'' $(0:1:0)$.
By restricting the parameter
$
a
$
of
$
M
_{
a,b
}
(
\K
)
$
such that
$
a
^
2
-
4
$
is not a
square in
\K
, we ensure that
$
(
0
,
0
)
$
is the only point with a
$
y
$
-coordinate of
$
0
$
.
\begin{hypothesis}
\label
{
hyp:a
_
minus
_
4
_
not
_
square
}
$
a
^
2
-
4
$
is not a square in
\K
.
\label
{
hyp:a
_
minus
_
4
_
not
_
square
}
$
a
^
2
-
4
$
is not a square in
\K
.
\end{hypothesis}
\begin{lstlisting}
[language=Coq]
Hypothesis mcu
_
no
_
square : forall x : K, x
^
+2 != (M#a)
^
+2 - 4
%:R.
...
...
@@ -235,41 +235,41 @@ Hypothesis mcu_no_square : forall x : K, x^+2 != (M#a)^+2 - 4%:R.
We define
$
\chi
$
and
$
\chi
_
0
$
to return the
\xcoord
of points on a curve.
\begin{dfn}
Let
$
\chi
$
and
$
\chi
_
0
$
:
\\
--
$
\chi
: M
_{
a,b
}
(
\K
)
\to
\K
\cup
\{\infty\}
$
\\
--
$
\chi
: M
_{
a,b
}
(
\K
)
\to
\K
\cup
\{\infty\}
$
\\
such that
$
\chi
(
\Oinf
)
=
\infty
$
and
$
\chi
((
x,y
))
=
x
$
.
\\
--
$
\chi
_
0
: M
_{
a,b
}
(
\K
)
\to
\K
$
\\
--
$
\chi
_
0
: M
_{
a,b
}
(
\K
)
\to
\K
$
\\
such that
$
\chi
_
0
(
\Oinf
)
=
0
$
and
$
\chi
_
0
((
x,y
))
=
x
$
.
\end{dfn}
Using projective coordinates we prove the formula for differential addition.
% (\lref{lemma:xADD}).
\begin{lemma}
\label
{
lemma:xADD
}
Let
$
M
_{
a,b
}$
be a Montgomery curve such that
$
a
^
2
-
4
$
is not a square in
\K
, and
let
$
X
_
1
, Z
_
1
, X
_
2
, Z
_
2
, X
_
4
, Z
_
4
\in
\K
$
, such that
$
(
X
_
1
,Z
_
1
)
\neq
(
0
,
0
)
$
,
$
(
X
_
2
,Z
_
2
)
\neq
(
0
,
0
)
$
,
$
X
_
4
\neq
0
$
and
$
Z
_
4
\neq
0
$
.
Define
\begin{align*}
X
_
3
&
= Z
_
4((X
_
1 - Z
_
1)(X
_
2+Z
_
2) + (X
_
1+Z
_
1)(X
_
2-Z
_
2))
^
2
\\
Z
_
3
&
= X
_
4((X
_
1 - Z
_
1)(X
_
2+Z
_
2) - (X
_
1+Z
_
1)(X
_
2-Z
_
2))
^
2,
\end{align*}
then for any point
$
P
_
1
$
and
$
P
_
2
$
in
$
M
_{
a,b
}
(
\K
)
$
such that
$
X
_
1
/
Z
_
1
=
\chi
(
P
_
1
)
, X
_
2
/
Z
_
2
=
\chi
(
P
_
2
)
$
, and
$
X
_
4
/
Z
_
4
=
\chi
(
P
_
1
-
P
_
2
)
$
,
we have
$
X
_
3
/
Z
_
3
=
\chi
(
P
_
1
+
P
_
2
)
$
.
\\
\textbf
{
Remark:
}
These definitions should be understood in
$
\K
\cup
\{\infty\}
$
.
If
$
x
\ne
0
$
then we define
$
x
/
0
=
\infty
$
.
\label
{
lemma:xADD
}
Let
$
M
_{
a,b
}$
be a Montgomery curve such that
$
a
^
2
-
4
$
is not a square in
\K
, and
let
$
X
_
1
, Z
_
1
, X
_
2
, Z
_
2
, X
_
4
, Z
_
4
\in
\K
$
, such that
$
(
X
_
1
,Z
_
1
)
\neq
(
0
,
0
)
$
,
$
(
X
_
2
,Z
_
2
)
\neq
(
0
,
0
)
$
,
$
X
_
4
\neq
0
$
and
$
Z
_
4
\neq
0
$
.
Define
\begin{align*}
X
_
3
&
= Z
_
4((X
_
1 - Z
_
1)(X
_
2+Z
_
2) + (X
_
1+Z
_
1)(X
_
2-Z
_
2))
^
2
\\
Z
_
3
&
= X
_
4((X
_
1 - Z
_
1)(X
_
2+Z
_
2) - (X
_
1+Z
_
1)(X
_
2-Z
_
2))
^
2,
\end{align*}
then for any point
$
P
_
1
$
and
$
P
_
2
$
in
$
M
_{
a,b
}
(
\K
)
$
such that
$
X
_
1
/
Z
_
1
=
\chi
(
P
_
1
)
, X
_
2
/
Z
_
2
=
\chi
(
P
_
2
)
$
, and
$
X
_
4
/
Z
_
4
=
\chi
(
P
_
1
-
P
_
2
)
$
,
we have
$
X
_
3
/
Z
_
3
=
\chi
(
P
_
1
+
P
_
2
)
$
.
\\
\textbf
{
Remark:
}
These definitions should be understood in
$
\K
\cup
\{\infty\}
$
.
If
$
x
\ne
0
$
then we define
$
x
/
0
=
\infty
$
.
\end{lemma}
Similarly we also prove the formula for point doubling.
% (\lref{lemma:xDBL}).
\begin{lemma}
\label
{
lemma:xDBL
}
Let
$
M
_{
a,b
}$
be a Montgomery curve such that
$
a
^
2
-
4
$
is not a square in
\K
, and
let
$
X
_
1
, Z
_
1
\in
\K
$
, such that
$
(
X
_
1
,Z
_
1
)
\neq
(
0
,
0
)
$
. Define
\begin{align*}
c
&
= (X
_
1 + Z
_
1)
^
2 - (X
_
1 - Z
_
1)
^
2
\\
X
_
3
&
= (X
_
1 + Z
_
1)
^
2(X
_
1-Z
_
1)
^
2
\\
Z
_
3
&
= c
\Big
((X
_
1 + Z
_
1)
^
2+
\frac
{
a-2
}{
4
}
\times
c
\Big
),
\end{align*}
then for any point
$
P
_
1
$
in
$
M
_{
a,b
}
(
\K
)
$
such that
$
X
_
1
/
Z
_
1
=
\chi
(
P
_
1
)
$
,
we have
$
X
_
3
/
Z
_
3
=
\chi
(
2
P
_
1
)
$
.
\label
{
lemma:xDBL
}
Let
$
M
_{
a,b
}$
be a Montgomery curve such that
$
a
^
2
-
4
$
is not a square in
\K
, and
let
$
X
_
1
, Z
_
1
\in
\K
$
, such that
$
(
X
_
1
,Z
_
1
)
\neq
(
0
,
0
)
$
. Define
\begin{align*}
c
&
= (X
_
1 + Z
_
1)
^
2 - (X
_
1 - Z
_
1)
^
2
\\
X
_
3
&
= (X
_
1 + Z
_
1)
^
2(X
_
1-Z
_
1)
^
2
\\
Z
_
3
&
= c
\Big
((X
_
1 + Z
_
1)
^
2+
\frac
{
a-2
}{
4
}
\times
c
\Big
),
\end{align*}
then for any point
$
P
_
1
$
in
$
M
_{
a,b
}
(
\K
)
$
such that
$
X
_
1
/
Z
_
1
=
\chi
(
P
_
1
)
$
,
we have
$
X
_
3
/
Z
_
3
=
\chi
(
2
P
_
1
)
$
.
\end{lemma}
With
\lref
{
lemma:xADD
}
and
\lref
{
lemma:xDBL
}
, we are able to compute efficiently
...
...
@@ -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 (with \coqe{montgomery_rec}).
% shown above.
% shown above.
% We prove its correctness for any point whose \xcoord is not 0.
%
...
...
@@ -307,9 +307,9 @@ we define a ladder \coqe{opt_montgomery} (in which $\K$ has not been fixed yet).
This gives us the theorem of the correctness of the Montgomery ladder.
\begin{theorem}
\label
{
thm:montgomery-ladder-correct
}
For all
$
n, m
\in
\N
$
,
$
x
\in
\K
$
,
$
P
\in
M
_{
a,b
}
(
\K
)
$
,
if
$
\chi
_
0
(
P
)
=
x
$
then
\coqe
{
opt
_
montgomery
}
returns
$
\chi
_
0
(
n
\cdot
P
)
$
\label
{
thm:montgomery-ladder-correct
}
For all
$
n, m
\in
\N
$
,
$
x
\in
\K
$
,
$
P
\in
M
_{
a,b
}
(
\K
)
$
,
if
$
\chi
_
0
(
P
)
=
x
$
then
\coqe
{
opt
_
montgomery
}
returns
$
\chi
_
0
(
n
\cdot
P
)
$
\end{theorem}
\begin{lstlisting}
[language=Coq]
Theorem opt
_
montgomery
_
ok (n m: nat) (x : K) :
...
...
@@ -344,8 +344,8 @@ preventing the use \tref{thm:montgomery-ladder-correct}
with
$
\K
=
\F
{
p
^
2
}$
.
\begin{sloppypar}
We first study Curve25519 and one of its quadratic twists Twist25519,
both defined over
\F
{
p
}
.
We first study Curve25519 and one of its quadratic twists Twist25519,
both defined over
\F
{
p
}
.
\end{sloppypar}
\subsubsection
{
Curves and twists
}
...
...
@@ -387,22 +387,22 @@ Fact two_not_square : forall x: Zmodp.type,
We now consider
$
M
_{
486662
,
1
}
(
\F
{
p
}
)
$
and
$
M
_{
486662
,
2
}
(
\F
{
p
}
)
$
, one of its quadratic twists.
% \begin{dfn}Let the following instantiations of \aref{alg:montgomery-double-add}:\\
\begin{dfn}
%Let the following instantiations of \aref{alg:montgomery-ladder}:\\
We instantiate
\coqe
{
opt
_
montgomery
}
in two specific ways:
\\
--
$
Curve
25519
\_
Fp
(
n,x
)
$
for
$
M
_{
486662
,
1
}
(
\F
{
p
}
)
$
.
\\
--
$
Twist
25519
\_
Fp
(
n,x
)
$
for
$
M
_{
486662
,
2
}
(
\F
{
p
}
)
$
.
%Let the following instantiations of \aref{alg:montgomery-ladder}:\\
We instantiate
\coqe
{
opt
_
montgomery
}
in two specific ways:
\\
--
$
Curve
25519
\_
Fp
(
n,x
)
$
for
$
M
_{
486662
,
1
}
(
\F
{
p
}
)
$
.
\\
--
$
Twist
25519
\_
Fp
(
n,x
)
$
for
$
M
_{
486662
,
2
}
(
\F
{
p
}
)
$
.
\end{dfn}
With
\tref
{
thm:montgomery-ladder-correct
}
we derive the following two lemmas:
\begin{lemma}
For all
$
x
\in
\F
{
p
}
,
\
n
\in
\N
,
\
P
\in
\F
{
p
}
\times
\F
{
p
}$
,
\\
such that
$
P
\in
M
_{
486662
,
1
}
(
\F
{
p
}
)
$
and
$
\chi
_
0
(
P
)
=
x
$
.
$$
Curve
25519
\_
Fp
(
n,x
)
=
\chi
_
0
(
n
\cdot
P
)
$$
For all
$
x
\in
\F
{
p
}
,
\
n
\in
\N
,
\
P
\in
\F
{
p
}
\times
\F
{
p
}$
,
\\
such that
$
P
\in
M
_{
486662
,
1
}
(
\F
{
p
}
)
$
and
$
\chi
_
0
(
P
)
=
x
$
.
$$
Curve
25519
\_
Fp
(
n,x
)
=
\chi
_
0
(
n
\cdot
P
)
$$
\end{lemma}
\begin{lemma}
For all
$
x
\in
\F
{
p
}
,
\
n
\in
\N
,
\
P
\in
\F
{
p
}
\times
\F
{
p
}$
\\
such that
$
P
\in
M
_{
486662
,
2
}
(
\F
{
p
}
)
$
and
$
\chi
_
0
(
P
)
=
x
$
.
$$
Twist
25519
\_
Fp
(
n,x
)
=
\chi
_
0
(
n
\cdot
P
)
$$
For all
$
x
\in
\F
{
p
}
,
\
n
\in
\N
,
\
P
\in
\F
{
p
}
\times
\F
{
p
}$
\\
such that
$
P
\in
M
_{
486662
,
2
}
(
\F
{
p
}
)
$
and
$
\chi
_
0
(
P
)
=
x
$
.
$$
Twist
25519
\_
Fp
(
n,x
)
=
\chi
_
0
(
n
\cdot
P
)
$$
\end{lemma}
As the Montgomery ladder does not depend on
$
b
$
, it is trivial to
see that the computations done for points in
$
M
_{
486662
,
1
}
(
\F
{
p
}
)
$
and in
...
...
@@ -490,15 +490,15 @@ As in $\F{p}$, we define $0^{-1} = 0$ and prove \lref{lemma:Zmodp2_field}.
We then specialize the basic operations in order to speed up the verification
of formulas by using rewrite rules:
\begin{equation*}
\begin{split}
(a,0) + (b,0)
&
= (a+b, 0)
\\
(a, 0)
^{
-1
}
&
= (a
^{
-1
}
, 0)
\end{split}
\qquad
\begin{split}
(a,0)
\cdot
(b,0)
&
= (a
\cdot
b, 0)
\\
(0,a)
^{
-1
}
&
= (0,(2
\cdot
a)
^{
-1
}
)
\end{split}
\begin{split}
(a,0) + (b,0)
&
= (a+b, 0)
\\
(a, 0)
^{
-1
}
&
= (a
^{
-1
}
, 0)
\end{split}
\qquad
\begin{split}
(a,0)
\cdot
(b,0)
&
= (a
\cdot
b, 0)
\\
(0,a)
^{
-1
}
&
= (0,(2
\cdot
a)
^{
-1
}
)
\end{split}
\end{equation*}
The injection
$
a
\mapsto
(
a,
0
)
$
from
$
\F
{
p
}$
to
$
\F
{
p
^
2
}$
preserves
...
...
@@ -521,12 +521,12 @@ Lemma x_is_on_curve_or_twist_implies_x_in_Fp2:
We now study the case of the scalar multiplication and show similar proofs.
\begin{dfn}
Define the functions
$
\varphi
_
c
$
,
$
\varphi
_
t
$
and
$
\psi
$
\\
--
$
\varphi
_
c: M
_{
486662
,
1
}
(
\F
{
p
}
)
\mapsto
M
_{
486662
,
1
}
(
\F
{
p
^
2
}
)
$
\\
Define the functions
$
\varphi
_
c
$
,
$
\varphi
_
t
$
and
$
\psi
$
\\
--
$
\varphi
_
c: M
_{
486662
,
1
}
(
\F
{
p
}
)
\mapsto
M
_{
486662
,
1
}
(
\F
{
p
^
2
}
)
$
\\
such that
$
\varphi
((
x,y
))
=
((
x,
0
)
,
(
y,
0
))
$
.
\\
--
$
\varphi
_
t: M
_{
486662
,
2
}
(
\F
{
p
}
)
\mapsto
M
_{
486662
,
1
}
(
\F
{
p
^
2
}
)
$
\\
--
$
\varphi
_
t: M
_{
486662
,
2
}
(
\F
{
p
}
)
\mapsto
M
_{
486662
,
1
}
(
\F
{
p
^
2
}
)
$
\\
such that
$
\varphi
((
x,y
))
=
((
x,
0
)
,
(
0
,y
))
$
.
\\
--
$
\psi
:
\F
{
p
^
2
}
\mapsto
\F
{
p
}$
\\
--
$
\psi
:
\F
{
p
^
2
}
\mapsto
\F
{
p
}$
\\
such that
$
\psi
(
x,y
)
=
x
$
.
\end{dfn}
...
...
@@ -535,14 +535,14 @@ Define the functions $\varphi_c$, $\varphi_t$ and $\psi$\\
For all
$
n
\in
\N
$
, for all point
$
P
\in\F
{
p
}
\times\F
{
p
}$
on the curve
$
M
_{
486662
,
1
}
(
\F
{
p
}
)
$
(respectively on the quadratic twist
$
M
_{
486662
,
2
}
(
\F
{
p
}
)
$
), we have:
\begin{align*}
P
\in
M
_{
486662,1
}
(
\F
{
p
}
)
&
\implies
\varphi
_
c(n
\cdot
P) = n
\cdot
\varphi
_
c(P)
\\
P
\in
M
_{
486662,2
}
(
\F
{
p
}
)
&
\implies
\varphi
_
t(n
\cdot
P) = n
\cdot
\varphi
_
t(P)
P
\in
M
_{
486662,1
}
(
\F
{
p
}
)
&
\implies
\varphi
_
c(n
\cdot
P) = n
\cdot
\varphi
_
c(P)
\\
P
\in
M
_{
486662,2
}
(
\F
{
p
}
)
&
\implies
\varphi
_
t(n
\cdot
P) = n
\cdot
\varphi
_
t(P)
\end{align*}
\end{lemma}
Notice that:
\begin{align*}
\forall
P
\in
M
_{
486662,1
}
(
\F
{
p
}
),
\ \ \psi
(
\chi
_
0(
\varphi
_
c(P))) =
\chi
_
0(P)
\\
\forall
P
\in
M
_{
486662,2
}
(
\F
{
p
}
),
\ \ \psi
(
\chi
_
0(
\varphi
_
t(P))) =
\chi
_
0(P)
\forall
P
\in
M
_{
486662,1
}
(
\F
{
p
}
),
\ \ \psi
(
\chi
_
0(
\varphi
_
c(P))) =
\chi
_
0(P)
\\
\forall
P
\in
M
_{
486662,2
}
(
\F
{
p
}
),
\ \ \psi
(
\chi
_
0(
\varphi
_
t(P))) =
\chi
_
0(P)
\end{align*}
In summary for all
$
n
\in
\N
,
\
n <
2
^{
255
}$
, for any given point
$
P
\in\F
{
p
}
\times\F
{
p
}$
...
...
paper/_reviews/A4_reviews-UsenixB.tex
View file @
6aef7107
...
...
@@ -3,12 +3,11 @@
\begin{tabular}
{
rl
}
\toprule
Review recommendation
&
4. Minor revision
\\
Writing quality
&
4. Well-written
\\
Reviewer interest
&
3. I would definitely go to this
\\
&
talk and tell my students or
\\
&
colleagues to read this paper
\\
Reviewer expertise
&
4. Expert
\\
Review recommendation
&
4. Minor revision
\\
Writing quality
&
4. Well-written
\\
Reviewer interest
&
3. I would definitely go to this talk and tell my students or colleagues
\\
&
to read this paper
\\
Reviewer expertise
&
4. Expert
\\
\bottomrule
\end{tabular}
...
...
paper/_reviews/A4_reviews-UsenixD.tex
View file @
6aef7107
...
...
@@ -3,12 +3,11 @@
\begin{tabular}
{
rl
}
\toprule
Review recommendation
&
5. Accept
\\
Writing quality
&
4. Well-written
\\
Reviewer interest
&
3. I would definitely go to this
\\
&
talk and tell my students or
\\
&
colleagues to read this paper
\\
Reviewer expertise
&
2. Some familiarity
\\
Review recommendation
&
5. Accept
\\
Writing quality
&
4. Well-written
\\
Reviewer interest
&
3. I would definitely go to this talk and tell my students or colleagues
\\
&
to read this paper
\\
Reviewer expertise
&
2. Some familiarity
\\
\bottomrule
\end{tabular}
...
...
paper/tikz/highlevel1.tex
View file @
6aef7107
\begin{tikzpicture}
[textstyle/.style=
{
black, anchor= south west, align=center, minimum height=0.45cm, text centered, font=
\
scriptsize
}
]
\begin{tikzpicture}
[textstyle/.style=
{
black, anchor= south west, align=center, minimum height=0.45cm, text centered, font=
\
tiny
}
]
% Bartzia & Strub
% Bartzia & Strub
\draw
[dashed, fill=doc@lstbackground]
(2.75,0.5) -- (2.75,2) -- (6,2) -- (6, 0.5) -- cycle;
\draw
(6,2) node[textstyle, anchor=north east]
{
Library from Bartzia
\&
Strub
}
;
% Mab
% Mab
\begin{scope}
[yshift=0 cm,xshift=0 cm]
\draw
(0,0) -- (1.5,0) -- (1.5,-0.75) -- (0, -0.75) -- cycle;
\draw
(0.75,-0.375) node[textstyle, anchor=center]
{$
M
_{
a,b
}
(
\K
)
$}
;
\draw
(0,0) -- (1.5,0) -- (1.5,-0.75) -- (0, -0.75) -- cycle;
\draw
(0.75,-0.375) node[textstyle, anchor=center]
{$
M
_{
a,b
}
(
\K
)
$}
;
\end{scope}
% Eab
% Eab
\begin{scope}
[yshift=1.5 cm,xshift=3 cm]
\draw
[fill=white]
(0,0) -- (1.5,0) -- (1.5,-0.75) -- (0, -0.75) -- cycle;
\draw
(0.75,-0.375) node[textstyle, anchor=center]
{$
E
_{
a',b'
}
(
\K
)
$}
;
\draw
[fill=white]
(0,0) -- (1.5,0) -- (1.5,-0.75) -- (0, -0.75) -- cycle;
\draw
(0.75,-0.375) node[textstyle, anchor=center]
{$
E
_{
a',b'
}
(
\K
)
$}
;
\end{scope}
% M is a finite assoc group
% M is a finite assoc group
\begin{scope}
[yshift=0 cm,xshift=3 cm]
\draw
[fill=green!20] (0,0) -- (3.25,0) -- (3.25,-0.75) -- (0, -0.75) -- cycle;
\draw
(1.675,-0.375) node[textstyle, anchor=center]
{$
M
_{
a,b
}
(
\K
)
$
is an Assoc. Fin. Grp.
}
;
\draw
[fill=green!20] (0,0) -- (3.25,0) -- (3.25,-0.75) -- (0, -0.75) -- cycle;
\draw
(1.675,-0.375) node[textstyle, anchor=center]
{$
M
_{
a,b
}
(
\K
)
$
is an Assoc. Fin. Grp.
}
;
\end{scope}
% Hypothesis x square is not 2
% Hypothesis x square is not 2
\begin{scope}
[yshift=-1.5 cm,xshift=0 cm]
\draw
[fill=orange!20] (0,0) -- (1.5,0) -- (1.5,-1.25) -- (0, -1.25) -- cycle;
\draw
(0,0) node[textstyle, anchor=north west]
{
\textbf
{
Hyp:
}}
;
\draw
(0.75,-0.375) node[textstyle, anchor=north]
{$
\forall
x
\in
\K
,
$
\\
$
x
^
2
\neq
a
^
2
-
4
$}
;
\draw
[fill=orange!20] (0,0) -- (1.5,0) -- (1.5,-1.25) -- (0, -1.25) -- cycle;
\draw
(0,0) node[textstyle, anchor=north west]
{
\textbf
{
Hyp:
}}
;
\draw
(0.75,-0.375) node[textstyle, anchor=north]
{$
\forall
x
\in
\K
,
$
\\
[.6ex]
$
x
^
2
\neq
a
^
2
-
4
$}
;
\end{scope}
% Final theorem
% Final theorem
\begin{scope}
[yshift=-1.5 cm,xshift=3 cm]
\draw
[fill=green!20] (0,0) -- (3.25,0) -- (3.25,-1.375) -- (0, -1.375) -- cycle;
\draw
(0,0) node[textstyle, anchor=north west]
{
\textbf
{
Thm:
}}
;
\draw
(1.675,-0.375) node[textstyle, anchor=north]
{$
\forall
x
\in
\K
, n
\in
\N
, P
\in
M
_{
a,b
}
(
\K
)
,
$
\\
$
x
=
\chi
_
0
(
P
)
\implies
$
\\
ladder
$
n
$
$
x
$
=
$
\chi
_
0
(
n
\cdot
P
)
$}
;
\draw
[fill=green!20] (0,0) -- (3.25,0) -- (3.25,-1.375) -- (0, -1.375) -- cycle;
\draw
(0,0) node[textstyle, anchor=north west]
{
\textbf
{
Thm:
}}
;
\draw
(1.675,-0.375) node[textstyle, anchor=north]
{$
\forall
x
\in
\K
, n
\in
\N
, P
\in
M
_{
a,b
}
(
\K
)
,
$
\\
[.6ex]
$
x
=
\chi
_
0
(
P
)
\implies
$
\\
[.6ex]
ladder
$
n
$
$
x
$
=
$
\chi
_
0
(
n
\cdot
P
)
$}
;
\end{scope}
\path
[thick, double, ->] (1.5,-0.375) edge [out=0, in=-180] (3,-0.375);
...
...
paper/tikz/highlevel2.tex
View file @
6aef7107
\begin{tikzpicture}
[textstyle/.style=
{
black, anchor= south west, align=center, minimum height=0.45cm, text centered, font=
\
scriptsize
}
]
\begin{tikzpicture}
[textstyle/.style=
{
black, anchor= south west, align=center, minimum height=0.45cm, text centered, font=
\
tiny
}
]
\draw
(6.75,1) node[textstyle, anchor=north east]
{$
p
=
\p
$
\\
$
C
=
M
_{
486662
,
1
}$
\\
$
T
=
M
_{
486662
,
2
}$
\\
}
;
\draw
(6.75,1) node[textstyle, anchor=north east]
{$
p
=
\p
$
\\
[.6ex]
$
C
=
M
_{
486662
,
1
}$
\\
[.6ex]
$
T
=
M
_{
486662
,
2
}$}
;
\begin{scope}
[yshift=1 cm,xshift=-0.5 cm]
\draw
[fill=green!20] (0,0) -- (1.5,0) -- (1.5,-0.75) -- (0, -0.75) -- cycle;
\draw
(0.75,-0.375) node[textstyle, anchor=center]
{$
p
$
is prime
}
;
\draw
[fill=green!20] (0,0) -- (1.5,0) -- (1.5,-0.75) -- (0, -0.75) -- cycle;
\draw
(0.75,-0.375) node[textstyle, anchor=center]
{$
p
$
is prime
}
;
\end{scope}
\begin{scope}
[yshift=-0.25 cm,xshift=-0.5 cm]
\draw
[fill=white]
(0.25,0) -- (1.25,0) -- (1.25,-0.75) -- (0.25, -0.75) -- cycle;
\draw
(0.75,-0.375) node[textstyle, anchor=center]
{$
\F
{
p
}$}
;
\draw
[fill=white]
(0.25,0) -- (1.25,0) -- (1.25,-0.75) -- (0.25, -0.75) -- cycle;
\draw
(0.75,-0.375) node[textstyle, anchor=center]
{$
\F
{
p
}$}
;
\end{scope}
\begin{scope}
[yshift=-1 cm,xshift=1.25 cm]
\draw
[fill=green!20]
(0,0) -- (1.25,0) -- (1.25,-0.75) -- (0, -0.75) -- cycle;
\draw
(0.615,-0.375) node[textstyle, anchor=center]
{$
\forall
x
\in
\F
{
p
}
,
$
\\
$
x
^
2
\neq
2
$}
;
\draw
[fill=green!20]
(0,0) -- (1.25,0) -- (1.25,-0.75) -- (0, -0.75) -- cycle;
\draw
(0.615,-0.375) node[textstyle, anchor=center]
{$
\forall
x
\in
\F
{
p
}
,
$
\\
[.6ex]
$
x
^
2
\neq
2
$}
;
\end{scope}
\begin{scope}
[yshift=-1 cm,xshift=2.625 cm]
\draw
[fill=green!20]
(0,0) -- (1.5,0) -- (1.5,-0.75) -- (0, -0.75) -- cycle;
\draw
(0.75,-0.375) node[textstyle, anchor=center]
{$
\forall
x
\in
\F
{
p
}
,
$
\\
$
x
^
2
\neq
a
^
2
-
4
$}
;
\draw
[fill=green!20]
(0,0) -- (1.5,0) -- (1.5,-0.75) -- (0, -0.75) -- cycle;
\draw
(0.75,-0.375) node[textstyle, anchor=center]
{$
\forall
x
\in
\F
{
p
}
,
$
\\
[.6ex]
$
x
^
2
\neq
a
^
2
-
4
$}
;
\end{scope}
\begin{scope}
[yshift=-1 cm,xshift=4.375 cm]
\draw
[fill=white]
(0,0) -- (1,0) -- (1,-0.75) -- (0, -0.75) -- cycle;
\draw
(0.5,-0.375) node[textstyle, anchor=center]
{$
C
(
\F
{
p
}
)
$}
;
\draw
[fill=white]
(0,0) -- (1,0) -- (1,-0.75) -- (0, -0.75) -- cycle;
\draw
(0.5,-0.375) node[textstyle, anchor=center]
{$
C
(
\F
{
p
}
)
$}
;
\end{scope}
\begin{scope}
[yshift=-1 cm,xshift=6.5 cm]
\draw
[fill=white]
(0,0) -- (1,0) -- (1,-0.75) -- (0, -0.75) -- cycle;
\draw
(0.5,-0.375) node[textstyle, anchor=center]
{$
T
(
\F
{
p
}
)
$}
;
\draw
[fill=white]
(0,0) -- (1,0) -- (1,-0.75) -- (0, -0.75) -- cycle;
\draw
(0.5,-0.375) node[textstyle, anchor=center]
{$
T
(
\F
{
p
}
)
$}
;
\end{scope}
\path
[thick, double, ->] (0.25,0.25) edge [out=-90, in=90] (0.25,-0.25);
...
...
@@ -40,19 +40,19 @@
\path
[thick, double, ->] (7,-0.625) edge [out=-90, in=90] (7,-1);
\begin{scope}
[yshift=-2.5 cm,xshift=1.
2
5 cm]
\draw
[fill=green!20]
(-0.
40
,0) -- (
1.90
,0) -- (
1.90
,-1.25) -- (-0.
42
, -1.25) -- cycle;
\draw
(0.75,0) node[textstyle, anchor=north]
{$
\forall
x
\in
\F
{
p
}
,
$
\\
$
\exists
P
\in
C
(
\F
{
p
}
)
,
$
\\
$
\exists
Q
\in
T
(
\F
{
p
}
)
$
,
\\
$
x
=
\chi
_
0
(
P
)
\vee
x
=
\chi
_
0
(
Q
)
$}
;
\begin{scope}
[yshift=-2.5 cm,xshift=1.
3
5 cm]
\draw
[fill=green!20]
(-0.
53
,0) -- (
2.03
,0) -- (
2.03
,-1.25) -- (-0.
53
, -1.25) -- cycle;
\draw
(0.75,0) node[textstyle, anchor=north]
{$
\forall
x
\in
\F
{
p
}
,
$
\\
[.6ex]
$
\exists
P
\in
C
(
\F
{
p
}
)
,
$
\\
[.6ex]
$
\exists
Q
\in
T
(
\F
{
p
}
)
$
,
\\
[.6ex]
$
x
=
\chi
_
0
(
P
)
\vee
x
=
\chi
_
0
(
Q
)
$}
;
\end{scope}
\begin{scope}
[yshift=-2.5 cm,xshift=4.125 cm]
\draw
[fill=green!20]
(-0.
25
,0) -- (1.7
0
,0) -- (1.7
0
,-1.25) -- (-0.
25
, -1.25) -- cycle;
\draw
(0.75,0) node[textstyle, anchor=north]
{$
\forall
x
\in
\F
{
p
}
,
$
\\
$
\forall
P
\in
C
(
\F
{
p
}
)
,
$
\\
$
x
=
\chi
_
0
(
P
)
\implies
$
\\
lad.
$
n
$
$
x
=
\chi
_
0
(
n
\cdot
P
)
$}
;
\draw
[fill=green!20]
(-0.
3
,0) -- (1.7
8
,0) -- (1.7
8
,-1.25) -- (-0.
3
, -1.25) -- cycle;
\draw
(0.75,0) node[textstyle, anchor=north]
{$
\forall
x
\in
\F
{
p
}
,
$
\\
[.6ex]
$
\forall
P
\in
C
(
\F
{
p
}
)
,
$
\\
[.6ex]
$
x
=
\chi
_
0
(
P
)
\implies
$
\\
[.6ex]
lad.
$
n
$
$
x
=
\chi
_
0
(
n
\cdot
P
)
$}
;
\end{scope}
\begin{scope}
[yshift=-2.5 cm,xshift=6.25 cm]
\draw
[fill=green!20]
(-0.
25
,0) -- (1.7
0
,0) -- (1.7
0
,-1.25) -- (-0.
25
, -1.25) -- cycle;
\draw
(0.75,0) node[textstyle, anchor=north]
{$
\forall
x
\in
\F
{
p
}
,
$
\\
$
\forall
Q
\in
T
(
\F
{
p
}
)
,
$
\\
$
x
=
\chi
_
0
(
Q
)
\implies
$
\\
lad.
$
n
$
$
x
=
\chi
_
0
(
n
\cdot
Q
)
$}
;
\draw
[fill=green!20]
(-0.
3
,0) -- (1.7
8
,0) -- (1.7
8
,-1.25) -- (-0.
3
, -1.25) -- cycle;
\draw
(0.75,0) node[textstyle, anchor=north]
{$
\forall
x
\in
\F
{
p
}
,
$
\\
[.6ex]
$
\forall
Q
\in
T
(
\F
{
p
}
)
,
$
\\
[.6ex]
$
x
=
\chi
_
0
(
Q
)
\implies
$
\\
[.6ex]
lad.
$
n
$
$
x
=
\chi
_
0
(
n
\cdot
Q
)
$}
;
\end{scope}
\path
[thick, double, ->] (1.875,-1.75) edge [out=-90, in=90] (1.875,-2.5);
...
...
@@ -61,13 +61,13 @@
\path
[thick, double, ->] (4.875,-1.75) edge [out=-90, in=90] (4.875,-2.5);
\path
[thick, double, ->] (7,-1.75) edge [out=-90, in=90] (7,-2.5);
% F(p^2)
% F(p^2)
\path
[thick, double, ->] (0.25,-1) edge [out=-90, in=90] (0.25,-2.5);
\begin{scope}
[yshift=-2.5 cm,xshift=-0.5 cm]
\draw
[fill=white]
(0.25,0) -- (1.25,0) -- (1.25,-0.75) -- (0.25, -0.75) -- cycle;
\draw
(0.75,-0.375) node[textstyle, anchor=center]
{$
\F
{
p
^
2
}$}
;
\draw
(0.75,-0.375) node[textstyle, anchor=center]
{$
\F
{
p
^
2
}$}
;
\end{scope}
\path
[thick, double, ->] (0.25,-3.25) edge [out=-90, in=90] (0.25,-5);
...
...
@@ -75,18 +75,18 @@
% C(F(p^2))
\begin{scope}
[yshift=-4.5 cm,xshift=-0.5 cm]
\draw
[fill=white]
(0,0) -- (1.5,0) -- (1.5,-0.75) -- (0, -0.75) -- cycle;
\draw
(0.75,-0.375) node[textstyle, anchor=center]
{$
C
(
\F
{
p
^
2
}
)
$}
;
\draw
[fill=white]
(0,0) -- (1.5,0) -- (1.5,-0.75) -- (0, -0.75) -- cycle;
\draw
(0.75,-0.375) node[textstyle, anchor=center]
{$
C
(
\F
{
p
^
2
}
)
$}
;
\end{scope}
\begin{scope}
[yshift=-4.5 cm,xshift=1.5 cm]
\draw
[fill=green!20]
(0,0) -- (2,0) -- (2,-0.75) -- (0, -0.75) -- cycle;
\draw
(1,-0.375) node[textstyle, anchor=center]
{$
C
(
\F
{
p
}
)
\subset
C
(
\F
{
p
^
2
}
)
$}
;
\draw
[fill=green!20]
(0,0) -- (2,0) -- (2,-0.75) -- (0, -0.75) -- cycle;
\draw
(1,-0.375) node[textstyle, anchor=center]
{$
C
(
\F
{
p
}
)
\subset
C
(
\F
{
p
^
2
}
)
$}
;
\end{scope}
\begin{scope}
[yshift=-5.5 cm,xshift=1.5 cm]
\draw
[fill=green!20]
(0,0) -- (2,0) -- (2,-0.75) -- (0, -0.75) -- cycle;
\draw
(1,-0.375) node[textstyle, anchor=center]
{$
T
(
\F
{
p
}
)
\subset
C
(
\F
{
p
^
2
}
)
$}
;
\draw
[fill=green!20]
(0,0) -- (2,0) -- (2,-0.75) -- (0, -0.75) -- cycle;
\draw
(1,-0.375) node[textstyle, anchor=center]
{$
T
(
\F
{
p
}
)
\subset
C
(
\F