references.bib

@article{lanotte_formal_2021,
	title = {A Formal Approach to Physics-Based Attacks in Cyber-Physical Systems (Extended Version)},
	url = {http://arxiv.org/abs/1902.04572},
	abstract = {We apply formal methods to lay and streamline theoretical foundations to reason about Cyber-Physical Systems ({CPSs}) and physics-based attacks, i.e., attacks targeting physical devices. We focus on a formal treatment of both integrity and denial of service attacks to sensors and actuators of {CPSs}, and on the timing aspects of these attacks. Our contributions are fourfold. (1){\textasciitilde}We define a hybrid process calculus to model both {CPSs} and physics-based attacks. (2){\textasciitilde}We formalise a threat model that specifies {MITM} attacks that can manipulate sensor readings or control commands in order to drive a {CPS} into an undesired state, and we provide the means to assess attack tolerance/vulnerability with respect to a given attack. (3){\textasciitilde}We formalise how to estimate the impact of a successful attack on a {CPS} and investigate possible quantifications of the success chances of an attack. (4){\textasciitilde}We illustrate our definitions and results by formalising a non-trivial running example in Uppaal {SMC}, the statistical extension of the Uppaal model checker; we use Uppaal {SMC} as an automatic tool for carrying out a static security analysis of our running example in isolation and when exposed to three different physics-based attacks with different impacts.},
	journaltitle = {{arXiv}:1902.04572 [cs, eess]},
	author = {Lanotte, Ruggero and Merro, Massimo and Munteanu, Andrei and Viganò, Luca},
	urldate = {2021-05-26},
	date = {2021-05-22},
	eprinttype = {arxiv},
	eprint = {1902.04572},
	keywords = {Computer Science - Cryptography and Security, Computer Science - Logic in Computer Science, Electrical Engineering and Systems Science - Systems and Control},
	file = {arXiv Fulltext PDF:C\:\\Users\\felix\\Zotero\\storage\\858CH33R\\Lanotte et al. - 2021 - A Formal Approach to Physics-Based Attacks in Cybe.pdf:application/pdf;arXiv.org Snapshot:C\:\\Users\\felix\\Zotero\\storage\\RJ63LT3H\\1902.html:text/html},
}

@report{chin_leo_2021,
	title = {Leo: A Programming Language for Formally Verified, Zero-Knowledge Applications},
	url = {https://eprint.iacr.org/2021/651},
	shorttitle = {Leo},
	abstract = {Decentralized ledgers that support rich applications suffer from three limitations. First, applications are provisioned tiny execution environments with limited running time, minimal stack size, and restrictive instruction sets. Second, applications must reveal their state transition, enabling miner frontrunning attacks and consensus instability. Third, applications offer weak guarantees of correctness and safety.

We design, implement, and evaluate Leo, a new programming language designed for formally verified, zero-knowledge applications. Leo provisions a powerful execution environment that is not restricted in running time, stack size, or instruction sets. Besides offering application privacy and mitigating miner-extractable value ({MEV}), Leo achieves two fundamental properties. First, applications are formally verified with respect to their high-level specification. Second, applications can be succinctly verified by anyone, regardless of the size of application.

Leo is the first known programming language to introduce a testing framework, package registry, import resolver, remote compiler, formally defined language, and theorem prover for general-purpose, zero-knowledge applications.},
	number = {651},
	author = {Chin, Collin and Wu, Howard and Chu, Raymond and Coglio, Alessandro and {McCarthy}, Eric and Smith, Eric},
	urldate = {2021-05-28},
	date = {2021},
	keywords = {decentralized applications, formal methods, implementation, programming languages, zero-knowledge proofs},
	file = {ePrint IACR Snapshot:C\:\\Users\\felix\\Zotero\\storage\\RXQI2F44\\651.html:text/html;ePrint IACR Full Text PDF:C\:\\Users\\felix\\Zotero\\storage\\6HU3MTMH\\Chin et al. - 2021 - Leo A Programming Language for Formally Verified,.pdf:application/pdf},
}

@report{camenisch_internet_2021,
	title = {Internet Computer Consensus},
	url = {https://eprint.iacr.org/2021/632},
	abstract = {We present the Internet Computer Consensus ({ICC}) family of protocols for atomic broadcast (a.k.a., consensus), which underpin the Byzantine fault-tolerant replicated state machines of the Internet Computer. The {ICC} protocols are leader-based protocols that assume partial synchrony, and that are fully integrated with a blockchain. The leader changes probabilistically in every round. These protocols are extremely simple and robust: in any round where the leader is corrupt (which itself happens with probability less than \$1/3\$), each {ICC} protocol will effectively allow another party to take over as leader for that round, with very little fuss, to move the protocol forward to the next round in a timely fashion. Unlike in many other protocols, there are no complicated subprotocols (such as "view change'' in {PBFT}) or unspecified subprotocols (such as "pacemaker'' in {HotStuff}). Moreover, unlike in many other protocols (such as {PBFT} and {HotStuff}), the task of reliably disseminating the blocks to all parties is an integral part the protocol, and not left to some other unspecified subprotocol. An additional property enjoyed by the {ICC} protocols (just like {PBFT} and {HotStuff}, and unlike others, such as Tendermint) is optimistic responsiveness, which means that when the leader is honest, the protocol will proceed at the pace of the actual network delay, rather than some upper bound on the network delay. We present three different protocols (along with various minor variations on each). One of these protocols ({ICC}1) is designed to be integrated with a peer-to-peer gossip sub-layer, which reduces the bottleneck created at the leader for disseminating large blocks, a problem that all leader-based protocols, like {PBFT} and {HotStuff}, must address, but typically do not. Our Protocol {ICC}2 addresses the same problem by substituting a low-communication reliable broadcast subprotocol (which may be of independent interest) for the gossip sub-layer.},
	number = {632},
	author = {Camenisch, Jan and Drijvers, Manu and Hanke, Timo and Pignolet, Yvonne-Anne and Shoup, Victor and Williams, Dominic},
	urldate = {2021-05-28},
	date = {2021},
	keywords = {consensus, cryptographic protocols},
	file = {ePrint IACR Snapshot:C\:\\Users\\felix\\Zotero\\storage\\TJDGCEJ8\\632.html:text/html;ePrint IACR Full Text PDF:C\:\\Users\\felix\\Zotero\\storage\\U9FLWD47\\Camenisch et al. - 2021 - Internet Computer Consensus.pdf:application/pdf},
}

@report{pass_tutorial_2021,
	title = {A Tutorial on Concurrent Zero Knowledge},
	url = {https://eprint.iacr.org/2021/615},
	abstract = {In this tutorial, we provide a brief overview of Concurrent Zero Knowledge and next present a simple proof of the existence of Concurrent Zero-knowledge arguments for N P based on one-way permutations.},
	number = {615},
	author = {Pass, Rafael},
	urldate = {2021-05-28},
	date = {2021},
	keywords = {cryptographic protocols, concurrency, zero knowledge},
	file = {ePrint IACR Snapshot:C\:\\Users\\felix\\Zotero\\storage\\QN5S2VTX\\615.html:text/html;ePrint IACR Full Text PDF:C\:\\Users\\felix\\Zotero\\storage\\WK9ZLXPV\\Pass - 2021 - A Tutorial on Concurrent Zero Knowledge.pdf:application/pdf},
}

@report{dijk_autonomous_2021,
	title = {Autonomous Secure Remote Attestation even when all Used and to be Used Digital Keys Leak},
	url = {https://eprint.iacr.org/2021/602},
	abstract = {We provide a new remote attestation scheme for secure processor technology, which is secure in the presence of an All Digital State Observing ({ADSO}) adversary. To accomplish this, we obfuscate session signing keys using a silicon Physical Unclonable Function ({PUF}) with an extended interface that combines the {LPN}-{PUF} concept with a repetition code for small failure probabilities, and we introduce a new signature scheme that only needs a message dependent subset of a session signing key for computing a signature and whose signatures cannot be successfully forged even if one subset per session signing key leaks. Our solution for remote attestation shows that results computed by enclaves can be properly verified even when an {ADSO}-adversary is present. For \$N=2{\textasciicircum}l\$ sessions, implementation results show that signing takes \$934.9+0.6{\textbackslash}cdot l\$ ms and produces a signature of \$8.2+0.03{\textbackslash}cdot l\$ {KB}, and verification by a remote user takes \$118.2+0.4{\textbackslash}cdot l\$ ms. During initialization, generation of all session keys takes \$819.3 {\textbackslash}cdot N\$ ms and corresponding storage is \$3 {\textbackslash}cdot 10{\textasciicircum}\{-5\} + 0.12 {\textbackslash}cdot N\$ {MB}.},
	number = {602},
	author = {Dijk, Marten van and Gurevin, Deniz and Jin, Chenglu and Khan, Omer and Nguyen, Phuong Ha},
	urldate = {2021-05-28},
	date = {2021},
	keywords = {cryptographic protocols, One Time Signatures, Physical Unclonable Function, Remote Attestation, Secure Processor Architecture},
	file = {ePrint IACR Snapshot:C\:\\Users\\felix\\Zotero\\storage\\NPVJ285Z\\602.html:text/html;ePrint IACR Full Text PDF:C\:\\Users\\felix\\Zotero\\storage\\I74H8XMT\\Dijk et al. - 2021 - Autonomous Secure Remote Attestation even when all.pdf:application/pdf},
}

@report{androulaki_ibm_2021,
	title = {{IBM} Digital Health Pass Whitepaper: A Privacy-Respectful Platform for Proving Health Status},
	url = {https://eprint.iacr.org/2021/704},
	shorttitle = {{IBM} Digital Health Pass Whitepaper},
	abstract = {{IBM} Digital Health Pass ({IDHP}) is a technology developed by {IBM} offering the technical infrastructure to allow individuals to prove their {COVID}19-related health status (e.g., whether that individual was tested negative for {COVID}19, has been partially/fully vaccinated, or recovered from {COVID}19) to third parties in a secure and privacy-respectful way.

In a nutshell, {IBM} Digital Health Pass technology enables issuers, i.e., authorised healthcare providers onboarded to the system by health authorities of a given country or jurisdiction, to produce digital attestations about individuals’ health status. These attestations, called Health Certificates are issued to individuals, called subjects or holders, and are stored on a piece of paper or within subjects’ mobile phone wallets. Subjects can then demonstrate the authenticity of one or more of their Health Certificates to third parties of their choice called verifiers, when the necessity of demonstrating {COVID}19 related health status arises. Subjects can also demonstrate their association with each of their Health Certificates.

{IBM} Digital Health Pass is built around preserving individuals’ privacy as a first-class requirement, based on established public key cryptography concepts in a way that can easily scale to millions of Health Certificates.},
	number = {704},
	author = {Androulaki, Elli and Circiumaru, Ilie and Vico, Jesus Diaz and Prada, Miguel and Sorniotti, Alessandro and Stoecklin, Marc and Vukolic, Marko and Wallace, Marie},
	urldate = {2021-05-28},
	date = {2021},
	keywords = {applications, certification, decentralised identity, privacy, security},
	file = {ePrint IACR Snapshot:C\:\\Users\\felix\\Zotero\\storage\\BWHB586H\\704.html:text/html;ePrint IACR Full Text PDF:C\:\\Users\\felix\\Zotero\\storage\\3WBI5BEF\\Androulaki et al. - 2021 - IBM Digital Health Pass Whitepaper A Privacy-Resp.pdf:application/pdf},
}

@article{ProVerif,
	title = {Modeling and Verifying Security Protocols with the Applied Pi Calculus and {ProVerif}},
	volume = {1},
	issn = {2474-1558, 2474-1566},
	url = {https://www.nowpublishers.com/article/Details/SEC-004},
	doi = {10.1561/3300000004},
	abstract = {Modeling and Verifying Security Protocols with the Applied Pi Calculus and {ProVerif}},
	pages = {1--135},
	number = {1},
	journaltitle = {Foundations and Trends® in Privacy and Security},
	shortjournal = {{SEC}},
	author = {Blanchet, Bruno},
	urldate = {2021-09-23},
	date = {2016-10-30},
	file = {Full Text PDF:C\:\\Users\\felix\\Zotero\\storage\\FB6J6YSA\\Blanchet - 2016 - Modeling and Verifying Security Protocols with the.pdf:application/pdf},
}

@inproceedings{tamarin,
	location = {Berlin, Heidelberg},
	title = {The {TAMARIN} Prover for the Symbolic Analysis of Security Protocols},
	isbn = {978-3-642-39799-8},
	doi = {10.1007/978-3-642-39799-8_48},
	series = {Lecture Notes in Computer Science},
	abstract = {The Tamarin prover supports the automated, unbounded, symbolic analysis of security protocols. It features expressive languages for specifying protocols, adversary models, and properties, and support for efficient deduction and equational reasoning. We provide an overview of the tool and its applications.},
	pages = {696--701},
	booktitle = {Computer Aided Verification},
	publisher = {Springer},
	author = {Meier, Simon and Schmidt, Benedikt and Cremers, Cas and Basin, David},
	editor = {Sharygina, Natasha and Veith, Helmut},
	date = {2013},
	langid = {english},
	keywords = {Adversary Model, Bilinear Pairing, Equational Theory, Message Authentication Code, Security Protocol},
	file = {Springer Full Text PDF:C\:\\Users\\felix\\Zotero\\storage\\NXWK23CI\\Meier et al. - 2013 - The TAMARIN Prover for the Symbolic Analysis of Se.pdf:application/pdf},
}

@inproceedings{SeemsLegit,
	location = {New York, {NY}, {USA}},
	title = {Seems Legit: Automated Analysis of Subtle Attacks on Protocols that Use Signatures},
	isbn = {978-1-4503-6747-9},
	url = {https://doi.org/10.1145/3319535.3339813},
	doi = {10.1145/3319535.3339813},
	series = {{CCS} '19},
	shorttitle = {Seems Legit},
	abstract = {The standard definition of security for digital signatures - existential unforgeability - does not ensure certain properties that protocol designers might expect. For example, in many modern signature schemes, one signature may verify against multiple distinct public keys. It is left to protocol designers to ensure that the absence of these properties does not lead to attacks. Modern automated protocol analysis tools are able to provably exclude large classes of attacks on complex real-world protocols such as {TLS}{\textasciitilde}1.3 and 5G. However, their abstraction of signatures (implicitly) assumes much more than existential unforgeability, thereby missing several classes of practical attacks. We give a hierarchy of new formal models for signature schemes that captures these subtleties, and thereby allows us to analyse (often unexpected) behaviours of real-world protocols that were previously out of reach of symbolic analysis. We implement our models in the Tamarin Prover, yielding the first way to perform these analyses automatically, and validate them on several case studies. In the process, we find new attacks on {DRKey} and {SOAP}'s {WS}-Security, both protocols which were previously proven secure in traditional symbolic models.},
	pages = {2165--2180},
	booktitle = {Proceedings of the 2019 {ACM} {SIGSAC} Conference on Computer and Communications Security},
	publisher = {Association for Computing Machinery},
	author = {Jackson, Dennis and Cremers, Cas and Cohn-Gordon, Katriel and Sasse, Ralf},
	urldate = {2021-09-23},
	date = {2019-11-06},
	keywords = {automated analysis, digital signatures, formal verification, proverif, security protocols, symbolic model, tamarin prover},
	file = {Full Text PDF:C\:\\Users\\felix\\Zotero\\storage\\4PBKNCW2\\Jackson et al. - 2019 - Seems Legit Automated Analysis of Subtle Attacks .pdf:application/pdf},
}

@inproceedings{DYStar,
	title = {{DY}* : A Modular Symbolic Verification Framework for Executable Cryptographic Protocol Code},
	url = {https://hal.inria.fr/hal-03178425},
	shorttitle = {{DY}*},
	abstract = {We present {DY}*, a new formal verification framework for the symbolic security analysis of cryptographic protocol code written in the F* programming language. Unlike automated symbolic provers, our framework accounts for advanced protocol features like unbounded loops and mutable recursive data structures, as well as low-level implementation details like protocol state machines and message formats, which are often at the root of real-world attacks. Our work extends a long line of research on using dependent type systems for this task, but takes a fundamentally new approach by explicitly modeling the global trace-based semantics within the framework, hence bridging the gap between trace-based and type-based protocol analyses. This approach enables us to uniformly, precisely, and soundly model, for the first time using dependent types, long-lived mutable protocol state, equational theories, fine-grained dynamic corruption, and trace-based security properties like forward secrecy and post-compromise security. {DY}* is built as a library of F* modules that includes a model of low-level protocol execution, a Dolev-Yao symbolic attacker, and generic security abstractions and lemmas, all verified using F*. The library exposes a high-level {API} that facilitates succinct security proofs for protocol code. We demonstrate the effectiveness of this approach through a detailed symbolic security analysis of the Signal protocol that is based on an interoperable implementation of the protocol from prior work, and is the first mechanized proof of Signal to account for forward and post-compromise security over an unbounded number of protocol rounds.},
	eventtitle = {{EuroS}\&P 2021 - 6th {IEEE} European Symposium on Security and Privacy},
	author = {Bhargavan, Karthikeyan and Bichhawat, Abhishek and Do, Quoc and Hosseyni, Pedram and Küsters, Ralf and Schmitz, Guido and Würtele, Tim},
	urldate = {2021-09-23},
	date = {2021-09-06},
	langid = {english},
	file = {Full Text PDF:C\:\\Users\\felix\\Zotero\\storage\\QTCHF27C\\Bhargavan et al. - 2021 - DY  A Modular Symbolic Verification Framework fo.pdf:application/pdf},
}

@article{ACL2,
	title = {An industrial strength theorem prover for a logic based on Common Lisp},
	volume = {23},
	issn = {1939-3520},
	doi = {10.1109/32.588534},
	abstract = {{ACL}2 is a reimplemented extended version of R.S. Boyer and J.S. Moore's (1979; 1988) Nqthm and M. Kaufmann's (1988) Pc-Nqthm, intended for large scale verification projects. The paper deals primarily with how we scaled up Nqthm's logic to an industrial strength" programming language-namely, a large applicative subset of Common Lisp-while preserving the use of total functions within the logic. This makes it possible to run formal models efficiently while keeping the logic simple. We enumerate many other important features of {ACL}2 and we briefly summarize two industrial applications: a model of the Motorola {CAP} digital signal processing chip and the proof of the correctness of the kernel of the floating point division algorithm on the {AMD}5/sub K/86 microprocessor by Advanced Micro Devices, Inc.},
	pages = {203--213},
	number = {4},
	journaltitle = {{IEEE} Transactions on Software Engineering},
	author = {Kaufmann, M. and Moore, J.S.},
	date = {1997-04},
	keywords = {Automatic logic units, Digital signal processing chips, Functional programming, Kernel, Large-scale systems, Logic devices, Logic programming, Mathematics, Microprocessors, Signal processing algorithms},
	file = {IEEE Xplore Full Text PDF:C\:\\Users\\felix\\Zotero\\storage\\FKSFUSWX\\Kaufmann und Moore - 1997 - An industrial strength theorem prover for a logic .pdf:application/pdf},
}

@inproceedings{Viper,
	location = {Berlin, Heidelberg},
	title = {Viper: A Verification Infrastructure for Permission-Based Reasoning},
	isbn = {978-3-662-49121-8},
	url = {https://doi.org/10.1007/978-3-662-49122-5_2},
	doi = {10.1007/978-3-662-49122-5_2},
	series = {{VMCAI} 2016},
	shorttitle = {Viper},
	abstract = {The automation of verification techniques based on first-order logic specifications has benefitted greatly from verification infrastructures such as Boogie and Why. These offer an intermediate language that can express diverse language features and verification techniques, as well as back-end tools: in particular, verification condition generators. However, these infrastructures are not well suited to verification techniques based on separation logic and other permission logics, because they do not provide direct support for permissions and because existing tools for these logics often favour symbolic execution over verification condition generation. Consequently, tool support for these logics where available is typically developed independently for each technique, dramatically increasing the burden of developing automatic tools for permission-based verification. In this paper, we present a verification infrastructure whose intermediate language supports an expressive permission model natively. We provide tool support including two back-end verifiers: one based on symbolic execution, and one on verification condition generation; an inference tool based on abstract interpretion is currently under development. A wide range of existing verification techniques can be implemented via this infrastructure, alleviating much of the burden of building permission-based verifiers, and allowing the developers of higher-level reasoning techniques to focus their efforts at an appropriate level of abstraction.},
	pages = {41--62},
	booktitle = {Proceedings of the 17th International Conference on Verification, Model Checking, and Abstract Interpretation - Volume 9583},
	publisher = {Springer-Verlag},
	author = {Müller, Peter and Schwerhoff, Malte and Summers, Alexander J.},
	urldate = {2021-09-23},
	date = {2016-01-17},
	file = {Eingereichte Version:C\:\\Users\\felix\\Zotero\\storage\\Y5QHI7IF\\Müller et al. - 2016 - Viper A Verification Infrastructure for Permissio.pdf:application/pdf},
}

@book{Isabelle,
	location = {Berlin Heidelberg},
	title = {Isabelle/{HOL}: A Proof Assistant for Higher-Order Logic},
	isbn = {978-3-540-43376-7},
	url = {https://www.springer.com/gp/book/9783540433767},
	series = {Lecture Notes in Computer Science},
	shorttitle = {Isabelle/{HOL}},
	abstract = {This volume is a self-contained introduction to interactive proof in high- order logic ({HOL}), using the proof assistant Isabelle 2002. Compared with existing Isabelle documentation, it provides a direct route into higher-order logic, which most people prefer these days. It bypasses ?rst-order logic and minimizes discussion of meta-theory. It is written for potential users rather than for our colleagues in the research world. Another departure from previous documentation is that we describe Markus Wenzel’s proof script notation instead of {ML} tactic scripts. The l- ter make it easier to introduce new tactics on the ?y, but hardly anybody does that. Wenzel’s dedicated syntax is elegant, replacing for example eight simpli?cation tactics with a single method, namely simp, with associated - tions. The book has three parts. – The ?rst part, Elementary Techniques, shows how to model functional programs in higher-order logic. Early examples involve lists and the natural numbers. Most proofs are two steps long, consisting of induction on a chosen variable followed by the auto tactic. But even this elementary part covers such advanced topics as nested and mutual recursion. – The second part, Logic and Sets, presents a collection of lower-level tactics that you can use to apply rules selectively. It also describes I- belle/{HOL}’s treatment of sets, functions, and relations and explains how to de?ne sets inductively. One of the examples concerns the theory of model checking, and another is drawn from a classic textbook on formal languages.},
	publisher = {Springer-Verlag},
	author = {Nipkow, Tobias and Paulson, Lawrence C. and Wenzel, Markus},
	urldate = {2021-09-23},
	date = {2002},
	langid = {english},
}

@inproceedings{InteractiveSignalVerification,
	title = {A Formal Security Analysis of the Signal Messaging Protocol},
	doi = {10.1109/EuroSP.2017.27},
	abstract = {Signal is a new security protocol and accompanying app that provides end-to-end encryption for instant messaging. The core protocol has recently been adopted by {WhatsApp}, Facebook Messenger, and Google Allo among many others, the first two of these have at least 1 billion active users. Signal includes several uncommon security properties (such as "future secrecy" or "post-compromise security"), enabled by a novel technique called ratcheting in which session keys are updated with every message sent. Despite its importance and novelty, there has been little to no academic analysis of the Signal protocol. We conduct the first security analysis of Signal's key agreement and double ratchet as a multi-stage key exchange protocol. We extract from the implementation a formal description of the abstract protocol, and define a security model which can capture the "ratcheting" key update structure. We then prove the security of Signal's core in our model, demonstrating several standard security properties. We have found no major flaws in the design, and hope that our presentation and results can serve as a starting point for other analyses of this widely adopted protocol.},
	eventtitle = {2017 {IEEE} European Symposium on Security and Privacy ({EuroS} P)},
	pages = {451--466},
	booktitle = {2017 {IEEE} European Symposium on Security and Privacy ({EuroS} P)},
	author = {Cohn-Gordon, Katriel and Cremers, Cas and Dowling, Benjamin and Garratt, Luke and Stebila, Douglas},
	date = {2017-04},
	keywords = {authenticated key exchange, {DH}-{HEMTs}, Encryption, future secrecy, Instant messaging, messaging, multi-stage key exchange, post-compromise security, Protocols, provable security, Public key, Signal},
	file = {IEEE Xplore Full Text PDF:C\:\\Users\\felix\\Zotero\\storage\\BANN572I\\Cohn-Gordon et al. - 2017 - A Formal Security Analysis of the Signal Messaging.pdf:application/pdf},
}

@article{NeedhamSchroederAttack,
	title = {An attack on the Needham-Schroeder public-key authentication protocol},
	volume = {56},
	issn = {0020-0190},
	url = {https://www.sciencedirect.com/science/article/pii/0020019095001442},
	doi = {10.1016/0020-0190(95)00144-2},
	abstract = {In this paper we present an attack upon the Needham-Schroeder public-key authentication protocol. The attack allows an intruder to impersonate another agent.},
	pages = {131--133},
	number = {3},
	journaltitle = {Information Processing Letters},
	shortjournal = {Information Processing Letters},
	author = {Lowe, Gavin},
	urldate = {2021-09-23},
	date = {1995-11-10},
	langid = {english},
	keywords = {Authentication protocols, Distributed systems, Public-key cryptography, Security in digital systems},
	file = {ScienceDirect Full Text PDF:C\:\\Users\\felix\\Zotero\\storage\\M9AWQK7R\\Lowe - 1995 - An attack on the Needham-Schroeder public-key auth.pdf:application/pdf},
}

@article{NeedhamSchroeder,
	title = {Using encryption for authentication in large networks of computers},
	volume = {21},
	issn = {0001-0782},
	url = {https://doi.org/10.1145/359657.359659},
	doi = {10.1145/359657.359659},
	abstract = {Use of encryption to achieve authenticated communication in computer networks is discussed. Example protocols are presented for the establishment of authenticated connections, for the management of authenticated mail, and for signature verification and document integrity guarantee. Both conventional and public-key encryption algorithms are considered as the basis for protocols.},
	pages = {993--999},
	number = {12},
	journaltitle = {Communications of the {ACM}},
	shortjournal = {Commun. {ACM}},
	author = {Needham, Roger M. and Schroeder, Michael D.},
	urldate = {2021-09-23},
	date = {1978-12-01},
	keywords = {security, authentication, data encryption standard, encryption, networks, protocols, public-key cryptosystems},
	file = {Full Text PDF:C\:\\Users\\felix\\Zotero\\storage\\NA8DESIS\\Needham und Schroeder - 1978 - Using encryption for authentication in large netwo.pdf:application/pdf},
}

@inproceedings{ChannelCalculus,
	location = {Berlin, Heidelberg},
	title = {A Calculus for Secure Channel Establishment in Open Networks},
	isbn = {978-3-540-58618-0},
	series = {{ESORICS} '94},
	pages = {175--192},
	booktitle = {Proceedings of the Third European Symposium on Research in Computer Security},
	publisher = {Springer-Verlag},
	author = {Maurer, Ueli M. and Schmid, Pierre E.},
	urldate = {2021-09-23},
	date = {1994-11-07},
}

@online{SignalBlog,
	title = {Advanced cryptographic ratcheting},
	url = {https://signal.org/blog/advanced-ratcheting/},
	abstract = {At Open Whisper Systems, we’ve been working on improving our encrypted asynchronous chat protocol for {TextSecure}.The {TextSecure} protocol was originally a derivative of {OTR}, with minor changes to accommodate it for transports with constraints like {SMS} or Push. Some of the recent changes we’ve mad...},
	titleaddon = {Signal Messenger},
	author = {Marlinspike, Moxie},
	urldate = {2021-09-23},
	date = {2013-11-26},
	langid = {english},
}

@article{SomethingYou,
	title = {Comparing passwords, tokens, and biometrics for user authentication},
	volume = {91},
	issn = {1558-2256},
	doi = {10.1109/JPROC.2003.819611},
	abstract = {For decades, the password has been the standard means for user authentication on computers. However, as users are required to remember more, longer, and changing passwords, it is evident that a more convenient and secure solution to user authentication is necessary. This paper examines passwords, security tokens, and biometrics-which we collectively call authenticators-and compares these authenticators and their combinations. We examine their effectiveness against several attacks and suitability for particular security specifications such as compromise detection and nonrepudiation. Examples of authenticator combinations and protocols are described to show tradeoffs and solutions that meet chosen, practical requirements. The paper endeavors to offer a comprehensive picture of user authentication solutions for the purposes of evaluating options for use and identifying deficiencies requiring further research.},
	pages = {2021--2040},
	number = {12},
	journaltitle = {Proceedings of the {IEEE}},
	author = {O'Gorman, L.},
	date = {2003-12},
	keywords = {Protocols, Authentication, Biometrics, Computer networks, Humans, Identity management systems, Internet, Protection, Security, Web sites},
	file = {IEEE Xplore Full Text PDF:C\:\\Users\\felix\\Zotero\\storage\\PMT944YG\\O'Gorman - 2003 - Comparing passwords, tokens, and biometrics for us.pdf:application/pdf},
}

@online{BlogADEM,
	title = {Signaling legal protection during cyber warfare: an authenticated digital emblem},
	url = {https://blogs.icrc.org/law-and-policy/2021/09/21/legal-protection-cyber-warfare-digital-emblem/},
	shorttitle = {Signaling legal protection during cyber warfare},
	abstract = {Warfare increasingly takes place in cyberspace. Could an ‘Authenticated Digital {EMblem}’ signal protected objects in an armed conflict?},
	titleaddon = {Humanitarian Law \& Policy Blog},
	author = {Linker, Felix and Basin, David},
	urldate = {2021-09-23},
	date = {2021-09-21},
	langid = {american},
}

@article{SMSAuthInsecure,
	title = {Security Analysis of {SMS} as a Second Factor of Authentication: The challenges of multifactor authentication based on {SMS}, including cellular security deficiencies, {SS}7 exploits, and {SIM} swapping},
	volume = {18},
	issn = {1542-7730},
	url = {https://doi.org/10.1145/3424302.3425909},
	doi = {10.1145/3424302.3425909},
	shorttitle = {Security Analysis of {SMS} as a Second Factor of Authentication},
	abstract = {Despite their popularity and ease of use, {SMS}-based authentication tokens are arguably one of the least secure forms of two-factor authentication. This does not imply, however, that it is an invalid method for securing an online account. The current security landscape is very different from that of two decades ago. Regardless of the critical nature of an online account or the individual who owns it, using a second form of authentication should always be the default option, regardless of the method chosen. In the wake of a large number of leaks and other intrusions, there are many username and password combinations out there in the wrong hands that make password spraying attacks cheap and easy to accomplish.},
	pages = {Pages 20:37--Pages 20:60},
	number = {4},
	journaltitle = {Queue},
	shortjournal = {Queue},
	author = {Jover, Roger Piqueras},
	urldate = {2021-09-23},
	date = {2020-08-31},
	file = {Full Text PDF:C\:\\Users\\felix\\Zotero\\storage\\ZWM2UGG7\\Jover - 2020 - Security Analysis of SMS as a Second Factor of Aut.pdf:application/pdf},
}

@online{noauthor_network_nodate,
	title = {Network Security: Private Communication in a Public World, 2nd Edition},
	url = {https://www.pearson.com/content/one-dot-com/one-dot-com/us/en/higher-education/program.html},
	shorttitle = {Network Security},
	abstract = {Network Security: Private Communication in a Public World, 2nd Edition},
	urldate = {2021-09-23},
	langid = {english},
}

@book{NetworkSecurityBook,
	location = {Upper Saddle River, {NJ}},
	edition = {2nd ed., 14th printing},
	title = {Network security private communication in a public world},
	isbn = {978-0-13-046019-6},
	series = {Prentice Hall series in computer networking and distributed systems The Radia Perlman series in computer networking and security},
	pagetotal = {713},
	publisher = {Prentice Hall {PTR}},
	author = {Kaufman, Charlie and Perlman, Radia and Speciner, Mike},
	date = {2011},
}

@inproceedings{AuthenticationSpec,
	title = {A hierarchy of authentication specifications},
	doi = {10.1109/CSFW.1997.596782},
	abstract = {Many security protocols have the aim of authenticating one agent to another. Yet there is no clear consensus in the academic literature about precisely what "authentication" means. We suggest that the appropriate authentication requirement will depend upon the use to which the protocol is put, and identify several possible definitions of "authentication". We formalize each definition using the process algebra {CSP}, use this formalism to study their relative strengths, and show how the model checker {FDR} can be used to test whether a system running the protocol meets such a specification.},
	eventtitle = {Proceedings 10th Computer Security Foundations Workshop},
	pages = {31--43},
	booktitle = {Proceedings 10th Computer Security Foundations Workshop},
	author = {Lowe, G.},
	date = {1997-06},
	keywords = {Mathematics, Protocols, Authentication, Algebra, Computer science, Computer security, Control systems, Stress, System testing},
	file = {IEEE Xplore Full Text PDF:C\:\\Users\\felix\\Zotero\\storage\\SFHTZ52S\\Lowe - 1997 - A hierarchy of authentication specifications.pdf:application/pdf},
}

@inproceedings{WebPKIMissingLinks,
	title = {{SoK}: Delegation and Revocation, the Missing Links in the Web's Chain of Trust},
	doi = {10.1109/EuroSP48549.2020.00046},
	shorttitle = {{SoK}},
	abstract = {The ability to quickly revoke a compromised key is critical to the security of any public-key infrastructure. Regrettably, most traditional certificate revocation schemes suffer from latency, availability, or privacy problems. These problems are exacerbated by the lack of a native delegation mechanism in {TLS}, which increasingly leads domain owners to engage in dangerous practices such as sharing their private keys with third parties. We analyze solutions that address the longstanding delegation and revocation shortcomings of the web {PKI}, with a focus on approaches that directly affect the chain of trust (i.e., the X.509 certification path). For this purpose, we propose a 19-criteria framework for characterizing revocation and delegation schemes. We also show that combining short-lived delegated credentials or proxy certificates with an appropriate revocation system would solve several pressing problems.},
	eventtitle = {2020 {IEEE} European Symposium on Security and Privacy ({EuroS} P)},
	pages = {624--638},
	booktitle = {2020 {IEEE} European Symposium on Security and Privacy ({EuroS} P)},
	author = {Chuat, Laurent and Abdou, {AbdelRahman} and Sasse, Ralf and Sprenger, Christoph and Basin, David and Perrig, Adrian},
	date = {2020-09},
	keywords = {content-delivery network ({CDN}), delegation, digital certificate, proxy certificate, public-key infrastructure ({PKI}), revocation},
	file = {IEEE Xplore Full Text PDF:C\:\\Users\\felix\\Zotero\\storage\\XY6GDJM7\\Chuat et al. - 2020 - SoK Delegation and Revocation, the Missing Links .pdf:application/pdf},
}

@online{noauthor_rfc4556_nodate,
	title = {rfc4556},
	url = {https://datatracker.ietf.org/doc/html/rfc4556.html},
	urldate = {2021-09-23},
	file = {rfc4556:C\:\\Users\\felix\\Zotero\\storage\\5DB2DVRP\\rfc4556.html:text/html},
}

@online{noauthor_rfc4556_nodate-1,
	title = {rfc4556},
	url = {https://datatracker.ietf.org/doc/html/rfc4556.html},
	urldate = {2021-09-23},
}

@report{KerberosRFC,
	title = {Public Key Cryptography for Initial Authentication in Kerberos ({PKINIT})},
	url = {https://datatracker.ietf.org/doc/rfc4556},
	abstract = {This document describes protocol extensions (hereafter called {PKINIT}) to the Kerberos protocol specification. These extensions provide a method for integrating public key cryptography into the initial authentication exchange, by using asymmetric-key signature and/or encryption algorithms in pre-authentication data fields. [{STANDARDS}-{TRACK}]},
	number = {{RFC} 4556},
	institution = {Internet Engineering Task Force},
	type = {Request for Comments},
	author = {Tung, Brian and Zhu, Larry},
	urldate = {2021-09-23},
	date = {2006-06},
	doi = {10.17487/RFC4556},
	note = {Num Pages: 42},
	file = {Full Text PDF:C\:\\Users\\felix\\Zotero\\storage\\QQ4V9WJQ\\Tung und Zhu - 2006 - Public Key Cryptography for Initial Authentication.pdf:application/pdf},
}

@report{ACMERFC,
	title = {Automatic Certificate Management Environment ({ACME})},
	url = {https://datatracker.ietf.org/doc/rfc8555},
	abstract = {Public Key Infrastructure using X.509 ({PKIX}) certificates are used for a number of purposes, the most significant of which is the authentication of domain names. Thus, certification authorities ({CAs}) in the Web {PKI} are trusted to verify that an applicant for a certificate legitimately represents the domain name(s) in the certificate. As of this writing, this verification is done through a collection of ad hoc mechanisms. This document describes a protocol that a {CA} and an applicant can use to automate the process of verification and certificate issuance. The protocol also provides facilities for other certificate management functions, such as certificate revocation.},
	number = {{RFC} 8555},
	institution = {Internet Engineering Task Force},
	type = {Request for Comments},
	author = {Barnes, Richard and Hoffman-Andrews, Jacob and {McCarney}, Daniel and Kasten, James},
	urldate = {2021-09-23},
	date = {2019-03},
	doi = {10.17487/RFC8555},
	note = {Num Pages: 95},
	file = {Full Text PDF:C\:\\Users\\felix\\Zotero\\storage\\KRCJDFP4\\Barnes et al. - 2019 - Automatic Certificate Management Environment (ACME.pdf:application/pdf},
}

@report{TLSRFC,
	title = {The Transport Layer Security ({TLS}) Protocol Version 1.3},
	url = {https://datatracker.ietf.org/doc/rfc8446},
	abstract = {This document specifies version 1.3 of the Transport Layer Security ({TLS}) protocol. {TLS} allows client/server applications to communicate over the Internet in a way that is designed to prevent eavesdropping, tampering, and message forgery. This document updates {RFCs} 5705 and 6066, and obsoletes {RFCs} 5077, 5246, and 6961. This document also specifies new requirements for {TLS} 1.2 implementations.},
	number = {{RFC} 8446},
	institution = {Internet Engineering Task Force},
	type = {Request for Comments},
	author = {Rescorla, Eric},
	urldate = {2021-09-23},
	date = {2018-08},
	doi = {10.17487/RFC8446},
	note = {Num Pages: 160},
	file = {Full Text PDF:C\:\\Users\\felix\\Zotero\\storage\\7D7PSPJR\\Rescorla - 2018 - The Transport Layer Security (TLS) Protocol Versio.pdf:application/pdf},
}

@report{WebAuthN,
	title = {Web Authentication: An {API} for accessing Public Key Credentials Level 1},
	url = {https://www.w3.org/TR/2019/REC-webauthn-1-20190304},
	abstract = {This specification defines an {API} enabling the creation and use of strong, attested, scoped, public key-based credentials by web applications, for the purpose of strongly authenticating users. Conceptually, one or more public key credentials, each scoped to a given {WebAuthn} Relying Party, are created by and bound to authenticators as requested by the web application. The user agent mediates access to authenticators and their public key credentials in order to preserve user privacy. Authenticators are responsible for ensuring that no operation is performed without user consent. Authenticators provide cryptographic proof of their properties to Relying Parties via attestation. This specification also describes the functional model for {WebAuthn} conformant authenticators, including their signature and attestation functionality.},
	institution = {W3C},
	type = {W3C Recommendation},
	author = {Balfanz, Dirk and Szeskis, Alexei and Hodges, Jeff and Jones, J.C. and Jones, Michael B. and Kumar, Akshay and Liao, Angelo and Lindemann, Rolf and Lundberg, Emil},
	urldate = {2021-09-23},
	date = {2019-03-04},
}

@inproceedings{TamarinTLS,
	location = {New York, {NY}, {USA}},
	title = {A Comprehensive Symbolic Analysis of {TLS} 1.3},
	isbn = {978-1-4503-4946-8},
	url = {https://doi.org/10.1145/3133956.3134063},
	doi = {10.1145/3133956.3134063},
	series = {{CCS} '17},
	abstract = {The {TLS} protocol is intended to enable secure end-to-end communication over insecure networks, including the Internet. Unfortunately, this goal has been thwarted a number of times throughout the protocol's tumultuous lifetime, resulting in the need for a new version of the protocol, namely {TLS} 1.3. Over the past three years, in an unprecedented joint design effort with the academic community, the {TLS} Working Group has been working tirelessly to enhance the security of {TLS}. We further this effort by constructing the most comprehensive, faithful, and modular symbolic model of the {TLS}{\textasciitilde}1.3 draft 21 release candidate, and use the {TAMARIN} prover to verify the claimed {TLS}{\textasciitilde}1.3 security requirements, as laid out in draft 21 of the specification. In particular, our model covers all handshake modes of {TLS} 1.3. Our analysis reveals an unexpected behaviour, which we expect will inhibit strong authentication guarantees in some implementations of the protocol. In contrast to previous models, we provide a novel way of making the relation between the {TLS} specification and our model explicit: we provide a fully annotated version of the specification that clarifies what protocol elements we modelled, and precisely how we modelled these elements. We anticipate this model artifact to be of great benefit to the academic community and the {TLS} Working Group alike.},
	pages = {1773--1788},
	booktitle = {Proceedings of the 2017 {ACM} {SIGSAC} Conference on Computer and Communications Security},
	publisher = {Association for Computing Machinery},
	author = {Cremers, Cas and Horvat, Marko and Hoyland, Jonathan and Scott, Sam and van der Merwe, Thyla},
	urldate = {2021-09-23},
	date = {2017-10-30},
	keywords = {authenticated key exchange, symbolic verification, tls{\textasciitilde}1.3},
	file = {Full Text PDF:C\:\\Users\\felix\\Zotero\\storage\\KQUE952T\\Cremers et al. - 2017 - A Comprehensive Symbolic Analysis of TLS 1.3.pdf:application/pdf},
}

@inproceedings{FStar,
	location = {New York, {NY}, {USA}},
	title = {Dependent types and multi-monadic effects in F*},
	isbn = {978-1-4503-3549-2},
	url = {https://doi.org/10.1145/2837614.2837655},
	doi = {10.1145/2837614.2837655},
	series = {{POPL} '16},
	abstract = {We present a new, completely redesigned, version of F*, a language that works both as a proof assistant as well as a general-purpose, verification-oriented, effectful programming language. In support of these complementary roles, F* is a dependently typed, higher-order, call-by-value language with \_primitive\_ effects including state, exceptions, divergence and {IO}. Although primitive, programmers choose the granularity at which to specify effects by equipping each effect with a monadic, predicate transformer semantics. F* uses this to efficiently compute weakest preconditions and discharges the resulting proof obligations using a combination of {SMT} solving and manual proofs. Isolated from the effects, the core of F* is a language of pure functions used to write specifications and proof terms---its consistency is maintained by a semantic termination check based on a well-founded order. We evaluate our design on more than 55,000 lines of F* we have authored in the last year, focusing on three main case studies. Showcasing its use as a general-purpose programming language, F* is programmed (but not verified) in F*, and bootstraps in both {OCaml} and F\#. Our experience confirms F*'s pay-as-you-go cost model: writing idiomatic {ML}-like code with no finer specifications imposes no user burden. As a verification-oriented language, our most significant evaluation of F* is in verifying several key modules in an implementation of the {TLS}-1.2 protocol standard. For the modules we considered, we are able to prove more properties, with fewer annotations using F* than in a prior verified implementation of {TLS}-1.2. Finally, as a proof assistant, we discuss our use of F* in mechanizing the metatheory of a range of lambda calculi, starting from the simply typed lambda calculus to System F-omega and even micro-F*, a sizeable fragment of F* itself---these proofs make essential use of F*'s flexible combination of {SMT} automation and constructive proofs, enabling a tactic-free style of programming and proving at a relatively large scale.},
	pages = {256--270},
	booktitle = {Proceedings of the 43rd Annual {ACM} {SIGPLAN}-{SIGACT} Symposium on Principles of Programming Languages},
	publisher = {Association for Computing Machinery},
	author = {Swamy, Nikhil and Hriţcu, Cătălin and Keller, Chantal and Rastogi, Aseem and Delignat-Lavaud, Antoine and Forest, Simon and Bhargavan, Karthikeyan and Fournet, Cédric and Strub, Pierre-Yves and Kohlweiss, Markulf and Zinzindohoue, Jean-Karim and Zanella-Béguelin, Santiago},
	urldate = {2021-09-23},
	date = {2016-01-11},
	keywords = {effectful programming, proof assistants, verification},
	file = {Full Text PDF:C\:\\Users\\felix\\Zotero\\storage\\Z2IDLMR5\\Swamy et al. - 2016 - Dependent types and multi-monadic effects in F.pdf:application/pdf},
}

@article{Igloo,
	title = {Igloo: soundly linking compositional refinement and separation logic for distributed system verification},
	volume = {4},
	url = {https://doi.org/10.1145/3428220},
	doi = {10.1145/3428220},
	shorttitle = {Igloo},
	abstract = {Lighthouse projects like {CompCert}, {seL}4, {IronFleet}, and {DeepSpec} have demonstrated that full system verification is feasible by establishing a refinement between an abstract system specification and an executable implementation. Existing approaches however impose severe restrictions on the abstract system specifications due to their limited expressiveness or versatility, or on the executable code due to their use of suboptimal code extraction or inexpressive program logics. We propose a novel methodology that combines the compositional refinement of event-based models of distributed systems with the verification of full-fledged program code using expressive separation logics, which support features of realistic programming languages like heap data structures and concurrency. Our main technical contribution is a formal framework that soundly relates event-based system models to program specifications in separation logics. This enables protocol development tools to soundly interoperate with program verifiers to establish a refinement between the model and the code. We formalized our framework, Igloo, in Isabelle/{HOL}. We report on three case studies, a leader election protocol, a replication protocol, and a security protocol, for which we refine formal requirements into program specifications that we implement in Java and Python and prove correct using the {VeriFast} and Nagini tools.},
	pages = {152:1--152:31},
	issue = {{OOPSLA}},
	journaltitle = {Proceedings of the {ACM} on Programming Languages},
	shortjournal = {Proc. {ACM} Program. Lang.},
	author = {Sprenger, Christoph and Klenze, Tobias and Eilers, Marco and Wolf, Felix A. and Müller, Peter and Clochard, Martin and Basin, David},
	urldate = {2021-09-23},
	date = {2020-11-13},
	keywords = {security protocols, compositional refinement, distributed systems, end-to-end verification, fault-tolerance, higher-order logic, leader election, separation logic, tool interoperability},
	file = {Full Text PDF:C\:\\Users\\felix\\Zotero\\storage\\8RKNUZTT\\Sprenger et al. - 2020 - Igloo soundly linking compositional refinement an.pdf:application/pdf},
}

@inproceedings{Coniks,
	title = {{CONIKS}: Bringing Key Transparency to End Users},
	isbn = {978-1-939133-11-3},
	url = {https://www.usenix.org/conference/usenixsecurity15/technical-sessions/presentation/melara},
	shorttitle = {\{{CONIKS}\}},
	eventtitle = {24th \{{USENIX}\} Security Symposium (\{{USENIX}\} Security 15)},
	pages = {383--398},
	author = {Melara, Marcela S. and Blankstein, Aaron and Bonneau, Joseph and Felten, Edward W. and Freedman, Michael J.},
	urldate = {2021-09-24},
	date = {2015},
	langid = {english},
	file = {Full Text PDF:C\:\\Users\\felix\\Zotero\\storage\\VGKH7XF2\\Melara et al. - 2015 - \{CONIKS\} Bringing Key Transparency to End Users.pdf:application/pdf},
}

@inproceedings{ClaimChain,
	location = {New York, {NY}, {USA}},
	title = {{ClaimChain}: Improving the Security and Privacy of In-band Key Distribution for Messaging},
	isbn = {978-1-4503-5989-4},
	url = {https://doi.org/10.1145/3267323.3268947},
	doi = {10.1145/3267323.3268947},
	series = {{WPES}'18},
	shorttitle = {{ClaimChain}},
	abstract = {The social demand for email end-to-end encryption is barely supported by mainstream service providers. Autocrypt is a new community-driven open specification for e-mail encryption that attempts to respond to this demand. In Autocrypt the encryption keys are attached directly to messages, and thus the encryption can be implemented by email clients without any collaboration of the providers. The decentralized nature of this in-band key distribution, however, makes it prone to man-in-the-middle attacks and can leak the social graph of users. To address this problem we introduce {ClaimChain}, a cryptographic construction for privacy-preserving authentication of public keys. Users store claims about their identities and keys, as well as their beliefs about others, in {ClaimChains}. These chains form authenticated decentralized repositories that enable users to prove the authenticity of both their keys and the keys of their contacts. {ClaimChains} are encrypted, and therefore protect the stored information, such as keys and contact identities, from prying eyes. At the same time, {ClaimChain} implements mechanisms to provide strong non-equivocation properties, discouraging malicious actors from distributing conflicting or inauthentic claims. We implemented {ClaimChain} and we show that it offers reasonable performance, low overhead, and authenticity guarantees.},
	pages = {86--103},
	booktitle = {Proceedings of the 2018 Workshop on Privacy in the Electronic Society},
	publisher = {Association for Computing Machinery},
	author = {Kulynych, Bogdan and Lueks, Wouter and Isaakidis, Marios and Danezis, George and Troncoso, Carmela},
	urldate = {2021-09-24},
	date = {2018-01-15},
	keywords = {privacy, decentralization, e-mail encryption, key distribution},
	file = {Full Text PDF:C\:\\Users\\felix\\Zotero\\storage\\I7I4T2GY\\Kulynych et al. - 2018 - ClaimChain Improving the Security and Privacy of .pdf:application/pdf},
}

@book{AlloyBook,
	location = {Cambridge, {MA}, {USA}},
	title = {Software Abstractions: Logic, Language, and Analysis},
	isbn = {978-0-262-10114-1},
	shorttitle = {Software Abstractions},
	abstract = {A new approach to software verification introduces Alloy, a language that captures the essence of software abstraction with an analysis that is fully automated.},
	pagetotal = {366},
	publisher = {{MIT} Press},
	author = {Jackson, Daniel},
	date = {2006-03-24},
	langid = {english},
}

@article{TLAPlus,
	title = {Hybrid Systems in {TLA}+},
	volume = {736},
	url = {https://www.microsoft.com/en-us/research/publication/hybrid-systems-tla/},
	abstract = {In the early 90s, hybrid systems became a fashionable topic in formal methods. Theoreticians typically respond to a new problem domain by inventing new formalisms. Physicists don’t have to revise the theory of differential equations every time they study a new kind of system, and computer scientists shouldn’t have to change their formalisms when they […]},
	pages = {77--102},
	journaltitle = {Hybrid Systems, Robert L. Grossman, Anil Nerode, Hans Rischel, and Anders P. Ravn, editors. Lecture Notes in Computer Science, Springer-Verlag},
	author = {Lamport, Leslie},
	urldate = {2021-09-24},
	date = {1993-04-06},
	langid = {american},
	file = {Full Text PDF:C\:\\Users\\felix\\Zotero\\storage\\TMQZEL3B\\Lamport - 1993 - Hybrid Systems in TLA+.pdf:application/pdf},
}

@article{ThesisInaKraan,
	title = {Proof planning for logic program synthesis},
	url = {https://era.ed.ac.uk/handle/1842/34920},
	abstract = {The area of logic program synthesis is attracting increased interest. Most efforts
have concentrated on applying techniques from functional program synthesis to
logic program synthesis. This thesis investigates a new approach: Synthesizing
logic programs automatically via middle-out reasoning in proof planning.},
	author = {Kraan, Ina},
	urldate = {2021-09-24},
	date = {1994},
	langid = {english},
	note = {Accepted: 2019-02-15T14:32:46Z
Publisher: The University of Edinburgh},
	file = {Full Text PDF:C\:\\Users\\felix\\Zotero\\storage\\E9NHVQK3\\Kraan - 1994 - Proof planning for logic program synthesis.pdf:application/pdf},
}

@article{NQTHM,
	title = {The Boyer-Moore theorem prover and its interactive enhancement},
	volume = {29},
	issn = {0898-1221},
	url = {https://www.sciencedirect.com/science/article/pii/0898122194002157},
	doi = {10.1016/0898-1221(94)00215-7},
	abstract = {The so-called Boyer-Moore Theorem Prover (otherwise known as Nqthm) has been used to perform a variety of verification tasks for two decades. We give an overview of both this system and an interactive enhancement of it, Pc-Nqthm, from a number of perspectives. First, we introduce the logic in which theorems are proved. Then, we briefly describe the two mechanized theorem proving systems. Next, we present a simple but illustrative example in some detail in order to give an impression of how these systems may be used successfully. Finally, we give extremely short descriptions of a large number of applications of these systems, in order to give an idea of the breadth of their uses. This paper is intended as an informal introduction to systems that have been described in detail and similarly summarized in many other books and papers; no new results are reported here. Our intention here is to present Nqthm to a new audience.},
	pages = {27--62},
	number = {2},
	journaltitle = {Computers \& Mathematics with Applications},
	shortjournal = {Computers \& Mathematics with Applications},
	author = {Boyer, R. S. and Kaufmann, M. and Moore, J. S.},
	urldate = {2021-09-24},
	date = {1995-01-01},
	langid = {english},
	keywords = {Boyer-Moore Theorem Prover, Interactive theorem proving, Nqthm, {PC}-Nqthm},
	file = {ScienceDirect Full Text PDF:C\:\\Users\\felix\\Zotero\\storage\\NFFHVKCA\\Boyer et al. - 1995 - The Boyer-Moore theorem prover and its interactive.pdf:application/pdf},
}

@online{noauthor_specifications_2007,
	title = {Specifications {\textbar} {OpenID}},
	url = {https://openid.net/developers/specs/},
	abstract = {{OpenID} specifications are developed by {OpenID} working groups and go through three phases: Drafts, Implementer’s Drafts, and Final Specifications. Implementer’s Drafts and Final Specifications provide intellectual property protections to implementers. Final Specifications are {OpenID} Foundation standards. Final Specifications {OpenID} Connect specifications: {OpenID} Connect Core – Defines the core {OpenID} Connect functionality: authentication built on top […]},
	urldate = {2021-09-24},
	date = {2007-10-09},
	langid = {american},
}

@report{OpenIdConnect,
	title = {{OpenID} Connect Core 1.0 incorporating errata set 1},
	url = {https://openid.net/specs/openid-connect-core-1_0.html},
	abstract = {{OpenID} Connect 1.0 is a simple identity layer on top of the {OAuth} 2.0 protocol. It enables Clients to verify the identity of the End-User based on the authentication performed by an Authorization Server, as well as to obtain basic profile information about the End-User in an interoperable and {REST}-like manner.

This specification defines the core {OpenID} Connect functionality: authentication built on top of {OAuth} 2.0 and the use of Claims to communicate information about the End-User. It also describes the security and privacy considerations for using {OpenID} Connect.},
	author = {Sakimura, N. and Bradley, J. and Jones, M. and de Medeiros, B. and Mortimore, C.},
	urldate = {2021-09-24},
	date = {2014-11-08},
}

@report{OAuthRFC,
	title = {The {OAuth} 2.0 Authorization Framework},
	url = {https://datatracker.ietf.org/doc/rfc6749},
	abstract = {The {OAuth} 2.0 authorization framework enables a third-party application to obtain limited access to an {HTTP} service, either on behalf of a resource owner by orchestrating an approval interaction between the resource owner and the {HTTP} service, or by allowing the third-party application to obtain access on its own behalf. This specification replaces and obsoletes the {OAuth} 1.0 protocol described in {RFC} 5849. [{STANDARDS}-{TRACK}]},
	number = {{RFC} 6749},
	institution = {Internet Engineering Task Force},
	type = {Request for Comments},
	author = {Hardt, Dick},
	urldate = {2021-09-24},
	date = {2012-10},
	doi = {10.17487/RFC6749},
	note = {Num Pages: 76},
	file = {Full Text PDF:C\:\\Users\\felix\\Zotero\\storage\\AK5KDWUG\\Hardt - 2012 - The OAuth 2.0 Authorization Framework.pdf:application/pdf},
}

@article{MastercardTamarin,
	title = {The {EMV} Standard: Break, Fix, Verify},
	url = {http://arxiv.org/abs/2006.08249},
	shorttitle = {The {EMV} Standard},
	abstract = {{EMV} is the international protocol standard for smartcard payment and is used in over 9 billion cards worldwide. Despite the standard's advertised security, various issues have been previously uncovered, deriving from logical flaws that are hard to spot in {EMV}'s lengthy and complex specification, running over 2,000 pages. We formalize a comprehensive symbolic model of {EMV} in Tamarin, a state-of-the-art protocol verifier. Our model is the first that supports a fine-grained analysis of all relevant security guarantees that {EMV} is intended to offer. We use our model to automatically identify flaws that lead to two critical attacks: one that defrauds the cardholder and a second that defrauds the merchant. First, criminals can use a victim's Visa contactless card to make payments for amounts that require cardholder verification, without knowledge of the card's {PIN}. We built a proof-of-concept Android application and successfully demonstrated this attack on real-world payment terminals. Second, criminals can trick the terminal into accepting an unauthentic offline transaction, which the issuing bank should later decline, after the criminal has walked away with the goods. This attack is possible for implementations following the standard, although we did not test it on actual terminals for ethical reasons. Finally, we propose and verify improvements to the standard that prevent these attacks, as well as any other attacks that violate the considered security properties. The proposed improvements can be easily implemented in the terminals and do not affect the cards in circulation.},
	journaltitle = {{arXiv}:2006.08249 [cs]},
	author = {Basin, David and Sasse, Ralf and Toro-Pozo, Jorge},
	urldate = {2021-09-24},
	date = {2021-02-17},
	eprinttype = {arxiv},
	eprint = {2006.08249},
	keywords = {Computer Science - Cryptography and Security},
	file = {arXiv Fulltext PDF:C\:\\Users\\felix\\Zotero\\storage\\ATFTP2SG\\Basin et al. - 2021 - The EMV Standard Break, Fix, Verify.pdf:application/pdf},
}

@inproceedings{Z3,
	location = {Berlin, Heidelberg},
	title = {Z3: An Efficient {SMT} Solver},
	isbn = {978-3-540-78800-3},
	doi = {10.1007/978-3-540-78800-3_24},
	series = {Lecture Notes in Computer Science},
	shorttitle = {Z3},
	abstract = {Satisfiability Modulo Theories ({SMT}) problem is a decision problem for logical first order formulas with respect to combinations of background theories such as: arithmetic, bit-vectors, arrays, and uninterpreted functions. Z3 is a new and efficient {SMT} Solver freely available from Microsoft Research. It is used in various software verification and analysis applications.},
	pages = {337--340},
	booktitle = {Tools and Algorithms for the Construction and Analysis of Systems},
	publisher = {Springer},
	author = {de Moura, Leonardo and Bjørner, Nikolaj},
	editor = {Ramakrishnan, C. R. and Rehof, Jakob},
	date = {2008},
	langid = {english},
	keywords = {Bound Model Check, Linear Arithmetic, Predicate Abstraction, Symbolic Execution, Theory Solver},
	file = {Springer Full Text PDF:C\:\\Users\\felix\\Zotero\\storage\\9UMMYANV\\de Moura und Bjørner - 2008 - Z3 An Efficient SMT Solver.pdf:application/pdf},
}

@inproceedings{nuXmv,
	location = {Cham},
	title = {The {nuXmv} Symbolic Model Checker},
	isbn = {978-3-319-08867-9},
	doi = {10.1007/978-3-319-08867-9_22},
	series = {Lecture Notes in Computer Science},
	abstract = {This paper describes the {nuXmv} symbolic model checker for finite- and infinite-state synchronous transition systems. {nuXmv} is the evolution of the {nuXmv} open source model checker. It builds on and extends {nuXmv} along two main directions. For finite-state systems it complements the basic verification techniques of {nuXmv} with state-of-the-art verification algorithms. For infinite-state systems, it extends the {nuXmv} language with new data types, namely Integers and Reals, and it provides advanced {SMT}-based model checking techniques.Besides extended functionalities, {nuXmv} has been optimized in terms of performance to be competitive with the state of the art. {nuXmv} has been used in several industrial projects as verification back-end, and it is the basis for several extensions to cope with requirements analysis, contract based design, model checking of hybrid systems, safety assessment, and software model checking.},
	pages = {334--342},
	booktitle = {Computer Aided Verification},
	publisher = {Springer International Publishing},
	author = {Cavada, Roberto and Cimatti, Alessandro and Dorigatti, Michele and Griggio, Alberto and Mariotti, Alessandro and Micheli, Andrea and Mover, Sergio and Roveri, Marco and Tonetta, Stefano},
	editor = {Biere, Armin and Bloem, Roderick},
	date = {2014},
	langid = {english},
	keywords = {Predicate Abstraction, Model Check, Model Check Problem, Software Model Check, Symbolic Model Checker},
	file = {Springer Full Text PDF:C\:\\Users\\felix\\Zotero\\storage\\GKIWX34X\\Cavada et al. - 2014 - The nuXmv Symbolic Model Checker.pdf:application/pdf},
}

@report{5GSpec,
	title = {Security architecture and procedures for 5G System},
	url = {https://www.etsi.org/deliver/etsi_ts/133500_133599/133501/16.07.01_60/ts_133501v160701p.pdf},
	shorttitle = {5G},
	number = {{TS} 133 501 V16.7.1},
	institution = {3GPP},
	urldate = {2021-09-28},
	date = {2021-08},
}

@incollection{InductionBundy,
	location = {Amsterdam},
	title = {Chapter 13 - The Automation of Proof by Mathematical Induction},
	isbn = {978-0-444-50813-3},
	url = {https://www.sciencedirect.com/science/article/pii/B9780444508133500151},
	series = {Handbook of Automated Reasoning},
	pages = {845--911},
	booktitle = {Handbook of Automated Reasoning},
	publisher = {North-Holland},
	author = {Bundy, Alan},
	editor = {Robinson, Alan and Voronkov, Andrei},
	urldate = {2021-09-28},
	date = {2001-01-01},
	langid = {english},
	doi = {10.1016/B978-044450813-3/50015-1},
	file = {Volltext:C\:\\Users\\felix\\Zotero\\storage\\Z2QWVLB4\\Bundy - 2001 - Chapter 13 - The Automation of Proof by Mathematic.pdf:application/pdf},
}