% Generated by IEEEtran.bst, version: 1.14 (2015/08/26)
\begin{thebibliography}{10}
\providecommand{\url}[1]{#1}
\csname url@samestyle\endcsname
\providecommand{\newblock}{\relax}
\providecommand{\bibinfo}[2]{#2}
\providecommand{\BIBentrySTDinterwordspacing}{\spaceskip=0pt\relax}
\providecommand{\BIBentryALTinterwordstretchfactor}{4}
\providecommand{\BIBentryALTinterwordspacing}{\spaceskip=\fontdimen2\font plus
\BIBentryALTinterwordstretchfactor\fontdimen3\font minus
  \fontdimen4\font\relax}
\providecommand{\BIBforeignlanguage}[2]{{%
\expandafter\ifx\csname l@#1\endcsname\relax
\typeout{** WARNING: IEEEtran.bst: No hyphenation pattern has been}%
\typeout{** loaded for the language `#1'. Using the pattern for}%
\typeout{** the default language instead.}%
\else
\language=\csname l@#1\endcsname
\fi
#2}}
\providecommand{\BIBdecl}{\relax}
\BIBdecl

\bibitem{Lamport_1994}
L.~Lamport, ``\BIBforeignlanguage{en}{The temporal logic of actions},''
  \emph{\BIBforeignlanguage{en}{ACM Transactions on Programming Languages and
  Systems}}, vol.~16, no.~3, p. 872–923, May 1994.

\bibitem{Holzmann_1997}
G.~Holzmann, ``\BIBforeignlanguage{en}{The model checker spin},''
  \emph{\BIBforeignlanguage{en}{IEEE Transactions on Software Engineering}},
  vol.~23, no.~5, p. 279–295, May 1997.

\bibitem{Clarke_Wang}
E.~M. Clarke and Q.~Wang, ``\BIBforeignlanguage{en}{25 years of model
  checking}.''

\bibitem{Basin_Cremers_Dreier_Sasse_2022}
D.~Basin, C.~Cremers, J.~Dreier, and R.~Sasse,
  ``\BIBforeignlanguage{en}{Tamarin: Verification of large-scale, real-world,
  cryptographic protocols},'' \emph{\BIBforeignlanguage{en}{IEEE Security \&
  Privacy}}, vol.~20, no.~3, p. 24–32, May 2022.

\bibitem{Kobeissi_Nicolas_Tiwari}
N.~Kobeissi, G.~Nicolas, and M.~Tiwari, ``\BIBforeignlanguage{en}{Verifpal:
  Cryptographic protocol analysis for the real world}.''

\bibitem{Blanchet_Jacomme}
B.~Blanchet and C.~Jacomme, ``\BIBforeignlanguage{en}{Cryptoverif: a
  computationally-sound security protocol verifier}.''

\bibitem{Basin_Linker_Sasse}
D.~Basin, F.~Linker, and R.~Sasse, ``\BIBforeignlanguage{en}{A formal analysis
  of the imessage pq3 messaging protocol}.''

\bibitem{Hippel2022_anonym}
Anonym, ``Anonymized for blinded submission,'' XXX.

\bibitem{Holzmann_2014}
G.~J. Holzmann, ``\BIBforeignlanguage{en}{Mars code},''
  \emph{\BIBforeignlanguage{en}{Communications of the ACM}}, vol.~57, no.~2, p.
  64–73, Feb. 2014.

\bibitem{Holzmann_Smith_2000}
G.~J. Holzmann and M.~H. Smith, ``\BIBforeignlanguage{en}{Automating software
  feature verification},'' \emph{\BIBforeignlanguage{en}{Bell Labs Technical
  Journal}}, vol.~5, no.~2, p. 72–87, 2000.

\bibitem{mcp}
\BIBentryALTinterwordspacing
W.~Visser, K.~Havelund, G.~Brat, and S.~Park, ``\BIBforeignlanguage{en}{Model
  checking programs},'' in \emph{\BIBforeignlanguage{en}{Proceedings ASE 2000.
  Fifteenth IEEE International Conference on Automated Software
  Engineering}}.\hskip 1em plus 0.5em minus 0.4em\relax Grenoble, France: IEEE,
  2000, p. 3–11. [Online]. Available:
  \url{http://ieeexplore.ieee.org/document/873645/}
\BIBentrySTDinterwordspacing

\bibitem{Cluzel_Georgiou_Moy_Zeller_2021}
\BIBentryALTinterwordspacing
G.~Cluzel, K.~Georgiou, Y.~Moy, and C.~Zeller,
  ``\BIBforeignlanguage{en}{Layered formal verification of a tcp stack},'' in
  \emph{\BIBforeignlanguage{en}{2021 IEEE Secure Development Conference
  (SecDev)}}.\hskip 1em plus 0.5em minus 0.4em\relax Atlanta, GA, USA: IEEE,
  Oct. 2021, p. 86–93. [Online]. Available:
  \url{https://ieeexplore.ieee.org/document/9652642/}
\BIBentrySTDinterwordspacing

\bibitem{Smith_1997}
\BIBentryALTinterwordspacing
M.~A.~S. Smith, ``\BIBforeignlanguage{eng}{Formal verification of tcp and
  t/tcp},'' Thesis, Massachusetts Institute of Technology, 1997, accepted:
  2008-09-03T18:09:43Z. [Online]. Available:
  \url{https://dspace.mit.edu/handle/1721.1/42779}
\BIBentrySTDinterwordspacing

\bibitem{Pacheco2022}
\BIBentryALTinterwordspacing
M.~L. Pacheco, M.~V. Hippel, B.~Weintraub, D.~Goldwasser, and C.~Nita-Rotaru,
  ``\BIBforeignlanguage{en}{Automated attack synthesis by extracting finite
  state machines from protocol specification documents},'' in
  \emph{\BIBforeignlanguage{en}{2022 IEEE Symposium on Security and Privacy
  (SP)}}.\hskip 1em plus 0.5em minus 0.4em\relax San Francisco, CA, USA: IEEE,
  May 2022, p. 51–68. [Online]. Available:
  \url{https://ieeexplore.ieee.org/document/9833673/}
\BIBentrySTDinterwordspacing

\bibitem{Woos_Wilcox_Anton_Tatlock_Ernst_Anderson_2016}
\BIBentryALTinterwordspacing
D.~Woos, J.~R. Wilcox, S.~Anton, Z.~Tatlock, M.~D. Ernst, and T.~Anderson,
  ``\BIBforeignlanguage{en}{Planning for change in a formal verification of the
  raft consensus protocol},'' in \emph{\BIBforeignlanguage{en}{Proceedings of
  the 5th ACM SIGPLAN Conference on Certified Programs and Proofs}}.\hskip 1em
  plus 0.5em minus 0.4em\relax St. Petersburg FL USA: ACM, Jan. 2016, p.
  154–165. [Online]. Available:
  \url{https://dl.acm.org/doi/10.1145/2854065.2854081}
\BIBentrySTDinterwordspacing

\bibitem{Wilcox_Woos_Panchekha_Tatlock_Wang_Ernst_Anderson}
J.~R. Wilcox, D.~Woos, P.~Panchekha, Z.~Tatlock, X.~Wang, M.~D. Ernst, and
  T.~Anderson, ``\BIBforeignlanguage{en}{Verdi: A framework for implementing
  and formally verifying distributed systems}.''

\bibitem{Ongaro}
D.~Ongaro, ``\BIBforeignlanguage{en}{Consensus: Bridging theory and
  practice}.''

\bibitem{Kozen_1977}
\BIBentryALTinterwordspacing
D.~Kozen, ``\BIBforeignlanguage{en}{Lower bounds for natural proof systems},''
  in \emph{\BIBforeignlanguage{en}{18th Annual Symposium on Foundations of
  Computer Science (sfcs 1977)}}.\hskip 1em plus 0.5em minus 0.4em\relax
  Providence, RI, USA: IEEE, Sep. 1977, p. 254–266. [Online]. Available:
  \url{http://ieeexplore.ieee.org/document/4567949/}
\BIBentrySTDinterwordspacing

\bibitem{Proverif}
B.~Blanchet, B.~Smyth, V.~Cheval, and M.~Sylvestre,
  ``\BIBforeignlanguage{en}{Proverif 2.05: Automatic cryptographic protocol
  verifier, user manual and tutorial}.''

\bibitem{Tamarin}
D.~Basin, C.~Cremers, J.~Dreier, and R.~Sasse,
  ``\BIBforeignlanguage{en}{Tamarin: Verification of large-scale, real-world,
  cryptographic protocols},'' \emph{\BIBforeignlanguage{en}{IEEE Security \&
  Privacy}}, vol.~20, no.~3, p. 24–32, May 2022.

\bibitem{Cremers}
\BIBentryALTinterwordspacing
C.~J.~F. Cremers, \emph{\BIBforeignlanguage{en}{The Scyther Tool: Verification,
  Falsification, and Analysis of Security Protocols}}, ser. Lecture Notes in
  Computer Science.\hskip 1em plus 0.5em minus 0.4em\relax Berlin, Heidelberg:
  Springer Berlin Heidelberg, 2008, vol. 5123, p. 414–418. [Online].
  Available: \url{http://link.springer.com/10.1007/978-3-540-70545-1_38}
\BIBentrySTDinterwordspacing

\bibitem{Pereira}
V.~Pereira, ``\BIBforeignlanguage{en}{Easycrypt - a (brief) tutorial}.''

\bibitem{ParnoSOK}
\BIBentryALTinterwordspacing
M.~Barbosa, G.~Barthe, K.~Bhargavan, B.~Blanchet, C.~Cremers, K.~Liao, and
  B.~Parno, ``Sok: Computer-aided cryptography,'' in \emph{2021 IEEE Symposium
  on Security and Privacy (SP)}, May 2021, p. 777–795. [Online]. Available:
  \url{https://ieeexplore.ieee.org/document/9519449/?arnumber=9519449}
\BIBentrySTDinterwordspacing

\bibitem{Basin_Cremers_Meadows_2018}
\BIBentryALTinterwordspacing
D.~Basin, C.~Cremers, and C.~Meadows, \emph{\BIBforeignlanguage{en}{Model
  Checking Security Protocols}}.\hskip 1em plus 0.5em minus 0.4em\relax Cham:
  Springer International Publishing, 2018, p. 727–762. [Online]. Available:
  \url{http://link.springer.com/10.1007/978-3-319-10575-8_22}
\BIBentrySTDinterwordspacing

\bibitem{Khan_Mukund_Suresh_2005}
\BIBentryALTinterwordspacing
A.~S. Khan, M.~Mukund, and S.~P. Suresh, \emph{\BIBforeignlanguage{en}{Generic
  Verification of Security Protocols}}, ser. Lecture Notes in Computer
  Science.\hskip 1em plus 0.5em minus 0.4em\relax Berlin, Heidelberg: Springer
  Berlin Heidelberg, 2005, vol. 3639, p. 221–235. [Online]. Available:
  \url{http://link.springer.com/10.1007/11537328_18}
\BIBentrySTDinterwordspacing

\bibitem{wayne_adversaries}
\BIBentryALTinterwordspacing
H.~Wayne, ``Modeling adversaries with tla+,''
  \url{https://www.hillelwayne.com/post/adversaries/}, 2019, accessed:
  2024-12-03. [Online]. Available:
  \url{https://www.hillelwayne.com/post/adversaries/}
\BIBentrySTDinterwordspacing

\bibitem{Narayana_Chen_Zhao_Chen_Fu_Zhou_2006}
\BIBentryALTinterwordspacing
P.~Narayana, R.~Chen, Y.~Zhao, Y.~Chen, Z.~Fu, and H.~Zhou, ``Automatic
  vulnerability checking of ieee 802.16 wimax protocols through tla+,'' in
  \emph{2006 2nd IEEE Workshop on Secure Network Protocols}, Nov. 2006, p.
  44–49. [Online]. Available:
  \url{https://ieeexplore.ieee.org/document/4110436/?arnumber=4110436}
\BIBentrySTDinterwordspacing

\bibitem{Delzanno_Tatarek_Traverso_2014}
G.~Delzanno, M.~Tatarek, and R.~Traverso, ``\BIBforeignlanguage{en}{Model
  checking paxos in spin},'' \emph{\BIBforeignlanguage{en}{Electronic
  Proceedings in Theoretical Computer Science}}, vol. 161, p. 131–146, Aug.
  2014.

\bibitem{Castro_Liskov_2002}
M.~Castro and B.~Liskov, ``\BIBforeignlanguage{en}{Practical byzantine fault
  tolerance and proactive recovery},'' \emph{\BIBforeignlanguage{en}{ACM
  Transactions on Computer Systems}}, vol.~20, no.~4, p. 398–461, Nov. 2002.

\bibitem{Henda}
\BIBentryALTinterwordspacing
N.~Ben~Henda, ``\BIBforeignlanguage{en}{Generic and efficient attacker models
  in spin},'' in \emph{\BIBforeignlanguage{en}{Proceedings of the 2014
  International SPIN Symposium on Model Checking of Software}}.\hskip 1em plus
  0.5em minus 0.4em\relax San Jose CA USA: ACM, Jul. 2014, p. 77–86.
  [Online]. Available: \url{https://dl.acm.org/doi/10.1145/2632362.2632378}
\BIBentrySTDinterwordspacing

\bibitem{Ginesin}
\BIBentryALTinterwordspacing
J.~Ginesin, M.~von Hippel, E.~Defloor, C.~Nita-Rotaru, and M.~Tüxen, ``A
  formal analysis of sctp: Attack synthesis and patch verification,'' no.
  arXiv:2403.05663, Mar. 2024, arXiv:2403.05663 [cs]. [Online]. Available:
  \url{http://arxiv.org/abs/2403.05663}
\BIBentrySTDinterwordspacing

\bibitem{TCPwn}
\BIBentryALTinterwordspacing
S.~Jero, E.~Hoque, D.~Choffnes, A.~Mislove, and C.~Nita-Rotaru,
  ``\BIBforeignlanguage{en}{Automated attack discovery in tcp congestion
  control using a model-guided approach},'' in
  \emph{\BIBforeignlanguage{en}{Proceedings 2018 Network and Distributed System
  Security Symposium}}.\hskip 1em plus 0.5em minus 0.4em\relax San Diego, CA:
  Internet Society, 2018. [Online]. Available:
  \url{https://www.ndss-symposium.org/wp-content/uploads/2018/02/ndss2018_02A-1_Jero_paper.pdf}
\BIBentrySTDinterwordspacing

\end{thebibliography}
