snapkitty
formal-verification
lean4
ahmad-foundations / papers /aes-cryptanalysis /aes_cryptanalysis.log
SNAPKITTYWEST's picture
push from SNAPKITTYWEST/ahmad-foundations
a32e94f verified
Raw History Blame Contribute Delete
34.9 kB
This is pdfTeX, Version 3.141592653-2.6-1.40.29 (MiKTeX 26.5) (preloaded format=pdflatex 2026.7.14) 20 AUG 2026 17:24
entering extended mode
restricted \write18 enabled.
%&-line parsing enabled.
**./aes_cryptanalysis.tex
(aes_cryptanalysis.tex
LaTeX2e <2026-06-01>
L3 programming layer <2026-06-18>
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/base\article.cls
Document Class: article 2025/01/22 v1.4n Standard LaTeX document class
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/base\size11.clo
File: size11.clo 2025/01/22 v1.4n Standard LaTeX file (size option)
)
\c@part=\count276
\c@section=\count277
\c@subsection=\count278
\c@subsubsection=\count279
\c@paragraph=\count280
\c@subparagraph=\count281
\c@figure=\count282
\c@table=\count283
\abovecaptionskip=\skip49
\belowcaptionskip=\skip50
\bibindent=\dimen150
)
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/geometry\geometry.sty
Package: geometry 2026/03/07 v6.0 Page Geometry
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/graphics\keyval.sty
Package: keyval 2026-05-17 v1.15 key=value parser (DPC)
\KV@toks@=\toks17
)
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/generic/iftex\ifvtex.sty
Package: ifvtex 2019/10/25 v1.7 ifvtex legacy package. Use iftex instead.
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/generic/iftex\iftex.sty
Package: iftex 2024/12/12 v1.0g TeX engine tests
))
\Gm@cnth=\count284
\Gm@cntv=\count285
\c@Gm@tempcnt=\count286
\Gm@bindingoffset=\dimen151
\Gm@wd@mp=\dimen152
\Gm@odd@mp=\dimen153
\Gm@even@mp=\dimen154
\Gm@layoutwidth=\dimen155
\Gm@layoutheight=\dimen156
\Gm@layouthoffset=\dimen157
\Gm@layoutvoffset=\dimen158
\Gm@dimlist=\toks18
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/geometry\geometry.cfg))
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/amsmath\amsmath.sty
Package: amsmath 2026/05/19 v2.18d AMS math features
\@mathmargin=\skip51
For additional information on amsmath, use the `?' option.
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/amsmath\amstext.sty
Package: amstext 2024/11/17 v2.01 AMS text
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/amsmath\amsgen.sty
File: amsgen.sty 1999/11/30 v2.0 generic functions
\@emptytoks=\toks19
\ex@=\dimen159
))
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/amsmath\amsbsy.sty
Package: amsbsy 1999/11/29 v1.2d Bold Symbols
\pmbraise@=\dimen160
)
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/amsmath\amsopn.sty
Package: amsopn 2022/04/08 v2.04 operator names
)
\inf@bad=\count287
LaTeX Info: Redefining \frac on input line 233.
\uproot@=\count288
\leftroot@=\count289
LaTeX Info: Redefining \overline on input line 398.
LaTeX Info: Redefining \colon on input line 409.
\classnum@=\count290
\DOTSCASE@=\count291
LaTeX Info: Redefining \ldots on input line 495.
LaTeX Info: Redefining \dots on input line 498.
LaTeX Info: Redefining \cdots on input line 619.
\Mathstrutbox@=\box53
\strutbox@=\box54
LaTeX Info: Redefining \big on input line 721.
LaTeX Info: Redefining \Big on input line 722.
LaTeX Info: Redefining \bigg on input line 723.
LaTeX Info: Redefining \Bigg on input line 724.
\big@size=\dimen161
LaTeX Font Info: Redeclaring font encoding OML on input line 742.
LaTeX Font Info: Redeclaring font encoding OMS on input line 743.
\macc@depth=\count292
LaTeX Info: Redefining \bmod on input line 904.
LaTeX Info: Redefining \pmod on input line 909.
LaTeX Info: Redefining \smash on input line 939.
LaTeX Info: Redefining \relbar on input line 969.
LaTeX Info: Redefining \Relbar on input line 970.
\c@MaxMatrixCols=\count293
\dotsspace@=\muskip17
\c@parentequation=\count294
\dspbrk@lvl=\count295
\tag@help=\toks20
\row@=\count296
\column@=\count297
\maxfields@=\count298
\andhelp@=\toks21
\eqnshift@=\dimen162
\alignsep@=\dimen163
\tagshift@=\dimen164
\tagwidth@=\dimen165
\totwidth@=\dimen166
\lineht@=\dimen167
\@envbody=\toks22
\multlinegap=\skip52
\multlinetaggap=\skip53
\mathdisplay@stack=\toks23
LaTeX Info: Redefining \[ on input line 2965.
LaTeX Info: Redefining \] on input line 2966.
)
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/amsfonts\amssymb.sty
Package: amssymb 2013/01/14 v3.01 AMS font symbols
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/amsfonts\amsfonts.sty
Package: amsfonts 2013/01/14 v3.01 Basic AMSFonts support
\symAMSa=\mathgroup4
\symAMSb=\mathgroup5
LaTeX Font Info: Redeclaring math symbol \hbar on input line 98.
LaTeX Font Info: Overwriting math alphabet `\mathfrak' in version `bold'
(Font) U/euf/m/n --> U/euf/b/n on input line 106.
)) (C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/amscls\amsthm.sty
Package: amsthm 2020/05/29 v2.20.6
\thm@style=\toks24
\thm@bodyfont=\toks25
\thm@headfont=\toks26
\thm@notefont=\toks27
\thm@headpunct=\toks28
\thm@preskip=\skip54
\thm@postskip=\skip55
\thm@headsep=\skip56
\dth@everypar=\toks29
)
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/mathtools\mathtools.sty
Package: mathtools 2024/10/04 v1.31 mathematical typesetting tools
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/tools\calc.sty
Package: calc 2025/03/01 v4.3b Infix arithmetic (KKT,FJ)
\calc@Acount=\count299
\calc@Bcount=\count300
\calc@Adimen=\dimen168
\calc@Bdimen=\dimen169
\calc@Askip=\skip57
\calc@Bskip=\skip58
LaTeX Info: Redefining \setlength on input line 86.
LaTeX Info: Redefining \addtolength on input line 87.
\calc@Ccount=\count301
\calc@Cskip=\skip59
)
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/mathtools\mhsetup.sty
Package: mhsetup 2021/03/18 v1.4 programming setup (MH)
)
\g_MT_multlinerow_int=\count302
\l_MT_multwidth_dim=\dimen170
\origjot=\skip60
\l_MT_shortvdotswithinadjustabove_dim=\dimen171
\l_MT_shortvdotswithinadjustbelow_dim=\dimen172
\l_MT_above_intertext_sep=\dimen173
\l_MT_below_intertext_sep=\dimen174
\l_MT_above_shortintertext_sep=\dimen175
\l_MT_below_shortintertext_sep=\dimen176
\xmathstrut@box=\box55
\xmathstrut@dim=\dimen177
) (C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/base\fontenc.sty
Package: fontenc 2025/07/18 v2.1d Standard LaTeX package
)
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/base\inputenc.sty
Package: inputenc 2024/02/08 v1.3d Input encoding file
\inpenc@prehook=\toks30
\inpenc@posthook=\toks31
)
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/microtype\microtype.sty
Package: microtype 2026/03/01 v3.2d Micro-typographical refinements (RS)
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/etoolbox\etoolbox.sty
Package: etoolbox 2025/10/02 v2.5m e-TeX tools for LaTeX (JAW)
\etb@tempcnta=\count303
)
\MT@toks=\toks32
\MT@tempbox=\box56
\MT@count=\count304
LaTeX Info: Redefining \noprotrusionifhmode on input line 1084.
LaTeX Info: Redefining \leftprotrusion on input line 1085.
\MT@prot@toks=\toks33
LaTeX Info: Redefining \rightprotrusion on input line 1104.
LaTeX Info: Redefining \textls on input line 1449.
\MT@outer@kern=\dimen178
LaTeX Info: Redefining \microtypecontext on input line 2053.
LaTeX Info: Redefining \textmicrotypecontext on input line 2070.
\MT@listname@count=\count305
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/microtype\microtype-pdf
tex.def
File: microtype-pdftex.def 2026/03/01 v3.2d Definitions specific to pdftex (RS)
LaTeX Info: Redefining \lsstyle on input line 944.
LaTeX Info: Redefining \lslig on input line 944.
\MT@outer@space=\skip61
)
Package microtype Info: Loading configuration file microtype.cfg.
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/microtype\microtype.cfg
File: microtype.cfg 2026/03/01 v3.2d microtype main configuration file (RS)
)
LaTeX Info: Redefining \microtypesetup on input line 3065.
)
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/hyperref\hyperref.sty
Package: hyperref 2026-06-17 v7.01r Hypertext links for LaTeX
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/kvsetkeys\kvsetkeys.sty
Package: kvsetkeys 2022-10-05 v1.19 Key value parser (HO)
)
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/generic/kvdefinekeys\kvdefine
keys.sty
Package: kvdefinekeys 2019-12-19 v1.6 Define keys (HO)
)
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/generic/pdfescape\pdfescape.s
ty
Package: pdfescape 2019/12/09 v1.15 Implements pdfTeX's escape features (HO)
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/generic/ltxcmds\ltxcmds.sty
Package: ltxcmds 2023-12-04 v1.26 LaTeX kernel commands for general use (HO)
)
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/generic/pdftexcmds\pdftexcmds
.sty
Package: pdftexcmds 2020-06-27 v0.33 Utility functions of pdfTeX for LuaTeX (HO
)
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/generic/infwarerr\infwarerr.s
ty
Package: infwarerr 2019/12/03 v1.5 Providing info/warning/error messages (HO)
)
Package pdftexcmds Info: \pdf@primitive is available.
Package pdftexcmds Info: \pdf@ifprimitive is available.
Package pdftexcmds Info: \pdfdraftmode found.
))
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/hycolor\hycolor.sty
Package: hycolor 2020-01-27 v1.10 Color options for hyperref/bookmark (HO)
)
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/hyperref\nameref.sty
Package: nameref 2026-01-29 v2.58 Cross-referencing by name of section
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/refcount\refcount.sty
Package: refcount 2019/12/15 v3.6 Data extraction from label references (HO)
)
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/generic/gettitlestring\gettit
lestring.sty
Package: gettitlestring 2019/12/15 v1.6 Cleanup title references (HO)
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/kvoptions\kvoptions.sty
Package: kvoptions 2022-06-15 v3.15 Key value format for package options (HO)
))
\c@section@level=\count306
)
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/generic/stringenc\stringenc.s
ty
Package: stringenc 2019/11/29 v1.12 Convert strings between diff. encodings (HO
)
)
\@linkdim=\dimen179
\Hy@linkcounter=\count307
\Hy@pagecounter=\count308
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/hyperref\pd1enc.def
File: pd1enc.def 2026-06-17 v7.01r Hyperref: PDFDocEncoding definition (HO)
Now handling font encoding PD1 ...
... no UTF-8 mapping file for font encoding PD1
) (C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/generic/intcalc\intcalc.sty
Package: intcalc 2019/12/15 v1.3 Expandable calculations with integers (HO)
)
\Hy@SavedSpaceFactor=\count309
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/hyperref\puenc.def
File: puenc.def 2026-06-17 v7.01r Hyperref: PDF Unicode definition (HO)
Now handling font encoding PU ...
... no UTF-8 mapping file for font encoding PU
)
Package hyperref Info: Hyper figures OFF on input line 4199.
Package hyperref Info: Link nesting OFF on input line 4204.
Package hyperref Info: Hyper index ON on input line 4207.
Package hyperref Info: Plain pages OFF on input line 4214.
Package hyperref Info: Backreferencing OFF on input line 4219.
Package hyperref Info: Implicit mode ON; LaTeX internals redefined.
Package hyperref Info: Bookmarks ON on input line 4466.
\c@Hy@tempcnt=\count310
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/url\url.sty
\Urlmuskip=\muskip18
Package: url 2013/09/16 ver 3.4 Verb mode for urls, etc.
)
LaTeX Info: Redefining \url on input line 4805.
\XeTeXLinkMargin=\dimen180
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/generic/bitset\bitset.sty
Package: bitset 2019/12/09 v1.3 Handle bit-vector datatype (HO)
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/generic/bigintcalc\bigintcalc
.sty
Package: bigintcalc 2019/12/15 v1.5 Expandable calculations on big integers (HO
)
))
\Fld@menulength=\count311
\Field@Width=\dimen181
\Fld@charsize=\dimen182
Package hyperref Info: Hyper figures OFF on input line 6091.
Package hyperref Info: Link nesting OFF on input line 6096.
Package hyperref Info: Hyper index ON on input line 6099.
Package hyperref Info: backreferencing OFF on input line 6106.
Package hyperref Info: Link coloring OFF on input line 6111.
Package hyperref Info: Link coloring with OCG OFF on input line 6116.
Package hyperref Info: PDF/A mode OFF on input line 6121.
\Hy@abspage=\count312
\c@Item=\count313
\c@Hfootnote=\count314
)
Package hyperref Info: Driver (autodetected): hpdftex.
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/hyperref\hpdftex.def
File: hpdftex.def 2026-06-17 v7.01r Hyperref driver for pdfTeX
\Fld@listcount=\count315
\c@bookmark@seq@number=\count316
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/rerunfilecheck\rerunfil
echeck.sty
Package: rerunfilecheck 2025-06-21 v1.11 Rerun checks for auxiliary files (HO)
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/generic/uniquecounter\uniquec
ounter.sty
Package: uniquecounter 2019/12/15 v1.4 Provide unlimited unique counter (HO)
)
Package uniquecounter Info: New unique counter `rerunfilecheck' on input line 2
84.
)
\Hy@SectionHShift=\skip62
)
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/booktabs\booktabs.sty
Package: booktabs 2020/01/12 v1.61803398 Publication quality tables
\heavyrulewidth=\dimen183
\lightrulewidth=\dimen184
\cmidrulewidth=\dimen185
\belowrulesep=\dimen186
\belowbottomsep=\dimen187
\aboverulesep=\dimen188
\abovetopsep=\dimen189
\cmidrulesep=\dimen190
\cmidrulekern=\dimen191
\defaultaddspace=\dimen192
\@cmidla=\count317
\@cmidlb=\count318
\@aboverulesep=\dimen193
\@belowrulesep=\dimen194
\@thisruleclass=\count319
\@lastruleclass=\count320
\@thisrulewidth=\dimen195
)
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/enumitem\enumitem.sty
Package: enumitem 2025/02/06 v3.11 Customized lists
\labelindent=\skip63
\enit@outerparindent=\dimen196
\enit@toks=\toks34
\enit@inbox=\box57
\enit@count@id=\count321
\enitdp@description=\count322
)
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/xcolor\xcolor.sty
Package: xcolor 2024/09/29 v3.02 LaTeX color extensions (UK)
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/graphics-cfg\color.cfg
File: color.cfg 2016/01/02 v1.6 sample color configuration
)
Package xcolor Info: Driver file: pdftex.def on input line 274.
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/graphics-def\pdftex.def
File: pdftex.def 2025/09/29 v1.2d Graphics/color driver for pdftex
)
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/graphics\mathcolor.ltx)
Package xcolor Info: Model `cmy' substituted by `cmy0' on input line 1349.
Package xcolor Info: Model `hsb' substituted by `rgb' on input line 1353.
Package xcolor Info: Model `RGB' extended on input line 1365.
Package xcolor Info: Model `HTML' substituted by `rgb' on input line 1367.
Package xcolor Info: Model `Hsb' substituted by `hsb' on input line 1368.
Package xcolor Info: Model `tHsb' substituted by `hsb' on input line 1369.
Package xcolor Info: Model `HSB' substituted by `hsb' on input line 1370.
Package xcolor Info: Model `Gray' substituted by `gray' on input line 1371.
Package xcolor Info: Model `wave' substituted by `hsb' on input line 1372.
) (C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/listings\listings.sty
\lst@mode=\count323
\lst@gtempboxa=\box58
\lst@token=\toks35
\lst@length=\count324
\lst@currlwidth=\dimen197
\lst@column=\count325
\lst@pos=\count326
\lst@lostspace=\dimen198
\lst@width=\dimen199
\lst@newlines=\count327
\lst@lineno=\count328
\lst@maxwidth=\dimen256
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/listings\lstpatch.sty
File: lstpatch.sty 2025/11/14 1.11b (Carsten Heinz)
)
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/listings\lstmisc.sty
File: lstmisc.sty 2025/11/14 1.11b (Carsten Heinz)
\c@lstnumber=\count329
\lst@skipnumbers=\count330
\lst@framebox=\box59
)
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/listings\listings.cfg
File: listings.cfg 2025/11/14 1.11b listings configuration
))
Package: listings 2025/11/14 1.11b (Carsten Heinz)
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/mdframed\mdframed.sty
Package: mdframed 2013/07/01 1.9b: mdframed
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/l3packages/xparse\xpars
e.sty
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/l3kernel\expl3.sty
Package: expl3 2026-06-18 L3 programming layer (loader)
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/l3backend\l3backend-pdf
tex.def
File: l3backend-pdftex.def 2026-02-18 L3 backend support: PDF output (pdfTeX)
\l__color_backend_stack_int=\count331
))
Package: xparse 2025-10-09 L3 Experimental document command parser
)
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/zref\zref-abspage.sty
Package: zref-abspage 2026-03-07 v2.37 Module abspage for zref (HO)
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/zref\zref-base.sty
Package: zref-base 2026-03-07 v2.37 Module base for zref (HO)
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/generic/etexcmds\etexcmds.sty
Package: etexcmds 2019/12/15 v1.7 Avoid name clashes with e-TeX commands (HO)
) (C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/auxhook\auxhook.sty
Package: auxhook 2019-12-17 v1.6 Hooks for auxiliary files (HO)
)
Package zref Info: New property list: main on input line 767.
Package zref Info: New property: default on input line 768.
Package zref Info: New property: page on input line 769.
)
\c@abspage=\count332
Package zref Info: New property: abspage on input line 67.
)
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/needspace\needspace.sty
Package: needspace 2025/03/13 v1.3e reserve vertical space
)
\mdf@templength=\skip64
\c@mdf@globalstyle@cnt=\count333
\mdf@skipabove@length=\skip65
\mdf@skipbelow@length=\skip66
\mdf@leftmargin@length=\skip67
\mdf@rightmargin@length=\skip68
\mdf@innerleftmargin@length=\skip69
\mdf@innerrightmargin@length=\skip70
\mdf@innertopmargin@length=\skip71
\mdf@innerbottommargin@length=\skip72
\mdf@splittopskip@length=\skip73
\mdf@splitbottomskip@length=\skip74
\mdf@outermargin@length=\skip75
\mdf@innermargin@length=\skip76
\mdf@linewidth@length=\skip77
\mdf@innerlinewidth@length=\skip78
\mdf@middlelinewidth@length=\skip79
\mdf@outerlinewidth@length=\skip80
\mdf@roundcorner@length=\skip81
\mdf@footenotedistance@length=\skip82
\mdf@userdefinedwidth@length=\skip83
\mdf@needspace@length=\skip84
\mdf@frametitleaboveskip@length=\skip85
\mdf@frametitlebelowskip@length=\skip86
\mdf@frametitlerulewidth@length=\skip87
\mdf@frametitleleftmargin@length=\skip88
\mdf@frametitlerightmargin@length=\skip89
\mdf@shadowsize@length=\skip90
\mdf@extratopheight@length=\skip91
\mdf@subtitleabovelinewidth@length=\skip92
\mdf@subtitlebelowlinewidth@length=\skip93
\mdf@subtitleaboveskip@length=\skip94
\mdf@subtitlebelowskip@length=\skip95
\mdf@subtitleinneraboveskip@length=\skip96
\mdf@subtitleinnerbelowskip@length=\skip97
\mdf@subsubtitleabovelinewidth@length=\skip98
\mdf@subsubtitlebelowlinewidth@length=\skip99
\mdf@subsubtitleaboveskip@length=\skip100
\mdf@subsubtitlebelowskip@length=\skip101
\mdf@subsubtitleinneraboveskip@length=\skip102
\mdf@subsubtitleinnerbelowskip@length=\skip103
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/mdframed\md-frame-0.mdf
File: md-frame-0.mdf 2013/07/01\ 1.9b: md-frame-0
)
\mdf@frametitlebox=\box60
\mdf@footnotebox=\box61
\mdf@splitbox@one=\box62
\mdf@splitbox@two=\box63
\mdf@splitbox@save=\box64
\mdfsplitboxwidth=\skip104
\mdfsplitboxtotalwidth=\skip105
\mdfsplitboxheight=\skip106
\mdfsplitboxdepth=\skip107
\mdfsplitboxtotalheight=\skip108
\mdfframetitleboxwidth=\skip109
\mdfframetitleboxtotalwidth=\skip110
\mdfframetitleboxheight=\skip111
\mdfframetitleboxdepth=\skip112
\mdfframetitleboxtotalheight=\skip113
\mdffootnoteboxwidth=\skip114
\mdffootnoteboxtotalwidth=\skip115
\mdffootnoteboxheight=\skip116
\mdffootnoteboxdepth=\skip117
\mdffootnoteboxtotalheight=\skip118
\mdftotallinewidth=\skip119
\mdfboundingboxwidth=\skip120
\mdfboundingboxtotalwidth=\skip121
\mdfboundingboxheight=\skip122
\mdfboundingboxdepth=\skip123
\mdfboundingboxtotalheight=\skip124
\mdf@freevspace@length=\skip125
\mdf@horizontalwidthofbox@length=\skip126
\mdf@verticalmarginwhole@length=\skip127
\mdf@horizontalspaceofbox=\skip128
\mdfsubtitleheight=\skip129
\mdfsubsubtitleheight=\skip130
\c@mdfcountframes=\count334
****** mdframed patching \endmdf@trivlist
****** -- success******
\mdf@envdepth=\count335
\c@mdf@env@i=\count336
\c@mdf@env@ii=\count337
\c@mdf@zref@counter=\count338
Package zref Info: New property: mdf@pagevalue on input line 895.
) (C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/cite\cite.sty
LaTeX Info: Redefining \cite on input line 302.
LaTeX Info: Redefining \nocite on input line 332.
Package: cite 2015/02/27 v 5.5
)
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/preprint\authblk.sty
Package: authblk 2001/02/27 1.3 (PWD)
\affilsep=\skip131
\@affilsep=\skip132
\c@Maxaffil=\count339
\c@authors=\count340
\c@affil=\count341
)
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/tools\array.sty
Package: array 2026/02/24 v2.7b Tabular extension package (FMi)
\col@sep=\dimen257
\ar@mcellbox=\box65
\extrarowheight=\dimen258
\NC@list=\toks36
\extratabsurround=\skip133
\backup@length=\skip134
\ar@cellbox=\box66
)
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/multirow\multirow.sty
Package: multirow 2024/11/12 v2.9 Span multiple rows of a table
\multirow@colwidth=\skip135
\multirow@cntb=\count342
\multirow@dima=\skip136
\bigstrutjot=\dimen259
)
Package hyperref Info: Option `colorlinks' set `true' on input line 18.
\c@theorem=\count343
(aes_cryptanalysis.aux)
\openout1 = `aes_cryptanalysis.aux'.
LaTeX Font Info: Checking defaults for OML/cmm/m/it on input line 55.
LaTeX Font Info: ... okay on input line 55.
LaTeX Font Info: Checking defaults for OMS/cmsy/m/n on input line 55.
LaTeX Font Info: ... okay on input line 55.
LaTeX Font Info: Checking defaults for OT1/cmr/m/n on input line 55.
LaTeX Font Info: ... okay on input line 55.
LaTeX Font Info: Checking defaults for T1/cmr/m/n on input line 55.
LaTeX Font Info: ... okay on input line 55.
LaTeX Font Info: Checking defaults for TS1/cmr/m/n on input line 55.
LaTeX Font Info: ... okay on input line 55.
LaTeX Font Info: Checking defaults for OMX/cmex/m/n on input line 55.
LaTeX Font Info: ... okay on input line 55.
LaTeX Font Info: Checking defaults for U/cmr/m/n on input line 55.
LaTeX Font Info: ... okay on input line 55.
LaTeX Font Info: Checking defaults for PD1/pdf/m/n on input line 55.
LaTeX Font Info: ... okay on input line 55.
LaTeX Font Info: Checking defaults for PU/pdf/m/n on input line 55.
LaTeX Font Info: ... okay on input line 55.
*geometry* driver: auto-detecting
*geometry* detected driver: pdftex
*geometry* verbose mode - [ preamble ] result:
* driver: pdftex
* paper: letterpaper
* layout: <same size as paper>
* layoutoffset:(h,v)=(0.0pt,0.0pt)
* modes:
* h-part:(L,W,R)=(72.26999pt, 469.75502pt, 72.26999pt)
* v-part:(T,H,B)=(72.26999pt, 650.43001pt, 72.26999pt)
* \paperwidth=614.295pt
* \paperheight=794.96999pt
* \textwidth=469.75502pt
* \textheight=650.43001pt
* \oddsidemargin=0.0pt
* \evensidemargin=0.0pt
* \topmargin=-37.0pt
* \headheight=12.0pt
* \headsep=25.0pt
* \topskip=11.0pt
* \footskip=30.0pt
* \marginparwidth=59.0pt
* \marginparsep=10.0pt
* \columnsep=10.0pt
* \skip\footins=10.0pt plus 4.0pt minus 2.0pt
* \hoffset=0.0pt
* \voffset=0.0pt
* \mag=1000
* \@twocolumnfalse
* \@twosidefalse
* \@mparswitchfalse
* \@reversemarginfalse
* (1in=72.27pt=25.4mm, 1cm=28.453pt)
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/graphics\graphicx.sty
Package: graphicx 2026-05-17 v1.2e Enhanced LaTeX Graphics (DPC,SPQR)
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/graphics\graphics.sty
Package: graphics 2026-05-17 v1.4h Standard LaTeX Graphics (DPC,SPQR)
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/graphics\trig.sty
Package: trig 2023/12/02 v1.11 sin cos tan (DPC)
)
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/graphics-cfg\graphics.c
fg
File: graphics.cfg 2016/06/04 v1.11 sample graphics configuration
)
Package graphics Info: Driver file: pdftex.def on input line 106.
)
\Gin@req@height=\dimen260
\Gin@req@width=\dimen261
)
LaTeX Info: Redefining \microtypecontext on input line 55.
Package microtype Info: Applying patch `item' on input line 55.
Package microtype Info: Applying patch `toc' on input line 55.
Package microtype Info: Applying patch `eqnum' on input line 55.
Package microtype Info: Applying patch `footnote' on input line 55.
Package microtype Info: Applying patch `verbatim' on input line 55.
LaTeX Info: Redefining \microtypesetup on input line 55.
Package microtype Info: Generating PDF output.
Package microtype Info: Character protrusion enabled (level 2).
Package microtype Info: Using default protrusion set `alltext'.
Package microtype Info: No font expansion.
Package microtype Info: No adjustment of tracking.
Package microtype Info: No adjustment of interword spacing.
Package microtype Info: No adjustment of character kerning.
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/microtype\mt-cmr.cfg
File: mt-cmr.cfg 2013/05/19 v2.2 microtype config. file: Computer Modern Roman
(RS)
)
Package hyperref Info: Link coloring ON on input line 55.
(aes_cryptanalysis.out) (aes_cryptanalysis.out)
\@outlinefile=\write3
\openout3 = `aes_cryptanalysis.out'.
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/context/base/mkii\supp-pdf.mk
ii
[Loading MPS to PDF converter (version 2006.09.02).]
\scratchcounter=\count344
\scratchdimen=\dimen262
\scratchbox=\box67
\nofMPsegments=\count345
\nofMParguments=\count346
\everyMPshowfont=\toks37
\MPscratchCnt=\count347
\MPscratchDim=\dimen263
\MPnumerator=\count348
\makeMPintoPDFobject=\count349
\everyMPtoPDFconversion=\toks38
)
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/epstopdf-pkg\epstopdf-b
ase.sty
Package: epstopdf-base 2020-01-24 v2.11 Base part for package epstopdf
Package epstopdf-base Info: Redefining graphics rule for `.eps' on input line 4
85.
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/00miktex\epstopdf-sys.c
fg
File: epstopdf-sys.cfg 2021/03/18 v2.0 Configuration of epstopdf for MiKTeX
))
\c@lstlisting=\count350
LaTeX Font Info: Trying to load font information for U+msa on input line 56.
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/amsfonts\umsa.fd
File: umsa.fd 2013/01/14 v3.01 AMS symbols A
)
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/microtype\mt-msa.cfg
File: mt-msa.cfg 2006/02/04 v1.1 microtype config. file: AMS symbols (a) (RS)
)
LaTeX Font Info: Trying to load font information for U+msb on input line 56.
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/amsfonts\umsb.fd
File: umsb.fd 2013/01/14 v3.01 AMS symbols B
)
(C:\Users\jessi\AppData\Local\Programs\MiKTeX\tex/latex/microtype\mt-msb.cfg
File: mt-msb.cfg 2005/06/01 v1.0 microtype config. file: AMS symbols (b) (RS)
)
Package microtype Info: Loading generic protrusion settings for font family
(microtype) `cmtt' (encoding: T1).
(microtype) For optimal results, create family-specific settings.
(microtype) See the microtype manual for details.
Overfull \hbox (21.92322pt too wide) in paragraph at lines 60--67
\T1/cmr/m/n/10 prior MITM ap-proaches), and a machine-checked proof that the co
n-straint sys-tem $\OMS/cmsy/m/n/10 C\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 K; X[];
[] ; X[]\OT1/cmr/m/n/10 ) =
[]
(aes_cryptanalysis.toc [1
{C:/Users/jessi/AppData/Local/MiKTeX/fonts/map/pdftex/pdftex.map}])
\tf@toc=\write4
\openout4 = `aes_cryptanalysis.toc'.
[2]
Package mdframed Info: mdframed detected package amsthm
changed the theorem header of amsthm
(mdframed) on input line 95.
[3]
Package hyperref Warning: Token not allowed in a PDF string (Unicode):
(hyperref) removing `\@textsuperscript' on input line 109.
Overfull \hbox (195.31322pt too wide) in paragraph at lines 129--143
[]
[]
[4]
Overfull \hbox (39.82985pt too wide) in paragraph at lines 198--210
[]
[]
Overfull \hbox (126.86444pt too wide) in paragraph at lines 221--224
\T1/cmr/m/it/10.95 ter-is-tic is at most $\OT1/cmr/m/n/10.95 2[]$\T1/cmr/m/it/1
0.95 , far be-low the $\OT1/cmr/m/n/10.95 2[]$ \T1/cmr/m/it/10.95 se-cu-rity th
resh-old. [][MACHINE-CHECKED][] \T1/cmtt/m/it/10.95 AES_10Round_Terminal_Result
.lean\T1/cmr/m/it/10.95 .
[]
Overfull \hbox (18.69676pt too wide) in paragraph at lines 248--252
\OMS/cmsy/m/n/10.95 f[]g$ \T1/cmr/m/it/10.95 onto $\OMS/cmsy/m/n/10.95 f\OT1/cm
r/m/n/10.95 0\OML/cmm/m/it/10.95 ; [] ; \OT1/cmr/m/n/10.95 254\OMS/cmsy/m/n/10.
95 g$ \T1/cmr/m/it/10.95 with max-i-mum en-tropy (100% uni-for-mity). [][VERIFI
ED-COMPUTATIONAL][]
[]
Overfull \hbox (14.3675pt too wide) in paragraph at lines 254--258
[][]\T1/cmr/bx/n/10.95 Definition 4.3 \T1/cmr/m/n/10.95 (Per-Round Weighted Gau
ge)\T1/cmr/bx/n/10.95 . [][]\T1/cmr/m/it/10.95 [NOVELTY-CANDIDATE][]Let weights
$\OML/cmm/m/it/10.95 w \OT1/cmr/m/n/10.95 = [1\OML/cmm/m/it/10.95 ; \OT1/cmr/m
/n/10.95 4\OML/cmm/m/it/10.95 ; \OT1/cmr/m/n/10.95 16\OML/cmm/m/it/10.95 ; \OT1
/cmr/m/n/10.95 64]$
[]
[5]
Overfull \hbox (47.53549pt too wide) in paragraph at lines 279--284
[][]\T1/cmr/bx/n/10.95 Theorem 4.4 \T1/cmr/m/n/10.95 (M�bius Bridge Mem-ory Re-
duc-tion)\T1/cmr/bx/n/10.95 . [][]\T1/cmr/m/it/10.95 [MACHINE-CHECKED][] [][NOV
ELTY-CANDIDATE][]The
[]
Overfull \hbox (71.46558pt too wide) in paragraph at lines 279--284
\T1/cmr/m/it/10.95 duc-tion lower bound of $\OT1/cmr/m/n/10.95 256\OMS/cmsy/m/n
/10.95 ^^B$ \T1/cmr/m/it/10.95 ($\OT1/cmr/m/n/10.95 2[]$\T1/cmr/m/it/10.95 ) ov
er na�ve MITM. [][MACHINE-CHECKED][] \T1/cmtt/m/it/10.95 AES_Mobius_Bridge_Theo
rems.lean
[]
Package hyperref Warning: Token not allowed in a PDF string (Unicode):
(hyperref) removing `math shift' on input line 313.
Package hyperref Warning: Token not allowed in a PDF string (Unicode):
(hyperref) removing `subscript' on input line 313.
Package hyperref Warning: Token not allowed in a PDF string (Unicode):
(hyperref) removing `math shift' on input line 313.
Overfull \hbox (18.07191pt too wide) in paragraph at lines 322--327
\T1/cmr/m/it/10.95 at-tack can be built on this lin-eariza-tion. [][MACHINE-CHE
CKED][] \T1/cmtt/m/it/10.95 AES_10Round_Terminal_Result.lean
[]
Overfull \hbox (21.5956pt too wide) in paragraph at lines 329--333
[][]\T1/cmr/bx/n/10.95 Theorem 5.3 \T1/cmr/m/n/10.95 (Rank vs. In-ver-sion Boun
d-ary)\T1/cmr/bx/n/10.95 . [][]\T1/cmr/m/it/10.95 [MACHINE-CHECKED][] [][NOVELT
Y-CANDIDATE][]The
[]
[6]
Overfull \hbox (182.04147pt too wide) in paragraph at lines 411--429
[]
[]
[7]
Overfull \hbox (58.19208pt too wide) in paragraph at lines 453--457
[][]\T1/cmr/bx/n/10.95 Proposition 8.1 \T1/cmr/m/n/10.95 (AES S-box Braid Depth
)\T1/cmr/bx/n/10.95 . [][]\T1/cmr/m/it/10.95 [VERIFIED-COMPUTATIONAL][] [][NOVE
LTY-CANDIDATE][]The
[]
Overfull \hbox (25.35147pt too wide) in paragraph at lines 459--463
[][]\T1/cmr/bx/n/10.95 Proposition 8.2 \T1/cmr/m/n/10.95 (Grover Or-a-cle Cost)
\T1/cmr/bx/n/10.95 . [][]\T1/cmr/m/it/10.95 [VERIFIED-COMPUTATIONAL][] [][NOVEL
TY-CANDIDATE][]A
[]
[8]
Overfull \hbox (157.0416pt too wide) in paragraph at lines 525--527
[]\T1/cmr/m/n/10.95 All code, Lean proofs, and MILP for-mu-la-tions are in the
open-source repos-i-tory \T1/cmtt/m/n/10.95 github.com/SNAPKITTYWEST/ahmad-foun
dations\T1/cmr/m/n/10.95 .
[]
[9] [10] (aes_cryptanalysis.aux)
***********
LaTeX2e <2026-06-01>
L3 programming layer <2026-06-18>
***********
LaTeX Warning: Label(s) may have changed. Rerun to get cross-references right.
Package rerunfilecheck Info: File `aes_cryptanalysis.out' has not changed.
(rerunfilecheck) Checksum: DEE582115B8C35213D9B403CD6908C9D;3817.
)
Here is how much of TeX's memory you used:
16859 strings out of 467510
270791 string characters out of 5408794
749179 words of memory out of 5000000
45767 multiletter control sequences out of 15000+600000
652880 words of font info for 104 fonts, out of 8000000 for 9000
1141 hyphenation exceptions out of 8191
75i,9n,79p,1016b,638s stack positions out of 10000i,1000n,20000p,200000b,200000s
<C:\Users\jessi\AppData\Local\MiKTeX\fonts/pk/ljfour/jknappen/ec/dpi600\ecbi
1095.pk> <C:\Users\jessi\AppData\Local\MiKTeX\fonts/pk/ljfour/jknappen/ec/dpi60
0\ecit1095.pk> <C:\Users\jessi\AppData\Local\MiKTeX\fonts/pk/ljfour/jknappen/ec
/dpi600\ectt1095.pk> <C:\Users\jessi\AppData\Local\MiKTeX\fonts/pk/ljfour/jknap
pen/ec/dpi600\ecbx0800.pk> <C:\Users\jessi\AppData\Local\MiKTeX\fonts/pk/ljfour
/jknappen/ec/dpi600\ecbx1200.pk> <C:\Users\jessi\AppData\Local\MiKTeX\fonts/pk/
ljfour/jknappen/ec/dpi600\ecti1095.pk> <C:\Users\jessi\AppData\Local\MiKTeX\fon
ts/pk/ljfour/jknappen/ec/dpi600\ecrm1095.pk> <C:\Users\jessi\AppData\Local\MiKT
eX\fonts/pk/ljfour/jknappen/ec/dpi600\ecbx1095.pk> <C:\Users\jessi\AppData\Loca
l\MiKTeX\fonts/pk/ljfour/jknappen/ec/dpi600\ecbx1440.pk> <C:\Users\jessi\AppDat
a\Local\MiKTeX\fonts/pk/ljfour/jknappen/ec/dpi600\ectt1000.pk> <C:\Users\jessi\
AppData\Local\MiKTeX\fonts/pk/ljfour/jknappen/ec/dpi600\ecrm1000.pk> <C:\Users\
jessi\AppData\Local\MiKTeX\fonts/pk/ljfour/jknappen/ec/dpi600\ecbx1000.pk> <C:\
Users\jessi\AppData\Local\MiKTeX\fonts/pk/ljfour/jknappen/ec/dpi600\ecit1000.pk
> <C:\Users\jessi\AppData\Local\MiKTeX\fonts/pk/ljfour/jknappen/ec/dpi600\ecti1
000.pk> <C:\Users\jessi\AppData\Local\MiKTeX\fonts/pk/ljfour/jknappen/ec/dpi600
\ecrm0800.pk> <C:\Users\jessi\AppData\Local\MiKTeX\fonts/pk/ljfour/jknappen/ec/
dpi600\ecrm1200.pk> <C:\Users\jessi\AppData\Local\MiKTeX\fonts/pk/ljfour/jknapp
en/ec/dpi600\ecbx1728.pk><C:/Users/jessi/AppData/Local/Programs/MiKTeX/fonts/ty
pe1/public/amsfonts/cm/cmbx10.pfb><C:/Users/jessi/AppData/Local/Programs/MiKTeX
/fonts/type1/public/amsfonts/cm/cmex10.pfb><C:/Users/jessi/AppData/Local/Progra
ms/MiKTeX/fonts/type1/public/amsfonts/cm/cmmi10.pfb><C:/Users/jessi/AppData/Loc
al/Programs/MiKTeX/fonts/type1/public/amsfonts/cm/cmmi12.pfb><C:/Users/jessi/Ap
pData/Local/Programs/MiKTeX/fonts/type1/public/amsfonts/cm/cmmi7.pfb><C:/Users/
jessi/AppData/Local/Programs/MiKTeX/fonts/type1/public/amsfonts/cm/cmmi8.pfb><C
:/Users/jessi/AppData/Local/Programs/MiKTeX/fonts/type1/public/amsfonts/cm/cmr1
0.pfb><C:/Users/jessi/AppData/Local/Programs/MiKTeX/fonts/type1/public/amsfonts
/cm/cmr7.pfb><C:/Users/jessi/AppData/Local/Programs/MiKTeX/fonts/type1/public/a
msfonts/cm/cmr8.pfb><C:/Users/jessi/AppData/Local/Programs/MiKTeX/fonts/type1/p
ublic/amsfonts/cm/cmsy10.pfb><C:/Users/jessi/AppData/Local/Programs/MiKTeX/font
s/type1/public/amsfonts/cm/cmsy8.pfb><C:/Users/jessi/AppData/Local/Programs/MiK
TeX/fonts/type1/public/amsfonts/cm/cmtt10.pfb>
Output written on aes_cryptanalysis.pdf (10 pages, 411021 bytes).
PDF statistics:
1012 PDF objects out of 1200 (max. 8388607)
78 named destinations out of 1000 (max. 500000)
20145 words of extra memory for PDF output out of 20736 (max. 10000000)