Showing 1–17 of 17 results for author: Künnemann, R

Symbolic Parallel Composition for Multi-language Protocol Verification

Authors: Faezeh Nasrabadi, Robert Künnemann, Hamed Nemati

Abstract: The implementation of security protocols often combines different languages. This practice, however, poses a challenge to traditional verification techniques, which typically assume a single-language environment and, therefore, are insufficient to handle challenges presented by the interplay of different languages. To address this issue, we establish principles for combining multiple programming l… ▽ More The implementation of security protocols often combines different languages. This practice, however, poses a challenge to traditional verification techniques, which typically assume a single-language environment and, therefore, are insufficient to handle challenges presented by the interplay of different languages. To address this issue, we establish principles for combining multiple programming languages operating on different atomic types using a symbolic execution semantics. This facilitates the (parallel) composition of labeled transition systems, improving the analysis of complex systems by streamlining communication between diverse programming languages. By treating the Dolev-Yao (DY) model as a symbolic abstraction, our approach eliminates the need for translation between different base types, such as bitstrings and DY terms. Our technique provides a foundation for securing interactions in multi-language environments, enhancing program verification and system analysis in complex, interconnected systems. △ Less

Submitted 15 May, 2025; v1 submitted 9 April, 2025; originally announced April 2025.

Comments: Authors' version; to appear in the 38th IEEE Computer Security Foundations Symposium

Adaptive Exploit Generation against Security Devices and Security APIs

Authors: Robert Künnemann, Julian Biehl

Abstract: Proof-of-concept exploits help demonstrate software vulnerability beyond doubt and communicate attacks to non-experts. But exploits can be configuration-specific, for example when in Security APIs, where keys are set up specifically for the application and enterprise the API serves. In this work, we show how to automatically derive proof-of-concept exploits against Security APIs using formal metho… ▽ More Proof-of-concept exploits help demonstrate software vulnerability beyond doubt and communicate attacks to non-experts. But exploits can be configuration-specific, for example when in Security APIs, where keys are set up specifically for the application and enterprise the API serves. In this work, we show how to automatically derive proof-of-concept exploits against Security APIs using formal methods. We extend the popular protocol verifier ProVerif with a language-agnostic template mechanism. Employing program snippets attached to steps in the model, we can transform attack traces (which ProVerif typically finds automatically) into programs. Our method is general, flexible and convenient. We demonstrate its use for the W3C Web Cryptography API, for PKCS#11 and for the YubiHSM2, providing the first formal model of the latter. △ Less

Submitted 2 October, 2024; originally announced October 2024.

SpecMon: Modular Black-Box Runtime Monitoring of Security Protocols

Authors: Kevin Morio, Robert Künnemann

Abstract: There exists a verification gap between formal protocol specifications and their actual implementations, which this work aims to bridge via monitoring for compliance to the formal specification. We instrument the networking and cryptographic library the application uses to obtain a stream of events. This is possible even without source code access. We then use an efficient algorithm to match these… ▽ More There exists a verification gap between formal protocol specifications and their actual implementations, which this work aims to bridge via monitoring for compliance to the formal specification. We instrument the networking and cryptographic library the application uses to obtain a stream of events. This is possible even without source code access. We then use an efficient algorithm to match these observations to traces that are valid in the specification model. In contrast to prior work, our algorithm can handle non-determinism and thus, multiple sessions. It also achieves a low overhead, which we demonstrate on the WireGuard reference implementation and a case study from prior work. We find that the reference Tamarin model for WireGuard can be used with little change: We only need to specify wire formats and correct some small inaccuracies that we discovered while conducting the case study. We also provide a soundness result for our algorithm that ensures it accepts only event streams that are valid according to the specification model. △ Less

Submitted 4 September, 2024; originally announced September 2024.

Comments: 21 pages, Full version of the corresponding ACM CCS '24 paper

Computationally Bounded Robust Compilation and Universally Composable Security

Authors: Robert Künnemann, Marco Patrignani, Ethan Cecchetti

