-
Notifications
You must be signed in to change notification settings - Fork 0
/
EverCryptAEAD.html
248 lines (227 loc) · 18.4 KB
/
EverCryptAEAD.html
1
2
3
4
5
6
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
80
81
82
83
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
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
<!DOCTYPE html>
<html class="writer-html4" lang="en" >
<head>
<meta charset="utf-8" />
<meta name="viewport" content="width=device-width, initial-scale=1.0" />
<title>AEAD (EverCrypt_AEAD.h) — HACL* and EverCrypt Manual documentation</title><link rel="stylesheet" href="static/css/theme.css" type="text/css" />
<link rel="stylesheet" href="static/pygments.css" type="text/css" />
<!--[if lt IE 9]>
<script src="static/js/html5shiv.min.js"></script>
<![endif]-->
<script>
var DOCUMENTATION_OPTIONS = {
URL_ROOT:'./',
VERSION:'',
LANGUAGE:'None',
COLLAPSE_INDEX:false,
FILE_SUFFIX:'.html',
HAS_SOURCE: true,
SOURCELINK_SUFFIX: '.txt'
};
</script>
<script src="static/jquery.js"></script>
<script src="static/underscore.js"></script>
<script src="static/doctools.js"></script>
<script src="https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.1/MathJax.js?config=TeX-AMS-MML_HTMLorMML"></script>
<script src="static/js/theme.js"></script>
<link rel="index" title="Index" href="genindex.html" />
<link rel="search" title="Search" href="search.html" />
<link rel="next" title="CTR-mode encryption (EverCrypt_CTR.h)" href="EverCryptCTR.html" />
<link rel="prev" title="CPU autodetection (EverCrypt_AutoConfig2.h)" href="EverCryptAutoConfig.html" />
</head>
<body class="wy-body-for-nav">
<div class="wy-grid-for-nav">
<nav data-toggle="wy-nav-shift" class="wy-nav-side">
<div class="wy-side-scroll">
<div class="wy-side-nav-search" >
<a href="index.html" class="icon icon-home"> HACL* and EverCrypt Manual
</a>
<div role="search">
<form id="rtd-search-form" class="wy-form" action="search.html" method="get">
<input type="text" name="q" placeholder="Search docs" />
<input type="hidden" name="check_keywords" value="yes" />
<input type="hidden" name="area" value="default" />
</form>
</div>
</div><div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="Navigation menu">
<p class="caption"><span class="caption-text">Contents:</span></p>
<ul class="current">
<li class="toctree-l1"><a class="reference internal" href="HaclValeEverCrypt.html">HACL*, Vale, and EverCrypt</a></li>
<li class="toctree-l1"><a class="reference internal" href="Supported.html">List of supported algorithms</a></li>
<li class="toctree-l1"><a class="reference internal" href="Overview.html">Underlying research</a></li>
<li class="toctree-l1"><a class="reference internal" href="Obtaining.html">Using the crypto library</a></li>
<li class="toctree-l1"><a class="reference internal" href="General.html">Digging into the F* source code</a></li>
<li class="toctree-l1"><a class="reference internal" href="HaclDoc.html">HACL APIs</a></li>
<li class="toctree-l1 current"><a class="reference internal" href="EverCryptDoc.html">EverCrypt APIs</a><ul class="current">
<li class="toctree-l2"><a class="reference internal" href="EverCryptAutoConfig.html">CPU autodetection (<code class="docutils literal notranslate"><span class="pre">EverCrypt_AutoConfig2.h</span></code>)</a></li>
<li class="toctree-l2 current"><a class="current reference internal" href="#">AEAD (<code class="docutils literal notranslate"><span class="pre">EverCrypt_AEAD.h</span></code>)</a><ul>
<li class="toctree-l3"><a class="reference internal" href="#state-management">State management</a></li>
<li class="toctree-l3"><a class="reference internal" href="#encryption-and-decryption">Encryption and decryption</a></li>
</ul>
</li>
<li class="toctree-l2"><a class="reference internal" href="EverCryptCTR.html">CTR-mode encryption (<code class="docutils literal notranslate"><span class="pre">EverCrypt_CTR.h</span></code>)</a></li>
<li class="toctree-l2"><a class="reference internal" href="EverCryptHash.html">Hashing (<code class="docutils literal notranslate"><span class="pre">EverCrypt_Hash.h</span></code>)</a></li>
<li class="toctree-l2"><a class="reference internal" href="EverCryptHMAC.html">HMAC (<code class="docutils literal notranslate"><span class="pre">EverCrypt_HMAC.h</span></code>)</a></li>
<li class="toctree-l2"><a class="reference internal" href="EverCryptHKDF.html">HKDF (<code class="docutils literal notranslate"><span class="pre">EverCrypt_HKDF.h</span></code>)</a></li>
<li class="toctree-l2"><a class="reference internal" href="EverCryptDRBG.html">HMAC-DRBG (<code class="docutils literal notranslate"><span class="pre">EverCrypt_DRBG.h</span></code>)</a></li>
<li class="toctree-l2"><a class="reference internal" href="EverCryptNonAgile.html">Non-agile APIs</a></li>
<li class="toctree-l2"><a class="reference internal" href="EverCryptDeprecated.html">Deprecated APIs</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="API.html">Which API to use</a></li>
<li class="toctree-l1"><a class="reference internal" href="Applications.html">Verified Applications</a></li>
</ul>
</div>
</div>
</nav>
<section data-toggle="wy-nav-shift" class="wy-nav-content-wrap"><nav class="wy-nav-top" aria-label="Mobile navigation menu" >
<i data-toggle="wy-nav-top" class="fa fa-bars"></i>
<a href="index.html">HACL* and EverCrypt Manual</a>
</nav>
<div class="wy-nav-content">
<div class="rst-content">
<div role="navigation" aria-label="Page navigation">
<ul class="wy-breadcrumbs">
<li><a href="index.html" class="icon icon-home"></a> »</li>
<li><a href="EverCryptDoc.html">EverCrypt APIs</a> »</li>
<li>AEAD (<code class="docutils literal notranslate"><span class="pre">EverCrypt_AEAD.h</span></code>)</li>
<li class="wy-breadcrumbs-aside">
</li>
</ul>
<hr/>
</div>
<div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article">
<div itemprop="articleBody">
<div class="section" id="aead-evercrypt-aead-h">
<h1>AEAD (<code class="docutils literal notranslate"><span class="pre">EverCrypt_AEAD.h</span></code>)<a class="headerlink" href="#aead-evercrypt-aead-h" title="Permalink to this headline">¶</a></h1>
<p>This API is:</p>
<ul class="simple">
<li><strong>agile</strong></li>
<li><strong>multiplexing</strong>: portable C (Chacha-Poly only); AVX (Chacha-Poly); AVX2
(Chacha-Poly); AESNI + CLMUL (AES128-GCM, AES256-GCM)</li>
<li><strong>stateful</strong></li>
</ul>
<p>Possible values for the agility argument (<code class="docutils literal notranslate"><span class="pre">Hacl_Spec.h</span></code>) :</p>
<div class="highlight-c notranslate"><div class="highlight"><pre><span></span>
<span class="cp">#define Spec_Agile_AEAD_AES128_GCM 0</span>
<span class="cp">#define Spec_Agile_AEAD_AES256_GCM 1</span>
<span class="cp">#define Spec_Agile_AEAD_CHACHA20_POLY1305 2</span>
<span class="cp">#define Spec_Agile_AEAD_AES128_CCM 3</span>
<span class="cp">#define Spec_Agile_AEAD_AES256_CCM 4</span>
<span class="cp">#define Spec_Agile_AEAD_AES128_CCM8 5</span>
<span class="cp">#define Spec_Agile_AEAD_AES256_CCM8 6</span>
</pre></div>
</div>
<p>Supported values for the agility argument: <code class="docutils literal notranslate"><span class="pre">Spec_Agile_AEAD_AES128_GCM</span></code>,
<code class="docutils literal notranslate"><span class="pre">Spec_Agile_AEAD_AES256_GCM</span></code>, <code class="docutils literal notranslate"><span class="pre">Spec_Agile_AEAD_CHACHA20_POLY1305</span></code></p>
<div class="section" id="state-management">
<h2>State management<a class="headerlink" href="#state-management" title="Permalink to this headline">¶</a></h2>
<p>Clients are first expected to allocate persistent state, which performs key
expansion and precomputes internal data for AES-GCM. <code class="docutils literal notranslate"><span class="pre">EverCrypt.AEAD</span></code> supports
IV reduction, meaning that IV lengths must satisfy the <code class="docutils literal notranslate"><span class="pre">iv_length</span></code> predicate
in <code class="docutils literal notranslate"><span class="pre">Spec.Agile.AEAD.fsti</span></code>.</p>
<div class="highlight-c notranslate"><div class="highlight"><pre><span></span>
<span class="n">EverCrypt_Error_error_code</span><span class="w"></span>
<span class="nf">EverCrypt_AEAD_create_in</span><span class="p">(</span><span class="n">Spec_Agile_AEAD_alg</span><span class="w"> </span><span class="n">a</span><span class="p">,</span><span class="w"> </span><span class="n">EverCrypt_AEAD_state_s</span><span class="w"> </span><span class="o">**</span><span class="n">dst</span><span class="p">,</span><span class="w"> </span><span class="kt">uint8_t</span><span class="w"> </span><span class="o">*</span><span class="n">k</span><span class="p">);</span><span class="w"></span>
</pre></div>
</div>
<p>The type <code class="docutils literal notranslate"><span class="pre">EverCrypt_AEAD_state_s</span></code> is a C abstract type which cannot be
allocated by clients, as is it an incomplete struct type. Therefore, the
expected usage for initialization is:</p>
<div class="highlight-c notranslate"><div class="highlight"><pre><span></span><span class="n">EverCrypt_AEAD_state_s</span><span class="w"> </span><span class="o">*</span><span class="n">dst</span><span class="p">;</span><span class="w"></span>
<span class="n">EverCrypt_Error_error</span><span class="w"> </span><span class="n">ret</span><span class="w"> </span><span class="o">=</span><span class="w"></span>
<span class="w"> </span><span class="n">EverCrypt_AEAD_create_in</span><span class="p">(</span><span class="n">Spec_Agile_AEAD_CHACHA20_POLY1305</span><span class="p">,</span><span class="w"> </span><span class="o">&</span><span class="n">dst</span><span class="p">,</span><span class="w"> </span><span class="n">key</span><span class="p">);</span><span class="w"></span>
</pre></div>
</div>
<p>Possible error codes can be determined by looking at the original F* signature
for <code class="docutils literal notranslate"><span class="pre">create_in</span></code>; at the time of writing, the function may return <code class="docutils literal notranslate"><span class="pre">Success</span></code>,
or <code class="docutils literal notranslate"><span class="pre">UnsupportedAlgorithm</span></code>. All other cases are eliminated via the <code class="docutils literal notranslate"><span class="pre">_</span> <span class="pre">-></span>
<span class="pre">False</span></code> in the post-condition.</p>
<p><code class="docutils literal notranslate"><span class="pre">UnsupportedAlgorithm</span></code> may be returned because of an unsupported algorithm
(e.g. AES-CCM) , or because no implementation is available for the target
platform (e.g. AES-GCM without ADX+BMI2).</p>
<p>State <strong>must</strong> be freed via the <code class="docutils literal notranslate"><span class="pre">free</span></code> function:</p>
<div class="highlight-c notranslate"><div class="highlight"><pre><span></span>
<span class="kt">void</span><span class="w"> </span><span class="nf">EverCrypt_AEAD_free</span><span class="p">(</span><span class="n">EverCrypt_AEAD_state_s</span><span class="w"> </span><span class="o">*</span><span class="n">s</span><span class="p">);</span><span class="w"></span>
</pre></div>
</div>
</div>
<div class="section" id="encryption-and-decryption">
<h2>Encryption and decryption<a class="headerlink" href="#encryption-and-decryption" title="Permalink to this headline">¶</a></h2>
<p>Both encryption and decryption take a piece of state which holds the key; a
piece of state may be reused as many times as desired.</p>
<p>Encryption has a substantial amount of preconditions; see <code class="docutils literal notranslate"><span class="pre">encrypt_pre</span></code> in
<code class="docutils literal notranslate"><span class="pre">EverCrypt.AEAD.fsti</span></code>, and <a class="reference internal" href="General.html#reading-preconditions"><span class="std std-ref">Reading F* preconditions</span></a> for a primer on
deciphering F* code.</p>
<p>At the time of writing, <code class="docutils literal notranslate"><span class="pre">encrypt</span></code> may return either <code class="docutils literal notranslate"><span class="pre">Success</span></code> or
<code class="docutils literal notranslate"><span class="pre">InvalidKey</span></code>. The latter is returned if and only if the <code class="docutils literal notranslate"><span class="pre">s</span></code> parameter is
<code class="docutils literal notranslate"><span class="pre">NULL</span></code>.</p>
<div class="highlight-c notranslate"><div class="highlight"><pre><span></span>
<span class="n">EverCrypt_Error_error_code</span><span class="w"></span>
<span class="nf">EverCrypt_AEAD_encrypt</span><span class="p">(</span><span class="w"></span>
<span class="w"> </span><span class="n">EverCrypt_AEAD_state_s</span><span class="w"> </span><span class="o">*</span><span class="n">s</span><span class="p">,</span><span class="w"></span>
<span class="w"> </span><span class="kt">uint8_t</span><span class="w"> </span><span class="o">*</span><span class="n">iv</span><span class="p">,</span><span class="w"></span>
<span class="w"> </span><span class="kt">uint32_t</span><span class="w"> </span><span class="n">iv_len</span><span class="p">,</span><span class="w"></span>
<span class="w"> </span><span class="kt">uint8_t</span><span class="w"> </span><span class="o">*</span><span class="n">ad</span><span class="p">,</span><span class="w"></span>
<span class="w"> </span><span class="kt">uint32_t</span><span class="w"> </span><span class="n">ad_len</span><span class="p">,</span><span class="w"></span>
<span class="w"> </span><span class="kt">uint8_t</span><span class="w"> </span><span class="o">*</span><span class="n">plain</span><span class="p">,</span><span class="w"></span>
<span class="w"> </span><span class="kt">uint32_t</span><span class="w"> </span><span class="n">plain_len</span><span class="p">,</span><span class="w"></span>
<span class="w"> </span><span class="kt">uint8_t</span><span class="w"> </span><span class="o">*</span><span class="n">cipher</span><span class="p">,</span><span class="w"></span>
<span class="w"> </span><span class="kt">uint8_t</span><span class="w"> </span><span class="o">*</span><span class="n">tag</span><span class="w"></span>
<span class="p">);</span><span class="w"></span>
</pre></div>
</div>
<div class="admonition note">
<p class="first admonition-title">Note</p>
<p class="last">There is no length parameter for the tag; looking at the source
<code class="docutils literal notranslate"><span class="pre">EverCrypt.AEAD.fsti</span></code>, one can see a precondition of the form <code class="docutils literal notranslate"><span class="pre">B.length</span> <span class="pre">tag</span>
<span class="pre">=</span> <span class="pre">tag_length</span> <span class="pre">a</span></code>, i.e. the length of the <code class="docutils literal notranslate"><span class="pre">tag</span></code> array must be of a suitable
length for the algorithm <code class="docutils literal notranslate"><span class="pre">a</span></code>. See <code class="docutils literal notranslate"><span class="pre">Spec.Agile.AEAD.fsti</span></code> for the
definition of <code class="docutils literal notranslate"><span class="pre">tag_length</span></code>. <strong>Unverified clients are strongly encouraged
to perform a run-time check!</strong></p>
</div>
<div class="highlight-c notranslate"><div class="highlight"><pre><span></span>
<span class="n">EverCrypt_Error_error_code</span><span class="w"></span>
<span class="nf">EverCrypt_AEAD_decrypt</span><span class="p">(</span><span class="w"></span>
<span class="w"> </span><span class="n">EverCrypt_AEAD_state_s</span><span class="w"> </span><span class="o">*</span><span class="n">s</span><span class="p">,</span><span class="w"></span>
<span class="w"> </span><span class="kt">uint8_t</span><span class="w"> </span><span class="o">*</span><span class="n">iv</span><span class="p">,</span><span class="w"></span>
<span class="w"> </span><span class="kt">uint32_t</span><span class="w"> </span><span class="n">iv_len</span><span class="p">,</span><span class="w"></span>
<span class="w"> </span><span class="kt">uint8_t</span><span class="w"> </span><span class="o">*</span><span class="n">ad</span><span class="p">,</span><span class="w"></span>
<span class="w"> </span><span class="kt">uint32_t</span><span class="w"> </span><span class="n">ad_len</span><span class="p">,</span><span class="w"></span>
<span class="w"> </span><span class="kt">uint8_t</span><span class="w"> </span><span class="o">*</span><span class="n">cipher</span><span class="p">,</span><span class="w"></span>
<span class="w"> </span><span class="kt">uint32_t</span><span class="w"> </span><span class="n">cipher_len</span><span class="p">,</span><span class="w"></span>
<span class="w"> </span><span class="kt">uint8_t</span><span class="w"> </span><span class="o">*</span><span class="n">tag</span><span class="p">,</span><span class="w"></span>
<span class="w"> </span><span class="kt">uint8_t</span><span class="w"> </span><span class="o">*</span><span class="n">dst</span><span class="w"></span>
<span class="p">);</span><span class="w"></span>
</pre></div>
</div>
</div>
</div>
</div>
</div>
<a href="https://github.com/project-everest/hacl-star/">
<img style="position: absolute; top: 0; right: 0; border: 0;" src="https://s3.amazonaws.com/github/ribbons/forkme_right_darkblue_121621.png" alt="Fork me on GitHub">
</a>
<footer><div class="rst-footer-buttons" role="navigation" aria-label="Footer">
<a href="EverCryptAutoConfig.html" class="btn btn-neutral float-left" title="CPU autodetection (EverCrypt_AutoConfig2.h)" accesskey="p" rel="prev"><span class="fa fa-arrow-circle-left" aria-hidden="true"></span> Previous</a>
<a href="EverCryptCTR.html" class="btn btn-neutral float-right" title="CTR-mode encryption (EverCrypt_CTR.h)" accesskey="n" rel="next">Next <span class="fa fa-arrow-circle-right" aria-hidden="true"></span></a>
</div>
<hr/>
<div role="contentinfo">
<p>© Copyright 2019, INRIA, Microsoft Research, CMU.</p>
</div>
Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
<a href="https://github.com/readthedocs/sphinx_rtd_theme">theme</a>
provided by <a href="https://readthedocs.org">Read the Docs</a>.
</footer>
</div>
</div>
</section>
</div>
<script>
jQuery(function () {
SphinxRtdTheme.Navigation.enable(true);
});
</script>
</body>
</html>