more

main.aux

@@ -4,7 +4,7 @@
 \providecommand\HyField@AuxAddToFields[1]{}
 \providecommand\HyField@AuxAddToCoFields[2]{}
 \citation{Lamport_1994,Holzmann_1997,Clarke_Wang}
-\citation{Basin_Cremers_Dreier_Sasse_2022,Blanchet_Smyth_Cheval_Sylvestre,Kobeissi_Nicolas_Tiwari,Blanchet_Jacomme,Basin_Linker_Sasse}
+\citation{Basin_Cremers_Dreier_Sasse_2022,Kobeissi_Nicolas_Tiwari,Blanchet_Jacomme,Basin_Linker_Sasse}
 \citation{Hippel2022_anonym}
 \providecommand \oddpage@label [2]{}
 \@writefile{toc}{\contentsline {section}{\numberline {I}Introduction}{1}{section.1}\protected@file@percent }
@@ -64,7 +64,6 @@
 \citation{Hippel2022_anonym}
 \citation{Hippel2022_anonym}
 \citation{Hippel2022_anonym}
-\citation{Hippel2022_anonym}
 \newlabel{res:raft_table}{{\caption@xref {res:raft_table}{ on input line 93}}{6}{Raft}{figure.caption.8}{}}
 \@writefile{lof}{\contentsline {figure}{\numberline {3}{\ignorespaces Breakdown of the attacker scenarios assessed with \textsc  {PANDA}\xspace  against our buggy Raft \textsc  {Promela}\xspace  model, \texttt  {raft-bug.pml}. In all experiments, the Raft model was set to five peers and the drop/replay limits of the gadgets \textsc  {PANDA}\xspace  synthesized were set to two. We conducted our experiments on a research computing cluster, allocating 250GB of memory to each verification run. The full models and attacker traces are included in the artifact.}}{6}{figure.caption.8}\protected@file@percent }
 \newlabel{res:raft_table}{{3}{6}{Breakdown of the attacker scenarios assessed with \korg against our buggy Raft \promela model, \texttt {raft-bug.pml}. In all experiments, the Raft model was set to five peers and the drop/replay limits of the gadgets \korg synthesized were set to two. We conducted our experiments on a research computing cluster, allocating 250GB of memory to each verification run. The full models and attacker traces are included in the artifact}{figure.caption.8}{}}
@@ -78,18 +77,18 @@
 \citation{Blanchet_Jacomme,Pereira}
 \citation{ParnoSOK,Basin_Cremers_Meadows_2018}
 \citation{Khan_Mukund_Suresh_2005,Clarke_Wang,wayne_adversaries,Narayana_Chen_Zhao_Chen_Fu_Zhou_2006,Delzanno_Tatarek_Traverso_2014}
-\citation{Wilcox_Woos_Panchekha_Tatlock_Wang_Ernst_Anderson,Castro_Liskov_2002}
+\citation{Wilcox_Woos_Panchekha_Tatlock_Wang_Ernst_Anderson,Castro_Liskov_2002,Delzanno_Tatarek_Traverso_2014}
 \citation{Henda}
 \citation{Ginesin}
 \citation{TCPwn}
 \bibstyle{IEEEtran}
 \bibdata{main}
 \bibcite{Lamport_1994}{1}
+\bibcite{Holzmann_1997}{2}
 \@writefile{toc}{\contentsline {section}{\numberline {V}Related Work}{7}{section.5}\protected@file@percent }
 \newlabel{sec:Related Work}{{V}{7}{Related Work}{section.5}{}}
 \@writefile{toc}{\contentsline {section}{\numberline {VI}Conclusion}{7}{section.6}\protected@file@percent }
 \newlabel{sec:conclusion}{{VI}{7}{Conclusion}{section.6}{}}
-\bibcite{Holzmann_1997}{2}
 \bibcite{Clarke_Wang}{3}
 \bibcite{Basin_Cremers_Dreier_Sasse_2022}{4}
 \bibcite{Kobeissi_Nicolas_Tiwari}{5}