Abstract: Universal Composability (UC) is the gold standard for cryptographic security, but mechanizing proofs of UC is notoriously difficult. A recently-discovered connection between UC and Robust Compilation (RC)$\unicode{x2014}$a novel theory of secure compilation$\unicode{x2014}$provides a means to verify UC proofs using tools that mechanize equality results. Unfortunately, the existing methods apply on… ▽ More Universal Composability (UC) is the gold standard for cryptographic security, but mechanizing proofs of UC is notoriously difficult. A recently-discovered connection between UC and Robust Compilation (RC)$\unicode{x2014}$a novel theory of secure compilation$\unicode{x2014}$provides a means to verify UC proofs using tools that mechanize equality results. Unfortunately, the existing methods apply only to perfect UC security, and real-world protocols relying on cryptography are only computationally secure. This paper addresses this gap by lifting the connection between UC and RC to the computational setting, extending techniques from the RC setting to apply to computational UC security. Moreover, it further generalizes the UC$\unicode{x2013}$RC connection beyond computational security to arbitrary equalities, providing a framework to subsume the existing perfect case, and to instantiate future theories with more complex notions of security. This connection allows the use of tools for proofs of computational indistinguishability to properly mechanize proofs of computational UC security. We demonstrate this power by using CryptoVerif to mechanize a proof that parts of the Wireguard protocol are computationally UC secure. Finally, all proofs of the framework itself are verified in Isabelle/HOL. △ Less

Submitted 26 January, 2024; originally announced January 2024.

Journal ref: Proceedings of the 2024 IEEE Computer Security Foundations Symposium (CSF)

CryptoBap: A Binary Analysis Platform for Cryptographic Protocols

Authors: Faezeh Nasrabadi, Robert Künnemann, Hamed Nemati

Abstract: We introduce CryptoBap, a platform to verify weak secrecy and authentication for the (ARMv8 and RISC-V) machine code of cryptographic protocols. We achieve this by first transpiling the binary of protocols into an intermediate representation and then performing a crypto-aware symbolic execution to automatically extract a model of the protocol that represents all its execution paths. Our symbolic e… ▽ More We introduce CryptoBap, a platform to verify weak secrecy and authentication for the (ARMv8 and RISC-V) machine code of cryptographic protocols. We achieve this by first transpiling the binary of protocols into an intermediate representation and then performing a crypto-aware symbolic execution to automatically extract a model of the protocol that represents all its execution paths. Our symbolic execution resolves indirect jumps and supports bounded loops using the loop-summarization technique, which we fully automate. The extracted model is then translated into models amenable to automated verification via ProVerif and CryptoVerif using a third-party toolchain. We prove the soundness of the proposed approach and used CryptoBap to verify multiple case studies ranging from toy examples to real-world protocols, TinySSH, an implementation of SSH, and WireGuard, a modern VPN protocol. △ Less

Submitted 18 September, 2023; v1 submitted 28 August, 2023; originally announced August 2023.

Automated Security Analysis of Exposure Notification Systems

Authors: Kevin Morio, Ilkan Esiyok, Dennis Jackson, Robert Künnemann

Abstract: We present the first formal analysis and comparison of the security of the two most widely deployed exposure notification systems, ROBERT and the Google and Apple Exposure Notification (GAEN) framework. ROBERT is the most popular instalment of the centralised approach to exposure notification, in which the risk score is computed by a central server. GAEN, in contrast, follows the decentralised app… ▽ More We present the first formal analysis and comparison of the security of the two most widely deployed exposure notification systems, ROBERT and the Google and Apple Exposure Notification (GAEN) framework. ROBERT is the most popular instalment of the centralised approach to exposure notification, in which the risk score is computed by a central server. GAEN, in contrast, follows the decentralised approach, where the user's phone calculates the risk. The relative merits of centralised and decentralised systems have proven to be a controversial question. The majority of the previous analyses have focused on the privacy implications of these systems, ours is the first formal analysis to evaluate the security of the deployed systems -- the absence of false risk alerts. We model the French deployment of ROBERT and the most widely deployed GAEN variant, Germany's Corona-Warn-App. We isolate the precise conditions under which these systems prevent false alerts. We determine exactly how an adversary can subvert the system via network and Bluetooth sniffing, database leakage or the compromise of phones, back-end systems and health authorities. We also investigate the security of the original specification of the DP3T protocol, in order to identify gaps between the proposed scheme and its ultimate deployment. We find a total of 27 attack patterns, including many that distinguish the centralised from the decentralised approach, as well as attacks on the authorisation procedure that differentiate all three protocols. Our results suggest that ROBERT's centralised design is more vulnerable against both opportunistic and highly resourced attackers trying to perform mass-notification attacks. △ Less

