Skip to content

Commit 626d38c

Browse files
committed
Desktop241226v1
1 parent 8ce9ffd commit 626d38c

File tree

16 files changed

+527
-5
lines changed

16 files changed

+527
-5
lines changed
File renamed without changes.
File renamed without changes.
File renamed without changes.

doc/easycrypt-aes/codes/NbAESEnc.jazz

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
/* Nonce-based symmetric encryption for 16-byte messages
2+
using AES as a PRF */
3+
4+
/* We use cpp to manage modules in Jasmin */
5+
#include "../aeslib/aes.jazz"
6+
7+
/* We make xor into a function, but this costs nothing
8+
because Jasmin compiler does not include inlining
9+
moves (warning issued o/w). */
10+
inline fn xor(reg u128 a, reg u128 b) -> reg u128 {
11+
reg u128 r;
12+
r = a^b;
13+
return r;
14+
}
15+
16+
/* These functions can be called from C for testing. */
17+
18+
export fn enc(reg u128 k, reg u128 n, reg u128 p) -> reg u128 {
19+
reg u128 mask,c;
20+
mask = aes(k,n);
21+
c = xor(mask,p);
22+
return(c);
23+
}
24+
25+
export fn dec(reg u128 k, reg u128 n, reg u128 c) -> reg u128 {
26+
reg u128 mask,p;
27+
mask = aes(k,n);
28+
p = xor(mask,c);
29+
return(p);
30+
}
40.9 KB
Binary file not shown.

doc/easycrypt-aes/cse-easycrypt-aes.tex

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -91,9 +91,21 @@ \subsection*{Changelog}
9191
\pagenumbering{arabic}
9292

9393
\tableofcontents
94+
\newpage
95+
\section{Preliminaries}
96+
\input{sections/prelimnaries}
97+
9498
\newpage
9599
\section{Block Cipher}
96100
\input{sections/block_cipher}
101+
102+
\newpage
103+
\section{Machine-checked Proofs for AES}
104+
\input{sections/machine-checked-proofs-aes}
105+
\newpage
106+
\section{Tutorials}
107+
\input{sections/tutorial}
108+
97109
%
98110
%\newpage
99111
%\section{Digital Signature Scheme: ALTEQ}
@@ -106,6 +118,12 @@ \section{Block Cipher}
106118
%\newpage
107119
\vfill
108120
\begin{thebibliography}{9}\large
121+
\bibitem{Introduction_to_Modern_Cryptography}
122+
Jonathan, Katz. \textit{Introduction to Modern Cryptography, Second Edition}., n.d.
123+
\bibitem{Cryptography_Made_Simple}
124+
Smart, Nigel P. \textit{Cryptography Made Simple. Information Security and Cryptography}. Cham: Springer International Publishing, 2016. https://doi.org/10.1007/978-3-319-21936-3.
125+
126+
109127
% \bibitem{alteq_signature_scheme}
110128
% Bläser, Markus, Dung Hoang Duong, Anand Kumar Narayanan, Thomas Plantard, Youming Qiao, Arnaud Sipasseuth, and Gang Tang. \textit{The ALTEQ Signature Scheme: Algorithm Specifications and Supporting Documentation.} Version 1.1.2, March 2024. Saarland University, University of Technology Sydney, University of Wollongong, SandboxAQ, Nokia Bell Labs, and KDDI Research, Inc.
111129
% \bibitem{crypto_theory_and_practice}

0 commit comments

Comments
 (0)