main.blg

@@ -8,15 +8,6 @@ Reallocated singl_function (elt_size=8) to 100 items from 50.
 Reallocated wiz_functions (elt_size=8) to 6000 items from 3000.
 Reallocated singl_function (elt_size=8) to 100 items from 50.
 Database file #1: main.bib
-Repeated entry---line 97 of file main.bib
- : @article{Kobeissi_Nicolas_Tiwari
- :                                 , title={Verifpal: Cryptographic Protocol Analysis for the Real World}, abstractNote={Verifpal is a new automated modeling framework and verifier for cryptographic protocols, optimized with heuristics for common-case protocol specifications, that aims to work better for real-world practitioners, students and engineers without sacrificing comprehensive formal verification features. In order to achieve this, Verifpal introduces a new, intuitive language for modeling protocols that is easier to write and understand than the languages employed by existing tools. Its formal verification paradigm is also designed explicitly to provide protocol modeling that avoids user error. Verifpal is able to model protocols under an active attacker with unbounded sessions and fresh values, and supports queries for advanced security properties such as forward secrecy or key compromise impersonation. Furthermore, Verifpal’s semantics have been formalized within the Coq theorem prover, and Verifpal models can be automatically translated into Coq as well as into ProVerif models for further verification. Verifpal has already been used to verify security properties for Signal, Scuttlebutt, TLS 1.3 as well as the first formal model for the DP-3T pandemic-tracing protocol, which we present in this work. Through Verifpal, we show that advanced verification with formalized semantics and sound logic can exist without any expense towards the convenience of real-world practitioners.}, author={Kobeissi, Nadim and Nicolas, Georgio and Tiwari, Mukesh}, language={en} }
-I'm skipping whatever remains of this entry
-Repeated entry---line 115 of file main.bib
- : @article{Clarke_Wang
- :                     , title={25 Years of Model Checking}, abstractNote={Model Checking is an automatic verification technique for large state transition systems. It was originally developed for reasoning about finite-state concurrent systems. The technique has been used successfully to debug complex computer hardware, communication protocols, and software. It is beginning to be used for analyzing cyberphysical, biological, and financial systems as well. The major challenge for the technique is a phenomenon called the State Explosion Problem. This issue is impossible to avoid in the worst case; but, by using sophisticated data structures and clever search algorithms, it is now possible to verify state transition systems with an astronomical number of states. In this paper, we will briefly review the development of Model Checking over the past 32 years, with an emphasis on model checking stochastic hybrid systems.}, author={Clarke, Edmund M and Wang, Qinsi}, language={en} }
-I'm skipping whatever remains of this entry
-Warning--I didn't find a database entry for "Blanchet_Smyth_Cheval_Sylvestre"
 -- IEEEtran.bst version 1.14 (2015/08/26) by Michael Shell.
 -- http://www.michaelshell.org/tex/ieeetran/bibtex/
 -- See the "IEEEtran_bst_HOWTO.pdf" manual for usage information.
@@ -42,7 +33,7 @@ Warning--empty journal in Ginesin
 Done.
 You've used 32 entries,
             4087 wiz_defined-function locations,
-            1049 strings with 14007 characters,
+            1047 strings with 13945 characters,
 and the built_in function-call counts, 19759 in all, are:
 = -- 1710
 > -- 401
@@ -81,4 +72,4 @@ warning$ -- 18
 while$ -- 51
 width$ -- 34
 write$ -- 345
-(There were 2 error messages)
+(There were 18 warnings)

main.fls

@@ -518,8 +518,6 @@ INPUT /usr/share/texmf-dist/fonts/vf/adobe/times/ptmrc7t.vf
 INPUT /usr/share/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm
 INPUT /usr/share/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm
 INPUT /usr/share/texmf-dist/fonts/vf/adobe/times/ptmr7t.vf