Submitted 2 October, 2022; originally announced October 2022.

Comments: 23 pages, Full version of the corresponding USENIX Security '23 paper

Accountable Javascript Code Delivery

Authors: Ilkan Esiyok, Pascal Berrang, Katriel Cohn-Gordon, Robert Kuennemann

Abstract: The internet is a major distribution platform for web applications, but there are no effective transparency and audit mechanisms in place for the web. Due to the ephemeral nature of web applications, a client visiting a website has no guarantee that the code it receives today is the same as yesterday, or the same as other visitors receive. Despite advances in web security, it is thus challenging t… ▽ More The internet is a major distribution platform for web applications, but there are no effective transparency and audit mechanisms in place for the web. Due to the ephemeral nature of web applications, a client visiting a website has no guarantee that the code it receives today is the same as yesterday, or the same as other visitors receive. Despite advances in web security, it is thus challenging to audit web applications before they are rendered in the browser. We propose Accountable JS, a browser extension and opt in protocol for accountable delivery of active content on a web page. We prototype our protocol, formally model its security properties with the Tamarin Prover, and evaluate its compatibility and performance impact with case studies including WhatsApp Web, AdSense and Nimiq. Accountability is beginning to be deployed at scale, with Meta's recent announcement of Code Verify available to all 2 billion WhatsApp users, but there has been little formal analysis of such protocols. We formally model Code Verify using the Tamarin Prover and compare its properties to our Accountable JS protocol. We also compare Code Verify's and Accountable JS extension's performance impacts on WhatsApp Web. △ Less

Submitted 12 January, 2023; v1 submitted 20 February, 2022; originally announced February 2022.

On the Soundness of Infrastructure Adversaries

Authors: Alexander Dax, Robert Künnemann

Abstract: Companies and network operators perform risk assessment to inform policy-making, guide infrastructure investments or to comply with security standards such as ISO 27001. Due to the size and complexity of these networks, risk assessment techniques such as attack graphs or trees describe the attacker with a finite set of rules. This characterization of the attacker can easily miss attack vectors or… ▽ More Companies and network operators perform risk assessment to inform policy-making, guide infrastructure investments or to comply with security standards such as ISO 27001. Due to the size and complexity of these networks, risk assessment techniques such as attack graphs or trees describe the attacker with a finite set of rules. This characterization of the attacker can easily miss attack vectors or overstate them, potentially leading to incorrect risk estimation. In this work, we propose the first methodology to justify a rule-based attacker model. Conceptually, we add another layer of abstraction on top of the symbolic model of cryptography, which reasons about protocols and abstracts cryptographic primitives. This new layer reasons about Internet-scale networks and abstracts protocols. We show, in general, how the soundness and completeness of a rule-based model can be ensured by verifying trace properties, linking soundness to safety properties and completeness to liveness properties. We then demonstrate the approach for a recently proposed threat model that quantifies the confidentiality of email communication on the Internet, including DNS, DNSSEC, and SMTP. Using off-the-shelf protocol verification tools, we discover two flaws in their threat model. After fixing them, we show that it provides symbolic soundness. △ Less

Submitted 14 May, 2021; originally announced May 2021.

Comments: 32 pages, Full version, To be published at IEEE CSF'21

Verifying Accountability for Unbounded Sets of Participants

Authors: Kevin Morio, Robert Künnemann

Abstract: Little can be achieved in the design of security protocols without trusting at least some participants. This trust should be justified or, at the very least, subject to examination. One way to strengthen trustworthiness is to hold parties accountable for their actions, as this provides a strong incentive to refrain from malicious behavior. This has led to an increased interest in accountability in… ▽ More Little can be achieved in the design of security protocols without trusting at least some participants. This trust should be justified or, at the very least, subject to examination. One way to strengthen trustworthiness is to hold parties accountable for their actions, as this provides a strong incentive to refrain from malicious behavior. This has led to an increased interest in accountability in the design of security protocols. In this work, we combine the accountability definition of Künnemann, Esiyok, and Backes, with the notion of case tests to extend its applicability to protocols with unbounded sets of participants. We propose a general construction of verdict functions and a set of verification conditions that achieve soundness and completeness. Expressing the verification conditions in terms of trace properties allows us to extend Tamarin -- a protocol verification tool -- with the ability to analyze and verify accountability properties in a highly automated way. In contrast to prior work, our approach is significantly more flexible and applicable to a wider range of protocols. △ Less

