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
93aef6f8
Commit
93aef6f8
authored
Jan 22, 2021
by
Peter Schwabe
Browse files
Small edits
parent
ac359637
Changes
1
Hide whitespace changes
Inline
Side-by-side
paper/rfc.tex
View file @
93aef6f8
...
...
@@ -91,8 +91,8 @@ the RFC uses an additional variable to decide whether a conditional swap
is required or not.
Later in our proof we use a simpler description of the ladder
(
\coqe
{
montgomery
_
rec
}
)
,
which strictly follows
\aref
{
alg:montgomery-ladder
}
,
and prove those
ladder
s equivalent.
(
\coqe
{
montgomery
_
rec
}
) which strictly follows
\aref
{
alg:montgomery-ladder
}
and prove those
description
s equivalent.
RFC 7748 describes the calculations done in X25519 as follows:
\emph
{
``To implement the X25519(k, u) [...] functions (where k is
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a 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