-INPUT /usr/share/texmf-dist/fonts/vf/adobe/times/ptmb7t.vf
-INPUT /usr/share/texmf-dist/fonts/tfm/adobe/times/ptmb8r.tfm
 INPUT /usr/share/texmf-dist/fonts/vf/adobe/times/ptmr7t.vf
 INPUT /usr/share/texmf-dist/fonts/tfm/adobe/times/ptmr8r.tfm
 INPUT /usr/share/texmf-dist/fonts/vf/adobe/times/ptmr7t.vf
@@ -539,6 +537,8 @@ INPUT /usr/share/texmf-dist/tex/latex/psnfss/ot1pcr.fd
 INPUT /usr/share/texmf-dist/tex/latex/psnfss/ot1pcr.fd
 INPUT /usr/share/texmf-dist/fonts/tfm/adobe/courier/pcrr7t.tfm
 INPUT /usr/share/texmf-dist/fonts/tfm/adobe/courier/pcrr7t.tfm
+INPUT /usr/share/texmf-dist/fonts/vf/adobe/times/ptmb7t.vf
+INPUT /usr/share/texmf-dist/fonts/tfm/adobe/times/ptmb8r.tfm
 INPUT /usr/share/texmf-dist/fonts/vf/adobe/courier/pcrr7t.vf
 INPUT /usr/share/texmf-dist/fonts/tfm/adobe/courier/pcrr8r.tfm
 INPUT ./sections/examples.tex

main.log

@@ -1,4 +1,4 @@
-This is pdfTeX, Version 3.141592653-2.6-1.40.26 (TeX Live 2024/Arch Linux) (preloaded format=pdflatex 2024.7.2)  3 DEC 2024 17:34
+This is pdfTeX, Version 3.141592653-2.6-1.40.26 (TeX Live 2024/Arch Linux) (preloaded format=pdflatex 2024.7.2)  4 DEC 2024 16:46
 entering extended mode
  restricted \write18 enabled.
  %&-line parsing enabled.