Submitted 20 May, 2021; v1 submitted 22 June, 2020; originally announced June 2020.

Comments: 22 pages, Full version of the corresponding CSF 2021 paper

Journal ref: IEEE CSF 2021, Vol. 1, p. 327-342

Trollthrottle -- Raising the Cost of Astroturfing

Authors: Ilkan Esiyok, Lucjan Hanzlik, Robert Kuennemann, Lena Marie Budde, Michael Backes

Abstract: Astroturfing, i.e., the fabrication of public discourse by private or state-controlled sponsors via the creation of fake online accounts, has become incredibly widespread in recent years. It gives a disproportionally strong voice to wealthy and technology-savvy actors, permits targeted attacks on public forums and could in the long run harm the trust users have in the internet as a communication p… ▽ More Astroturfing, i.e., the fabrication of public discourse by private or state-controlled sponsors via the creation of fake online accounts, has become incredibly widespread in recent years. It gives a disproportionally strong voice to wealthy and technology-savvy actors, permits targeted attacks on public forums and could in the long run harm the trust users have in the internet as a communication platform. Countering these efforts without deanonymising the participants has not yet proven effective; however, we can raise the cost of astroturfing. Following the principle `one person, one voice', we introduce Trollthrottle, a protocol that limits the number of comments a single person can post on participating websites. Using direct anonymous attestation and a public ledger, the user is free to choose any nickname, but the number of comments is aggregated over all posts on all websites, no matter which nickname was used. We demonstrate the deployability of Trollthrottle by retrofitting it to the popular news aggregator website Reddit and by evaluating the cost of deployment for the scenario of a national newspaper (168k comments per day), an international newspaper (268k c/d) and Reddit itself (4.9M c/d). △ Less

Submitted 19 April, 2020; originally announced April 2020.

Causality & Control Flow

Authors: Robert Künnemann, Deepak Garg, Michael Backes

Abstract: Causality has been the issue of philosophic debate since Hippocrates. It is used in formal verification and testing, e.g., to explain counterexamples or construct fault trees. Recent work defines actual causation in terms of Pearl's causality framework, but most definitions brought forward so far struggle with examples where one event preempts another one. A key point to capturing such examples… ▽ More Causality has been the issue of philosophic debate since Hippocrates. It is used in formal verification and testing, e.g., to explain counterexamples or construct fault trees. Recent work defines actual causation in terms of Pearl's causality framework, but most definitions brought forward so far struggle with examples where one event preempts another one. A key point to capturing such examples in the context of programs or distributed systems is a sound treatment of control flow. We discuss how causal models should incorporate control flow and discover that much of what Pearl/Halpern's notion of contingencies tries to capture is captured better by an explicit modelling of the control flow in terms of structural equations and an arguably simpler definition. Inspired by causality notions in the security domain, we bring forward a definition of causality that takes these control-variables into account. This definition provides a clear picture of the interaction between control flow and causality and captures these notoriously difficult preemption examples without secondary concepts. We give convincing results on a benchmark of 34 examples from the literature. △ Less

Submitted 30 October, 2019; originally announced October 2019.

Comments: In Proceedings CREST 2019, arXiv:1910.13641

Journal ref: EPTCS 308, 2019, pp. 32-46

Universal Composability is Robust Compilation

Authors: Marco Patrignani, Robert Künnemann, Riad S. Wahby

Abstract: This paper discusses the relationship between two frameworks: universal composability (UC) and robust compilation (RC). In cryptography, UC is a framework for the specification and analysis of cryptographic protocols with a strong compositionality guarantee: UC protocols remain secure even when composed with other protocols. In programming language security, RC is a novel framework for determining… ▽ More This paper discusses the relationship between two frameworks: universal composability (UC) and robust compilation (RC). In cryptography, UC is a framework for the specification and analysis of cryptographic protocols with a strong compositionality guarantee: UC protocols remain secure even when composed with other protocols. In programming language security, RC is a novel framework for determining secure compilation by proving whether compiled programs are as secure as their source-level counterparts no matter what target-level code they interact with. Presently, these disciplines are studied in isolation, though we argue that there is a deep connection between them and exploring this connection will benefit both research fields. This paper formally proves the connection between UC and RC and then it explores the benefits of this connection. For this, this paper first identifies which conditions must programming languages fulfil in order to possibly attain UC-like composition. Then, it proves UC of both an existing and a new commitment protocol as a corollary of the related compilers attaining RC. Finally, it mechanises these proofs in Deepsec, obtaining symbolic guarantees that the protocol is indeed UC. Our connection lays the groundwork towards a better and deeper understanding of both UC and RC, and the benefits we showcase from this connection provide first evidence of scalable mechanised proofs for UC. △ Less

Submitted 15 December, 2022; v1 submitted 18 October, 2019; originally announced October 2019.

Automated Verification of Accountability in Security Protocols

Authors: Robert Künnemann, Ilkan Esiyok, Michael Backes

Abstract: Accountability is a recent paradigm in security protocol design which aims to eliminate traditional trust assumptions on parties and hold them accountable for their misbehavior. It is meant to establish trust in the first place and to recognize and react if this trust is violated. In this work, we discuss a protocol agnostic definition of accountability: a protocol provides accountability (w.r.t.… ▽ More Accountability is a recent paradigm in security protocol design which aims to eliminate traditional trust assumptions on parties and hold them accountable for their misbehavior. It is meant to establish trust in the first place and to recognize and react if this trust is violated. In this work, we discuss a protocol agnostic definition of accountability: a protocol provides accountability (w.r.t. some security property) if it can identify all misbehaving parties, where misbehavior is defined as a deviation from the protocol that causes a security violation. We provide a mechanized method for the verification of accountability and demonstrate its use for verification and attack finding on various examples from the accountability and causality literature, including Certificate Transparency and Kroll Accountable Algorithms protocol. We reach a high degree of automation by expressing accountability in terms of a set of trace properties and show their soundness and completeness. △ Less

Submitted 8 May, 2019; v1 submitted 28 May, 2018; originally announced May 2018.

Sufficient and necessary causation are dual

Authors: Robert Künnemann

Abstract: Causation has been the issue of philosophic debate since Hippocrates. Recent work defines actual causation in terms of Pearl/Halpern's causality framework, formalizing necessary causes (IJCAI'15). This has inspired causality notions in the security domain (CSF'15), which, perhaps surprisingly, formalize sufficient causes instead. We provide an explicit relation between necessary and sufficient cau… ▽ More Causation has been the issue of philosophic debate since Hippocrates. Recent work defines actual causation in terms of Pearl/Halpern's causality framework, formalizing necessary causes (IJCAI'15). This has inspired causality notions in the security domain (CSF'15), which, perhaps surprisingly, formalize sufficient causes instead. We provide an explicit relation between necessary and sufficient causes. △ Less

Submitted 25 October, 2017; originally announced October 2017.

Towards Automated Network Mitigation Analysis (extended)

Authors: Patrick Speicher, Marcel Steinmetz, Jörg Hoffmann, Michael Backes, Robert Künnemann

Abstract: Penetration testing is a well-established practical concept for the identification of potentially exploitable security weaknesses and an important component of a security audit. Providing a holistic security assessment for networks consisting of several hundreds hosts is hardly feasible though without some sort of mechanization. Mitigation, prioritizing counter-measures subject to a given budget,… ▽ More Penetration testing is a well-established practical concept for the identification of potentially exploitable security weaknesses and an important component of a security audit. Providing a holistic security assessment for networks consisting of several hundreds hosts is hardly feasible though without some sort of mechanization. Mitigation, prioritizing counter-measures subject to a given budget, currently lacks a solid theoretical understanding and is hence more art than science. In this work, we propose the first approach for conducting comprehensive what-if analyses in order to reason about mitigation in a conceptually well-founded manner. To evaluate and compare mitigation strategies, we use simulated penetration testing, i.e., automated attack-finding, based on a network model to which a subset of a given set of mitigation actions, e.g., changes to the network topology, system updates, configuration changes etc. is applied. Using Stackelberg planning, we determine optimal combinations that minimize the maximal attacker success (similar to a Stackelberg game), and thus provide a well-founded basis for a holistic mitigation strategy. We show that these Stackelberg planning models can largely be derived from network scan, public vulnerability databases and manual inspection with various degrees of automation and detail, and we simulate mitigation analysis on networks of different size and vulnerability. △ Less

Submitted 4 January, 2019; v1 submitted 15 May, 2017; originally announced May 2017.

Comments: Cleaned up presentation to focus on mitigation analysis in simulated pentesting. Stackelberg planning in a more general scope and the algorithm proposed in v1 are extended and discussed in more detail in Speicher et.al.: Stackelberg Planning: Towards Effective Leader-Follower State Space Search, AAAI'18

Computational Soundness for Dalvik Bytecode

Authors: Michael Backes, Robert Künnemann, Esfandiar Mohammadi

Abstract: Automatically analyzing information flow within Android applications that rely on cryptographic operations with their computational security guarantees imposes formidable challenges that existing approaches for understanding an app's behavior struggle to meet. These approaches do not distinguish cryptographic and non-cryptographic operations, and hence do not account for cryptographic protections:… ▽ More Automatically analyzing information flow within Android applications that rely on cryptographic operations with their computational security guarantees imposes formidable challenges that existing approaches for understanding an app's behavior struggle to meet. These approaches do not distinguish cryptographic and non-cryptographic operations, and hence do not account for cryptographic protections: f(m) is considered sensitive for a sensitive message m irrespective of potential secrecy properties offered by a cryptographic operation f. These approaches consequently provide a safe approximation of the app's behavior, but they mistakenly classify a large fraction of apps as potentially insecure and consequently yield overly pessimistic results. In this paper, we show how cryptographic operations can be faithfully included into existing approaches for automated app analysis. To this end, we first show how cryptographic operations can be expressed as symbolic abstractions within the comprehensive Dalvik bytecode language. These abstractions are accessible to automated analysis, and they can be conveniently added to existing app analysis tools using minor changes in their semantics. Second, we show that our abstractions are faithful by providing the first computational soundness result for Dalvik bytecode, i.e., the absence of attacks against our symbolically abstracted program entails the absence of any attacks against a suitable cryptographic program realization. We cast our computational soundness result in the CoSP framework, which makes the result modular and composable. △ Less

Submitted 25 October, 2016; v1 submitted 15 August, 2016; originally announced August 2016.

Comments: Technical report for the ACM CCS 2016 conference paper

Automated analysis of security protocols with global state

Authors: Steve Kremer, Robert Künnemann

Abstract: Security APIs, key servers and protocols that need to keep the status of transactions, require to maintain a global, non-monotonic state, e.g., in the form of a database or register. However, most existing automated verification tools do not support the analysis of such stateful security protocols - sometimes because of fundamental reasons, such as the encoding of the protocol as Horn clauses, whi… ▽ More Security APIs, key servers and protocols that need to keep the status of transactions, require to maintain a global, non-monotonic state, e.g., in the form of a database or register. However, most existing automated verification tools do not support the analysis of such stateful security protocols - sometimes because of fundamental reasons, such as the encoding of the protocol as Horn clauses, which are inherently monotonic. A notable exception is the recent tamarin prover which allows specifying protocols as multiset rewrite (msr) rules, a formalism expressive enough to encode state. As multiset rewriting is a "low-level" specification language with no direct support for concurrent message passing, encoding protocols correctly is a difficult and error-prone process. We propose a process calculus which is a variant of the applied pi calculus with constructs for manipulation of a global state by processes running in parallel. We show that this language can be translated to msr rules whilst preserving all security properties expressible in a dedicated first-order logic for security properties. The translation has been implemented in a prototype tool which uses the tamarin prover as a backend. We apply the tool to several case studies among which a simplified fragment of PKCS\#11, the Yubikey security token, and an optimistic contract signing protocol. △ Less

Submitted 12 May, 2014; v1 submitted 5 March, 2014; originally announced March 2014.