@@ -1315,15 +1315,12 @@ LaTeX Warning: No \author given.
 LaTeX Warning: No \author given.
 
 (./sections/abstract.tex) (./sections/introduction.tex
+LaTeX Font Info:    Trying to load font information for U+msa on input line 7.
 
-LaTeX Warning: Citation `Blanchet_Smyth_Cheval_Sylvestre' on page 1 undefined o
-n input line 3.
-
-LaTeX Font Info:    Trying to load font information for U+msa on input line 6.
 (/usr/share/texmf-dist/tex/latex/amsfonts/umsa.fd
 File: umsa.fd 2013/01/14 v3.01 AMS symbols A
 )
-LaTeX Font Info:    Trying to load font information for U+msb on input line 6.
+LaTeX Font Info:    Trying to load font information for U+msb on input line 7.
 
 (/usr/share/texmf-dist/tex/latex/amsfonts/umsb.fd
 File: umsb.fd 2013/01/14 v3.01 AMS symbols B
@@ -1373,6 +1370,15 @@ LaTeX Font Info:    Trying to load font information for TS1+pcr on input line 3
  (/usr/share/texmf-dist/tex/latex/psnfss/ts1pcr.fd
 File: ts1pcr.fd 2001/06/04 font definitions for TS1/pcr.
 )
+Underfull \hbox (badness 10000) in paragraph at lines 360--361
+
+ []
+
+
+Underfull \hbox (badness 10000) in paragraph at lines 360--361
+
+ []
+
 Excluding 'comment' comment.) (./sections/case_studies.tex
 Underfull \hbox (badness 4144) in paragraph at lines 19--19
 []\OT1/pcr/m/n/10 SYN_RECEIVED \OT1/ptm/m/n/10 is even-tu-ally fol-lowed by
@@ -1398,6 +1404,9 @@ Underfull \hbox (badness 3646) in paragraph at lines 109--109
 []\OT1/ptm/m/n/10 Fig. 3: |Break-down of the at-tacker sce-nar-ios as-sessed
  []
 
+
+LaTeX Warning: `!h' float specifier changed to `!ht'.
+
 ) (./sections/proofs.tex
 Underfull \hbox (badness 3503) in paragraph at lines 19--21
 [][]\OT1/ptm/b/n/10 Definition 2 \OT1/ptm/m/n/10 (Pro-cess)\OT1/ptm/b/n/10 . []
@@ -1428,6 +1437,12 @@ Underfull \hbox (badness 1715) in paragraph at lines 97--99
 ** WARNING: IEEEtran.bst: No hyphenation pattern has been
 ** loaded for the language `en'. Using the pattern for
 ** the default language instead.
+** WARNING: IEEEtran.bst: No hyphenation pattern has been
+** loaded for the language `en'. Using the pattern for
+** the default language instead.
+** WARNING: IEEEtran.bst: No hyphenation pattern has been
+** loaded for the language `en'. Using the pattern for
+** the default language instead.
 [7]
 ** WARNING: IEEEtran.bst: No hyphenation pattern has been
 ** loaded for the language `en'. Using the pattern for
@@ -1472,12 +1487,6 @@ Underfull \hbox (badness 1715) in paragraph at lines 97--99
 ** loaded for the language `en'. Using the pattern for
 ** the default language instead.
 ** WARNING: IEEEtran.bst: No hyphenation pattern has been
-** loaded for the language `en'. Using the pattern for
-** the default language instead.
-** WARNING: IEEEtran.bst: No hyphenation pattern has been
-** loaded for the language `en'. Using the pattern for
-** the default language instead.
-** WARNING: IEEEtran.bst: No hyphenation pattern has been
 ** loaded for the language `eng'. Using the pattern for
 ** the default language instead.
 ** WARNING: IEEEtran.bst: No hyphenation pattern has been
@@ -1568,22 +1577,19 @@ L3 programming layer <2024-02-20>
  ***********
 
 
-LaTeX Warning: There were undefined references.
-
-
 LaTeX Warning: There were multiply-defined labels.
 
 Package rerunfilecheck Info: File `main.out' has not changed.
 (rerunfilecheck)             Checksum: 27EE6006AAFB1A1E6386C970007B5C60;1792.
  ) 
 Here is how much of TeX's memory you used:
- 41059 strings out of 476076
+ 41058 strings out of 476076
- 907916 string characters out of 5793776
+ 907883 string characters out of 5793776
  2208187 words of memory out of 5000000
- 62173 multiletter control sequences out of 15000+600000
+ 62172 multiletter control sequences out of 15000+600000
  606090 words of font info for 125 fonts, out of 8000000 for 9000
  14 hyphenation exceptions out of 8191
- 99i,11n,101p,1201b,1550s stack positions out of 10000i,1000n,20000p,200000b,200000s
+ 99i,11n,101p,1201b,1517s stack positions out of 10000i,1000n,20000p,200000b,200000s
 </usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmex10.pfb></usr/share/
 texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb></usr/share/texmf-dist/fon
 ts/type1/public/amsfonts/cm/cmmi5.pfb></usr/share/texmf-dist/fonts/type1/public
@@ -1595,7 +1601,7 @@ lic/amsfonts/cm/cmsy7.pfb></usr/share/texmf-dist/fonts/type1/urw/courier/ucrr8a
 .pfb></usr/share/texmf-dist/fonts/type1/urw/times/utmb8a.pfb></usr/share/texmf-
 dist/fonts/type1/urw/times/utmbi8a.pfb></usr/share/texmf-dist/fonts/type1/urw/t
 imes/utmr8a.pfb></usr/share/texmf-dist/fonts/type1/urw/times/utmri8a.pfb>
-Output written on ./main.pdf (8 pages, 267478 bytes).
+Output written on ./main.pdf (8 pages, 266844 bytes).
 PDF statistics:
  565 PDF objects out of 1000 (max. 8388607)
  520 compressed objects within 6 object streams