{'fraction_non_alphanumeric': 0.03683557192072193, 'fraction_numerical': 0.006429836673779935, 'mean_word_length': 4.255295756065381, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 29, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
On the Soundness of Infrastructure Adversaries

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.


I. INTRODUCTION
The Internet is the primary medium for distributing entertainment, news and knowledge and an important pillar to industrial commerce. It is constructed from service providers interoperating according to several protocols. Many of them were conceived before the Internet was even considered a Mass Medium [43]; they were hence designed to be fast and serviceoriented, whereas security was a second thought. Trust between service providers at different protocol layers is thus an implicit assumption, making it difficult to estimate potential attacks' impact.
High-profile attacks, e.g. on routing [39] or name resolution [44] are a painful reminder of these trust assumptions. They also highlight the slow adoption of security protocols, which were developed only post-hoc, to mitigate some of these issues. Even for TLS [48], which enjoys high popularity, adoption was and remains slow. According to Qualys Labs [35], 6% of all websites still support SSL 3.0, which is exploitable in various manners and was deprecated in 2015. Moreover, security protocols rely on trust assumptions and a complicated interplay between routing, name resolution, and the application layer. An example is RFC 7817 [42], which defines certificate validation for email transport. It mandates that the certificate contains the email domain (the part after the '@') and not just the target server's domain name, as a name resolution attacker can easily manipulate the latter. Large-scale attacks thus rarely exploit previously unknown flaws in a single protocol, but instead target their deployment in the wild.
Despite the effort put into securing individual protocols and cryptographic primitives in the past decades, worldwide attacks like the Great Cannon [40] or spying systems like PRISM [25] exploit weak components and (the absence of) trust anchors in the infrastructure. To analyze an infrastructure like the Internet, with broken legacy protocols, unstable trust assumptions, and varying degrees of centralization on different layers, a high-level approach is necessary.
Risk assessment originates in the formal assessment of potential failures in large infrastructures like power plants. Techniques like fault trees provide a systematic method for identifying and minimizing potential risks. They were soon adopted for IT infrastructure. These techniques usually consider the severity of known vulnerabilities and some valuation of critical assets. The problem size grows with the size of the network. Therefore, most of these techniques formalize the threat model as a set of rules. Those techniques include planning, attack graphs (which were derived from fault graphs), and game-based models. 1 While these analyses are formal and well justified, the rules themselves are not formally justified. It is not safe to assume that the set of rules is comprehensive. Thus the analysis may miss potential attack vectors. There is a surprising similarity to the soundness of the Dolev-Yao model. Abadi and Rogaway's seminal paper on computational soundness [2] considered the soundness of a such a rule-based symbolic attacker on protocols in the computational model. Likewise, our focus is on the soundness of a rule-based attacker, the infrastructure attacker (IA), but in the symbolic model instead of the computational model. In both cases, the need for further abstraction is driven by the complexity of the problem (infrastructure analysis/protocol analysis) but requires justification.
Contributions 1) We define proof obligations for the correctness of an infrastructure attacker in the STRIPS framework for planning as a set of trace properties. We show that soundness can be proven by verifying safety properties, and correctness by verifying liveness properties. 2) We apply this definition to an IA model for email communication [52] and establish its soundness (barring some minor flaws).
3) We show how to automate the proof of this trace properties by over-approximating all possible instantiations of the IA model with a single process. The protocol transformations we introduce to this end are of independent interest, as they can help to reduce drastically the size of processes that model an adversary with limited access to network traffic. 4) We show various authentication properties of SMTP in conjunction with DNS, DNSSEC, and a simple resolver model in ProVerif. As a by-product, this model provides the first automated verification result for authentication in DNSSEC.
II. RELATED WORK 1) Risk assessment techniques: The most popular techniques for the analysis of IT infrastructure are attack graphs [56] and trees [49], see [38] for a recent survey. They originate in risk assessment and reliability analysis for critical infrastructures. Fault tree analysis [16] was used, e.g. for analyzing nuclear power plants or military missile control systems. Attack graphs and trees have been used to assess risks in forensic examination [37], network security [34,47] or cloud infrastructures [3]. Used naïvely, both techniques suffer from the state explosion property. Luckily, a large body of work is devoted to improving performance, e.g. generating of minimal attack graphs [24], distributing attack graph generation [32] or the efficient representation of network defenses [30].
More recently, planning was considered as an alternative technique with great benefits in terms of performance [23]. Planning is one of the oldest sub-areas of AI and benefits from being a well-studied research field with a large community and a focus on optimizing performance. Compared to various semantics for attack graphs, there is a fairly wide agreement on the STRIPS framework [21]. Planning was used for attack graph generation [26], network analysis [12], penetration testing [45], and internet infrastructure analysis [53]. Additionally, the popular attack graph formalism can be translated into a planning problem [29].
2) Infrastructure analysis: Until recently, these approaches were used to analyze local networks or the public infrastructure unrelated to information security. Presumably, this was due to the problem size associated with large-scale infrastructures like the Internet. Frey et al. [22] conducted one of the first Internet-scale infrastructure assessments in terms of security evaluation. They investigated the Border Gateway Protocol deployment looking into potential threats and vulnerabilities. Simeonovski et al. [51] present a technique that models services, providers, and dependencies on the Internet as a property graph, establishing a high-level IA model. This model is used to reason about dependencies between services and infrastructure providers and how these dependencies can be exploited to impact a large amount of end users. They conduct a largescale case study by using a simple tainting-style propagation technique in a graph database highly optimized for reachability queries. They studied several attack scenarios like emailsniffing and DDOS caused by the distribution of malicious JavaScript. More recently, Speicher et al. [52] introduced the first deployment analysis on a global level, evaluating various measures to secure the email infrastructure against large-scale attacks. They employ Stackelberg planning [53], which is a twostage planning technique that computes all defender plans that are Pareto-optimal with respect to their cost and the worst-case impact of an attacker.
To our knowledge, all these assessment approaches have only informally justified their threat models. Given the high abstraction level of their reasoning, validation using formal analysis techniques is necessary. Sheyner et al. [50] propose the use of symbolic model checking to generate attack graphs from a finite state machine that represents the network. Here, state transitions correspond to atomic attacker steps which themselves require justification. This approach is neither applicable to larger networks (because of the aforementioned state-explosion property) nor does it provide the desired level of justification (as network attackers are too complex for finite state machines).
3) The analogy to computational soundness: In contrast to cryptographic primitives like encryption or signatures, larger cryptographic protocols are typically analyzed in the Dolev-Yao model [19], where cryptographic primitives (short: crypto primitives) are abstracted with a term algebra. Proofs in the computational model are possible, but become prohibitively complex due to the need to reason about probabilistic behavior and runtime. Mechanization becomes incredible difficult [8] and manual proofs can easily miss details. By contrast, the abstraction of cryptography by a term algebra has enabled the development of fully automatic and semi-automatic protocol verifiers [10,41] that can handle highly complex protocols, e.g. TLS 1.3 [9,18].
To bridge both worlds, Abadi and Rogaway [2] introduced computational soundness, justifying the use of the symbolic model for protocol analysis. Gaining the advantages of automation in the symbolic model, and the stronger guarantees of the computational model, the notion of computational soundness is seen as a massive milestone in protocol verification. With this work, we want to extend on this stack in an analogous fashion,  and introduce the notion of symbolic soundness relating the infrastructure adversary to the symbolic model in a similar fashion. This is depicted in Fig. 1.
To attain this goal, we lift this approach from the protocol level to the infrastructure level. To readers familiar with computational soundness, Tab. I can help to support this analogy.
We formalize the IA model as a planning problem in the STRIPS formalism [21]. The rules represent an infrastructure attacker that can selectively corrupt parts of the infrastructure, but assumes that protocols themselves are secure. Dolev-Yao models, by contrast, represent a network attacker, but assume the crypto primitives to be perfect. To reason about the validity of the model w.r.t. those assumptions, they need to be formalized. As they are implicit in the respective semantics (STRIPS / process calculus with term algebra), a low-level semantics is necessary to state these assumptions. Assumptions about protocols are stated in the Dolev-Yao model, usually within a process calculus with a term algebra. Assumptions about cryptographic primitives are stated as asymptotic probability bounds on the probability of a runtimebounded Turing machines winning some game.
Symbolic soundness asserts that, when compiling a given infrastructure model into a process, all symbolic traces that this process allows can be mapped to attacker plans in the planning model. This is structurally similar to computational soundness, which ensures that no computational attacks are missed by mapping all computational executions to symbolic traces (with a negligible failure probability). We can thus show that no symbolic attack is missed by the IA model, provided the protocols are working as intended. To be clear: symbolic soundness does not imply computational soundness, but both combine. If a symbolic soundness result asserts the absence of attacks w.r.t. to some symbolic model, then a computational soundness can extend this result to the computational model of cryptography. This requires that the computational soundness result supports the cryptographic primitives and process calculus used by the symbolic soundness result.
Much like results in computational soundness, symbolic soundness results apply to a fixed set of primitives, in their case: protocols. We model an infrastructure consisting of DNS, DNSSEC and SMTP, using a dialect of the appliedπ calculus [1]. 4) Symbolic completeness and liveness properties: In contrast to computational soundness, the completeness of an IA model is equally important to the analysis. A quantitative analysis, e.g. counting the number of affected hosts, is incorrect if the IA model overestimates the protocol attacker's capabilities. In the case of Stackelberg planning, this might lead to the proposition of suboptimal countermeasures and, if the defender budget is fixed, to an allocation that is not optimal for security. We therefore define symbolic completeness and show a set of conditions that implies the completeness of this model. Unfortunately, one of these is a liveness property, i.e., a property of the form: 'the [protocol] eventually enters a desirable state' [36]. Practically all protocol verification tools [10,41,17] in the unbounded model cover only safety properties, i.e., properties of the form 'the protocol never enters a bad state'. Hence, there is currently no support for the verification of liveness properties such as ours. We further elaborate on this topic in section IV-C. 5) Analysis of DNSSEC: To our knowledge, our case study provides not only the first automated result w.r.t. an infrastructure attacker, but also the first automated verification result for DNSSEC. Chetioui et al. [14] investigate (weak) secrecy in E-DNSSEC, a variant of DNSSEC that adds encryption, in ProVerif. Kammuller [31] also cover authentication in a handwritten, but automatically verified proof in Isabelle/HOL.

III. BACKGROUND: AUTOMATED PLANNING
A planning task is usually described in the STRIPS framework [21]. Here, Π " pP, I, A, Gq is defined over a high-level representation of the world in which each state σ is built over a set of state propositions P. I Ď P is the initial state and the task is to reach a goal states in G Ď 2 P . A set of actions A over P defines transitions between states. Actions are described as a triple (pre, del, add) where pre Ď P is the set of preconditions needed in the current state to make the action applicable, del Ď P tells which proposition will be deleted in the transition to the next state whereas add Ď P tells which propositions are added. In classical planning, we assume that all actions have a deterministic effect and that the initial state of the world is known from beginning. A state σ is reachable from I, if there is a sequence of actions a 0¨¨¨ak , which can be applied to I one after another resulting in σ. We call this sequence of actions a plan π to reach σ. The basic idea behind planning is to find a sequence of actions, s.t. their application starting from the initial state I leads to one of the goal states in G. Speicher et al., e.g., consider the initial state as the nodes that an attacker controls from the start, e.g., different nation-state adversaries or companies abusing power.
Goal states are valuable assets that need to be protected, e.g., the largest mail providers within some country. Over the years, several variations of automated planning have been developed, with different modeling assumption and resulting complexity classes for plan existence, worst-case runtime, etc.
We focus on classical planning for the ease of presentation. Our approach easily transfers to probabilistic planning when considering uncertainty about the initial set-up or effect probabilities as model parameters. We cannot justify these parameters via protocol verification (which is typically possibilistic) or cryptographic reasoning in general. These parameters model uncertainty about the attacker's capabilities and intentions. They are thus outside the current scope of formal analysis in security. Our infrastructure attacker is described by actions that have only positive preconditions and postconditions, i.e., they are described as pairs ppre, postq P P 2 instead of tuples ppre, del , add q. Such planning tasks are called delete-relaxed or monotonous and are easier to solve. Delete-relaxed planning aligns with the implicit assumption that attackers only gain assets in attack graph analysis [5].
Stackelberg planning [53] elevates this form of analysis to a two-player planning task in an attacker/defender scenario. In this scenario, the defender tries to implement mitigation strategies to limit the impact of the worst-case attacker strategy. A Stackelberg planning task differs from a classical task by dividing the set of actions into leader (or attacker) actions A L and into follower (or defender) actions A F . Further, the goal states are now defined for the defender, namely defender/follower goals G F . In this setting, an attack is composed of attacker actions, but applies to a world state where the defender has applied a plan composed of defender actions to the initial state. Every attack is annotated with some attacker reward, which depends on the severity of the attack (e.g. number of corrupted connections due to the attack). Defender actions come with a cost. The Stackelberg planning algorithm computes the set of Pareto-optimal pairs of attacker and defender plans. For the soundness of the attacker model, it is enough to consider the classical planning task where the follower actions are removed and only the attacker goal is considered, but the initial state can be any state reachable via defender actions. In our analysis, the initial state is, in fact, arbitrary.

IV. SYMBOLIC SOUNDNESS AND COMPLETENESS
We introduce the concepts of symbolic soundness and symbolic completeness, which relate the infrastructure adversary model (formalized as a planning problem) to the Dolev-Yao model [19]. Our approach applies to security properties that can be expressed as trace properties. We start by introducing the necessary notation and concepts. Then we introduce the conditions under which symbolic soundness and symbolic completeness hold. Finally, we prove these statements.

A. Notation
For a sequence s P Σ˚, let setpsq be the set of elements in s. For e P Σ, s˝e denotes the concatenation with e. For S Ď Σ, s| S is s with every element outside S removed.
The IA model is formalized in terms of a finite set of planning actions. We define postseqpπq " post 0 , post 1 , . . . , post n to be the sequence of postconditions of some plan π " ppre 0 , post 0 q, . . . , ppre n , post n q. We define a planning trace of some plan π as a sequence pt " s 1 , s 2 , . . . , s n , where for all i P t1, . . . , nu, s i P permppost i q is some permutation of post i . If all postconditions in π are singleton sets, it has only one pt. Let T Π pσq be the union of all planning traces reaching σ, and (with slight abuse of notation) T Π Ď P˚denote the union of planning traces over all states.
For generality, symbolic soundness and completeness are formulated independent of the process calculus. We assume a set of traces of form traces " Events˚that represents the possible behavior of a protocol and is usually specified by encoding it into a process. To simplify the presentation and avoid introducing a mapping function, we assume a nonempty intersection between predicates P and events Events. Our aim is to match planning traces and protocol traces on this intersection, which we denote by Σ X . Typically, the predicates/events in this set signify the corruption of some party or the partial compromise of certain infrastructure services (cf. Table III for examples). We hence call them corruption predicates.
When all predicates P are contained in Σ X , our approach can be seen as a refinement, where planning traces provide an abstract view on protocol traces.

B. Symbolic Soundness
We define the symbolic soundness of a planning task w.r.t. a set of traces. We will then provide sufficient conditions for this property. Two of them can be checked statically on the planning problem; the third holds for most process calculi. The fourth induces a set of trace properties that can be discharged to protocol verifiers. We say that a planning task is sound if any behavior of the protocol, e.g. an attack, is represented in the planning task.
Symbolic soundness provides guarantees with respect to the Dolev-Yao model. In case the Dolev-Yao model (represented by T ) is covered by a computational soundness result, these guarantees may translate to the computational model, but a priori, these are guarantees in a symbolic model of cryptography. We now state and discuss sufficient conditions for soundness for an arbitrary but fixed planning problem Π " pP, I, A, Gq and a set of traces T . Discussion. This condition is true w.l.o.g. for all monotonic planning tasks [13] whose postconditions are positive. Any action with n ą 1 postconditions a " ppre, tc 1 , ..., c n uq can be split into n actions a i " ppre, tc i uq without losing completeness or soundness. Since we never delete any information from the state, each plan where a occurs can be recovered by substituting a with the sequence a 1 , . . . , a n . Conversely, we can apply a whenever any plan contains some a i . CS 2. All corruption predicates are reproducible in the planning model.
Discussion. This condition is largely technical. Note first that post is singleton by CS 1. The set of corruption predicates Σ X should be chosen to represent all events where planning traces and protocol traces ought to match. Hence the planning model must be able to produce them. Furthermore, any planning task can be transformed so that all predicates in P appear in some action's postcondition: we let I " H and add an action that reaches the initial state. Now all actions with preconditions that do not appear in any postcondition can be removed and P be set to the union of postconditions. As Σ X Ď P, this implies CS 2.
CS 3. The set of traces is prefix-closed. For any k ą 0 @e 1 , . . . , e k .pe 1 , . . . , e k q P T ùñ pe 1 , . . . , e k´1 q P T Discussion. This condition concerns the semantics of the process calculus. It holds for ProVerif [10], Tamarin [41] and Scyther [17]. CS 4. The production of predicates in Σ X is not dependent on predicates outside of this set. @post P Σ X .@ppre, tpostuq P A.@f P pre : f P Σ X Discussion. The corruption predicates Σ X are used to describe the security model in both languages. With this condition we restrict the model to independent of predicates outside of Σ X . We refrain from forbidding predicates outside of Σ X in the planning model as they appear to be useful in quantitative tasks. For instance, counting occurrences of specific corruption predicates can be essential in a quantitative analysis. Such a model would be depended on predicates in Σ X but not vice versa.
where there is exactly one set per postcondition tc i u. (By CS 1, all postconditions are singleton.) We assume that, whenever a postcondition c i appears in a trace, then a matching precondition appears, too, namely the precondition of some action in A ci . @i P t1..nu, t P T : c i P t^c i P Σ X ùñ Da " ppre i , tc i uq P A ci : @g P pre i : g P t.
Discussion. This property is a safety property and can be shown using any protocol verifier that handles correspondence properties, e.g. Tamarin [41] or Scyther [17]. In Section VIII, we use ProVerif [10] to this end.
The following theorem establishes the soundness of this approach: Theorem 1. If CS 1, CS 2, CS 3, CS 4 and CS 5 hold, then Π is symbolically sound.
Proof. Proof by induction over the length of t| ΣX . Base case |t| ΣX | " 0: Let σ = I. Then T Π pσq = setppqq. For the empty trace t, it holds that t| ΣX = pq P T Π pσq. Inductive step: Let |t| ΣX | " k`1.Let t| ΣX " pe 1 e 2 ..e k`1 q. By CS 3 and the inductive hypothesis, there is a t k | ΣX " pe 1 e 2 ..e k q and a planning trace pt k , with pt k « t k . From pt k we can infer that there exists a reachable state (of Π) σ k with σ k | ΣX " te 1 , e 2 , ..e k u.
By CS 1, we get that all postconditions of any action in A are singleton sets. By CS 2, there exists an action a P A with a " ppre a , post a q and post a " e k`1 . Let A e k`1 be the partition of all of A containing all actions with postcondition e k`1 . As e k`1 P Σ X , by CS 4 all preconditions are in Σ X , too. By CS 5, there exists an action a˚" ppre, te k`1 uq s.t. for all g P pre : g P t k . As pre Ď Σ X , all g P pre are in setpt k | ΣX q " setppt k | ΣX q and thus in σ k . Applying a˚to the state, we get σ k`1 with σ k`1 | ΣX " te 1 , e 2 , ..e k , e k`1 u.
Finally, we can conclude that there exists a planning trace

C. Symbolic Completeness
The complementing property to symbolic soundness is symbolic completeness. It ensures that the planning model does not introduce spurious attacks that cannot occur in the protocol model. Planning problems are frequently used to perform a quantitative assessment of, e.g. the number of reachable goal states or the probability of reaching certain assets. The correctness of such an assessment relies on symbolic soundness and symbolic completeness. This is in contrast to computational completeness, which is of little interest as long as the symbolic model is good enough to provide verification results.
We provide an additional assumption that ensures symbolic completeness. Unfortunately, it is a liveness property, i.e., a property of the form: 'the [protocol] eventually enters a desirable state' [36] and cannot be verified by the current generation of protocol verifiers.

CC 1.
If an action is available and the trace contains the necessary preconditions, then the trace can be extended so it contains this action's postcondition. @t P T ,a " ptp 1 , ..., p n u, cq P A : c P Σ X^p tp 1 , ..., p n uq Ă setptq ùñ Dt 1 P T : t 1 " t˝t r^p setpt r q X Σ X q " tcu.
Discussion. Lamport [36] informally describes such properties as liveness properties. Note that here, the 'desirable state' is an additional attack step. As we only consider finite traces, Alpern and Schneider's definition of liveness [4], -which is well known because it decomposes trace properties into safety and liveness properties -does not classify CC 1 as a liveness property. 2 Other characterisations do, see Kindler [33] for a survey.
Nevertheless, state-of-the-art protocol verifiers in the unbounded setting [10,41,17] only support the specification of properties of the form @t P T .ϕptq where ϕ is a property that is protocol-agnostic, i.e. invariant w.r.t. T . This prohibits a direct encoding of CC 1.
Backes, Dreier, Kremer, and Künnemann propose an encoding of liveness properties for Tamarin that allows transforming liveness properties into this fragment of safety properties [7]. Their methodology is based on the idea that the protocol specifies a way to reach the 'desirable state,' e.g. by defining a recovery protocol. Hence any trace either already reached a desirable state or it has not exhausted all specified recovery steps -which is a safety property. Unfortunately, this approach does not apply here, as, in our case, the protocol model is not meant to specify how an attack is mounted.
An alternative approach to a direct encoding is to show that any trace t can be combined with any trace t 1 that contains p 1 , . . . , p n , c, and nothing else. This may hold for processes of a certain form. With such a result, protocol verifiers could again be used to show the existence of t 1 . For the present paper, we leave the verification of CC 1 as an open question.
Under this condition, and if we assume the set of traces to be prefix-closed, we obtain symbolic completeness. Theorem 2. If CS 1, CS 3, CS 4 and CC 1 hold, then Π is symbolically complete.
Proof. Induction over the length of pt | ΣX . Base case: |pt| ΣX | = 0: Holds trivially for σ " I. Inductive step: Let pt | ΣX = e 1 ...e k e k`1 . From the IH and CS 3, we know that there exists a trace t k « e 1 , . . . , e k « pt k . By definition of «, we know that e k`1 P Events and from pt P T Π , we conclude that there is a e k`1 P A with e k`1 as a postcondition which was used to construct pt. By CS 1, a e k`1 = (pre, te k`1 u). By CS 4 we know that pre Ď Σ X . The preconditions are met: pre Ă setpt k | ΣX q because pre Ă setppt k | ΣX q. Thus, we can apply CC 1 for a " a e k`1 and t " t k to obtain a trace t 1 « t k˝tr with t r | ΣX " e k`1 . Hence t 1 « t k˝ek`1 « e 1 ...e k e k`1 « pt.
To summarize: in conjunction, Theorem 1 and Theorem 2 ensure that the set of planning traces induced by Π and the set of protocol traces T are equal modulo Σ X if conditions CS 1 -CS 5 and CC 1 are met. This is necessary for risk estimation techniques that compute the expected loss of value or the probability of a breach. CS 1 to CS 2 are satisfied w.l.o.g. for monotonic planning tasks and CS 3 is a standard assumption in protocol verification. CS 4 is a restriction we place on the composition of the security model and auxiliary models for the planning task. The remaining assumptions CS 5 and CC 1 are both trace properties, the former a safety property, the latter a liveness property. Given the lack of tool support, we will now focus on symbolic soundness, which ensures that that the planning model considers all possible attacks. If symbolic soundness holds, any quantitative result that is monotonic in A -e.g. the expected damage or the probability of reaching a critical asset -can be considered an upper bound, provided, of course, that model parameters such as the value of assets and probabilities of actions are correct.

V. APPLICATIONS
The previous section results lay the foundation for using highly optimized planners for the analysis of large networks. We envision the following applications.
a) Protocol analysis for limited network attackers: Today's protocol verification focuses on protocols in isolation and against an attacker who can eavesdrop and modify all messages on the network. In terms of communication, this is the worst-case assumption for distributed services on the Internet. On the other hand, underlying services like the PKI or name resolution are almost always trusted and, more often than not, vastly simplified to the point of complete abstraction. For perspective, the Dolev-Yao model, which formalized these assumptions, is older than the first implementation of name resolution.
Planning models scale much better to large problem sizes (in terms of actions) than protocol verifiers, and are thus able to analyze the security of protocols in threat scenarios that are more complicated to describe. Incorporating more precise assumptions about the attacker could lead to more nuanced results, e.g. about protocol security in various topologies.
b) Cost-benefit guided protocol deployment in the Internet: Deployment assessment techniques are based on an infrastructure threat model and consider the deployment of a protocol as a 'countermeasure.' Using the recently proposed 'Stackelberg planning algorithm,' it is possible to obtain the set of all Pareto-optimal protocol deployments per node. This allows for an evaluation of the actual benefit of new proposals vis-à-vis the current infrastructure of the Internet. It makes it possible to compare proposals against each other that are incomparable on paper, e.g. is DNSSEC a better solution against JavaScript injection attacks than application-specific techniques like subresource integrity on the HTML level.
This technique has been applied to email [52] and the web [54], comparing solutions at the routing layer, resolution layer and application layer. A weak point of this methodology was the lack of justification for their attacker model. Symbolic soundness and completeness can bridge this gap, as we will demonstrate for a subset of the email model [52]. As we argued in Section III, to justify the correctness of the Stackelberg planning problem, it is sufficient to show the symbolic soundness/correctness for the attacker planning problem, but for arbitrary initial states.
c) Corporate network analysis: Risk assessment techniques for local networks (e.g. mulVal [46]) focus on implementation-level flaws, e.g. buffer overruns, but often ignore the protocol level implications. An attacker that captures the company's certificate authority or authentication server can usually exploit this infrastructure's trust to obtain critical assets. Moreover, modern cloud-based services introduce new dependencies on external infrastructure. These aspects are rarely considered and could be improved by a rule-based representation of the involved protocol's flaws.

VI. BACKGROUND: EMAIL CASE STUDY
We recall the email infrastructure attacker model by Speicher et al. [52] to justify its soundness in the next chapter. Using Stackelberg planning, they investigated how existing protocols can be used to secure users against large-scale eavesdropping by countries. While the impact of many techniques is different depending on the attacker and defender country (e.g. Russia and China are much more self-reliant than, e.g. Brazil), the enforcement of TLS and improved certificate validation have a significant impact throughout. In the following, we will focus on their threat model and infrastructure representation.
The email infrastructure is modeled as a labeled property graph [51], which is simply a graph with edge and node labels that describe service providers and their interdependencies. Definition 4. A labeled property graph is a directed multigraph and described as a quadruple G = (V ,E,λ,µ) over an alphabet Σ. V is the set of nodes. E Ă pVˆV q is a set of edges between nodes. The function λ : V Y E Ñ Σ maps a label from the alphabet Σ to nodes and edges. µ : pV Y EqˆK Ñ S maps a string value s P S to a node/edge and a key k P K.   Table II shows the node labels and edge labels used by Simeonovski et al. [51]. Figure 2 provides an example for the interaction between two mail providers. The green nodes represent IPv4 addresses and are labeled IP. They are associated to autonomous systems (orange, labeled AS) via the relation ORIG.
The blue nodes represent domain names and are labeled Dom. They are associated to IPs or other domains via the relations A, MX and NS which encode the resources records that were obtained by scanning. They designate the domain's IP address (A), its responsible mail server (MX) and its authoritative name server (NS), respectively.
The label DNS records the relationship between authoritative name servers and RES between mail servers and their resolvers. RTEpAS b q is used to record routing dependencies. If AS a is connected to AS c and, somewhere along the way, a package might traverse AS b , an attacker at AS b could eavesdrop that communication. Domains, IPs and ASes are associated to countries via LOC edges.

A. Infrastructure attacker model
An attacker in this model can be a country or a group of countries that can corrupt all servers in their jurisdiction, as well as to observe, intercept and alter all messages routed through their jurisdiction. 3 The IA model tracks infrastructure compromise at different levels with corresponding predicates. For example, if the attacker has compromised the resolver of some domain, we would consider the integrity of all domain name resolutions of this domain compromised. However, the resolved domains themselves are not be compromised and may be safe to use for clients that use a different resolver. These predicates will be part of Σ X and thus have to coincide with corresponding events in the protocol model.
There are 16 rules (also called action schemas) that define how these predicates can be derived. They are parametric in the graph: for a given graph, they are compiled into a finite set of attacker actions A and predicates P. Our focus is on the methodology; hence we will refer to Appendix A for the full set of attacker rules and only give a flavor of these rules with the following simple example.  The intuition is as follows. If the attacker controls the route from a domain to the resolver that this domain uses, then we consider the integrity of any name resolution this domain attempts compromised. If the domain that is resolved uses DNSSEC, however, then the resolver can verify the integrity of this signature and this attack vector is not available. (A different rule deals with the case where the resolver itself is compromised.) The predicate nDNSSEC cannot be produced by the attacker, as it is a defender predicate.
In Speicher et al.'s model, all attacker rules that produce the predicate unconf are associated with a reward in terms of the number of users affected. The Stackelberg planning algorithm maximizes the sum of rewards. As unconf P Σ X , the symbolic soundness result ensures that this is an upper bound.

B. Limitations
To simplify presentation, we concentrate on the core model, consisting of resolvers, DNS, DNSSEC and SMTP. We left out SMTP over TLS, DANE and IPsec for secure inter-AS communication. The protocol transformations we present in the next section would apply to the full model, as these protocols could be added without changing the structure of the processes. Thus the methodology would be the same, but the ProVerif processes would need to be extended.
The attacker model is not probabilistic, but relies on correct attacker rewards, which Speicher et al. [52] estimated from public sources. These are model parameters and need to be estimated.

VII. BACKGROUND: PROVERIF
In the following, we introduce ProVerif's dialect of the applied´π calculus [10,11]. Readers familiar with it can safely skip to the next section.

A. Syntax
We present the syntax of the calculus in Figure 3. Terms represent messages and data. Processes represent entities/programs. We use x, y, z to represent variables, a, b, c, n, k, s for free names and p, q for public names. We use FN and PN to refer to the set of free names and public names, respectively. Both are arbitrary, but infinite. The function symbol f represents a M, N ::" terms v, x, y, z variable a, b, c, n, k, s free name p, q public name f pM 1 , ..., M n q constructor application P, Q ::" constructor whereas we use g to represent destructors. Both are abstract function symbols with some fixed arity.
Terms are defined over names, variables, and the applications of constructors. Destructors are used to manipulate terms in processes: let x " gpM 1 , ..., M n q in P else Q binds x to the result of the destructor application of g on M 1 ...M n and continues with process P . If the application fails, however, we continue with process Q. A destructor g is defined by a finite set of reductions def pgq :" gpN 1 , ..., N n q Ñ N where the terms N, N 1 , ..., N n are build without free names and varpN q Ă varpN 1 Y ... Y N N q. A destructor fails, if no reduction applies.
Example 2. Symmetric encryption is described by a 2-ary constructor senc and a 2-ary destructor with the following reduction: sdecpsencpx, yq, yq Ñ x We write f npP q (and f vpP q) for the sets of names (variables) that are free in P . A substitution δ = tt t1 { x1 u , ..., t tn { xn uu is a partial function, mapping variables to terms. The domain of δ is Dpδq = tx 1 , ..., x n u and δ maps x i to t i . The application of g on the terms M 1 , ..., M n is defined if and only if there exists some substitution δ and a reduction rule gpN 1 , ..., N n q Ñ N such that for all i P t1, ..., nu it holds that N i " M i σ. In this case, let x " gpM 1 , ..., M n q in P else Q would bind x to N δ and continue to execute P .
Additionally, the process calculus provides the instruction eventpF q.P to emit some F P Σ Event as an annotation of the process and continue to execute P . We define the set of these annotations as Events :" tF pt 1 , .., t k q | t i terms, F P Σ Event with arity ku.
The remaining constructs depicted in Figure 3 are standard constructs included in the π-calculus. 0, or the nil process, indicates the end of the process and does nothing. P |Q composes P and Q in parallel and !P represents and unbounded number of copies of P in parallel composition. A channel can be any term M . The process inpM, xq.P receives a message on channel M . It then continues to execute P with x being bound to the received message. outpM, N q.P outputs a term N on channel M and executes P . pνaqP depicts a restriction. It first creates a free name a and then executes P . A free name a is a secret and cannot be guessed, but it may be obtainable via computation/deduction of public messages. The conditional Q compares two terms M and N and executes P if they are equal and Q otherwise. Note that this is just a special case of destructor application. Let equal be a destructor symbol and def pequal q = tequal pM, M q Ñ M u. Then if M " N then P else Q can also be expressed as " equal pM, N q in P else Q with x being not free in P and Q. For brevity, we will omit trailing 0 processes and empty else-branches.

B. Semantics
We define the semantics by first introducing the notions of frame and deduction. A frame νE.δ represents a sequence of messages observed so far and the secrets generated by the protocol. The first is captured by a substitution δ, the latter by the set of used names E.
Deduction describes the capabilities of an adversary to infer and compute new terms from already observed messages. We define the deduction relation νE.δ $ t between a frame and a derivable term as the smallest relation s.t. the rules in Figure  5 hold. We further define f priv as a subset of all constructor symbols where the DCON deduction rule cannot be used. We refer to f priv as private constructor symbols.
The operational semantics are defined by a labeled transition relation between process configurations. This configuration is represented by a 3-tuple pE, P, δq. P is a multiset representation of processes being executed in parallel. E is the set of free names generated by the processes in P. δ is a substitution modeling the messages observed by the environment.
The labeled transition relation of our calculus can be found in Figure 4. Each transition between two configurations is labeled with some F P Events Y tHu. For the ease of presentation, we omit empty sets and write Ñ instead of H Ý Ñ. We define Ñ˚to represent multiple application of transition rules labeled with the empty set. For the other F P Events we define F ù ñ as Ñ˚F Ý ÑÑ˚.
Definition 5 (Traces). Given a process P , we now define its traces: tracespP q " ! pF 1 , ...F n q | pH, tP u, Hq F1 ù ù ñ pE 1 , P 1 , δ 1 q F2 ù ù ñ . . . Fn ù ù ñ pE n , P n , δ n q ) VIII. CASE STUDY: EMAIL We now come back to Speicher et al.'s email case study (Section VI) to investigate the symbolic soundness of their model. Our focus will be on the methodology. We first present a translation from labeled property graphs into processes. Verifying this process for each property graph is impractical, both because of the size of the graph (protocol verifiers do not scale well with the model size) and because any change in the infrastructure would require a new analysis. Hence, we define two process transformations that allow for a sound mapping of all these processes to a single process, i.e. an over-approximation. We verify this process in ProVerif and can thus provide a symbolic soundness result for all process graphs at once.

A. Symbolic model
We define a function F from property graphs to processes in Figure 6. We use the following notation: ‚ For a finite set S " ta, .., zu, sPS P psq denotes P paq | . . . | P pzq. Instead of s P S, we sometimes use set-builder notation to directly define the components of each s. ‚ For a fixed labeled property graph G that is implicit in the context, we write V x as a subset of all nodes in V with label x. We write y L Ý Ñ z to represent an edge in G labelled with L connecting the two nodes x and y. To ease notation, we use d, e for nodes representing domain names, r for resolvers and n for name servers. ‚ We further assume that all nodes are public names, to avoid introducing a mapping. Our process represents SMTP, DNS, DNSSEC, resolvers, and a simplified version of inter-AS communication. As we focus on the methodology, we do not elaborate on the subprocesses modeling these protocols, but on the top-level process that composes them. The processes P smtp-server and P smtp-client describe the client and server roles within the SMTP protocol. Each provider v defines several mail servers d c{s MX (or e c{s MX ) via the MX resource record. Each of those execute both client and server roles. They have one or many IP addresses i c{s MX , which are located in autonomous systems as c{s MX . Whereas the process P smtp-server only models the receiving part of the SMTP protocol, P smtp-client models DNS/DNSSEC requests as well as the client role of SMTP. To establish the connections between the different services, we use the IP addresses to model channels between them. These channels are built over private constructors. In contrast to the Dolev-Yao model, the attacker cannot eavesdrop or manipulate messages per default, but needs to obtain access to these channels by compromising either domain names, IP addresses, or ASes. pE, P Y # t0u, δq Ñ pE, P, δq  The processes P res , P ns , and P rns describe the resolver and server role within the DNS protocol, which, depending on the server's configuration, include the DNSSEC extension. Process P res models the resolver role by communicating with the DNS/DNSSEC infrastructure, on the one hand, and with the requesting role of the mail server. As with the previously mentioned process, the IPs are used to construct private channels via private constructors. The same holds for the name server role modeled by P ns . An exception is the process P rns modeling root name servers. We assume that root servers cannot be corrupted, since that would break the DNS/DNSSEC infrastructure as a whole. Therefore, the attacker is not able to corrupt the connection between the root server process and the process modeling the resolver role. Connections established by the processes P res and P ns , however, may be corrupted by corrupting their domain names, IP addresses, or ASes. For simplicity, we constrained our DNS model to two levels of name servers.
With this construction we represent the structure of the IA model. We instantiate all communication paths and relations in the IA model using the same labeled property graph G. Further, all featured protocols and functionalities of the IA model are represented by subprocesses in our model, as well as the notion of corruption.
In the follow up, we will modify the top-level structure, but leave the processes P smtp-client , P smtp-server , P res , P ns and P rns intact. They are detailed in Appendix C.

B. Proof via sound process transformations
With F, we can, in principle, verify the symbolic soundness of each planning task induced by some property graph G. The respective model FpGq can become very large: property graphs can have thousands to millions of nodes, whereas the majority of protocol models fits on a piece of paper. Protocol verifiers are not optimized for models of this size. Moreover, it is tedious to generate and verify a process whenever a new attacker country is considered or the property graph is modified. Last but not least, the analogy to computational soundness (Sec. II-3) suggest that symbolic soundness results (a) should encompass some set of protocols and (b) apply to any network composed of them, here described by the property graph. 4 Conceptually, we therefore desire a result that is independent of G.
To this end, we propose the following proof technique specific to the applied-π calculus. Let FpGq be a function from property graphs 5 to processes and assume that it can be expressed only using the applied-π calculus and the meta language operation sPS P psq. In the first step, we construct a process P such that, for all G, tracespFpGqq Ď tracespP q. This implies that every trace property that holds for P also holds for FpGq, independent of G. To this end, we apply to two transformations that over-approximates a process.
The first permits substituting several uniform parallel processes sPS P psq by a single process under replication that obtains this input from the adversary. In the description of FpGq, G can only occur within these S, hence the resulting process is now independent of G.

Lemma 1.
With we relate the replication of a process inp Ý Ñ v q.P , where Ý Ñ v can be supplied by the adversary (i.e., the frame), to a finite parallel execution of the same process P , where Ý Ñ v gets substituted with public names supplied by G.
We may now automatically conduct the following verification steps with ProVerif (or any other verifier). ProVerif's abstraction in particular is sensitive to how deep in a process an input occurs. The second transformation thus permits pushing inputs further inside the process to aid verification.
Lemma 2. For all processes Q that contain exactly one subprocess inpxq.P , let Q 1 be Q with P instead of this subprocess. Then: tracespinpxq.Q 1 q Ď tracespQq.
Both lemmas are proven in Appendix B. In the second step, we ensure that these transformations have been correctly applied, i.e., that tracespFpGqq Ď tracespP q follows from Lemma 1 and 2. In the third step, we verify the three syntactic conditions on the planning task. Finally, we use ProVerif to show Condition CS 5. We partition A by postcondition. For this condition to hold, each element must have the following form.
A i " tppre 1 i , tpost i uq, ppre 2 i , tpost i uq, ..., ppre k i , tpost i uqu. We translate each element into a correspondence query: for each trace, if post i occurs then pre 1 i , pre 2 i or any other pre j i , j P t1,¨¨¨, ku, occurs as well. As Condition CS 3 holds for any ProVerif process, we obtain symbolic soundness by Theorem 1.

C. ProVerif Model Introduction
Using the two lemmas above, we can transform all F pGq into the process P , whose structure we present in Figure 7. The full model is in Appendix C.
In this model, the adversary is also able to choose which processes communicate, and thus controls the underlying network topology. Given the process model based on the graph G in Figure 6 and our ProVerif model P , we show that the transformations have been applied correctly.  ! ( i n ( dom c : dom ) ; i n ( i p c : i p ) ; i n ( AS c : a s ) ; ! ( P smtp-client ( prov , dom c , i p c , AS c ) ) ) | ! ( i n ( dom s : dom ) ; i n ( i p s : i p ) ; i n ( AS s : a s ) ; ! ( Psmtp-server ( prov , dom s , i p s , AS s ) ) ) | ! ( i n ( dom r : dom ) ; i n ( i p r : i p ) ; i n ( AS r : a s ) ; ! ( Pres ( dom r , i p r , AS r ) ) ) | ! ( i n ( dom d : dom ) ; i n ( i p d : i p ) ; i n ( AS d : a s ) ; ! ( Pns ( dom d , i p d , AS d ) ) ) | ! ( i n ( dom rn : dom ) ; i n ( i p r n : i p ) ; i n ( AS rn : a s ) ; ! ( Prns ( dom rn , i p r n , AS rn ) ) ) ) Fig. 7: Simplified ProVerif model (inpmq short for inpc, mq).
Lemmas 1 and 2 reduce the proof of this theorem to a structural argument (see Appendix B). The syntactic conditions on the planning task can be verified by inspecting it (Appendix A). Condition CS 1, discussed in Sec. IV-B, holds as there is no negated postconditions. Condition CS 2 holds, as all events in Σ X occur as a postcondition of some rule. Condition CS 4 holds, as all preconditions are in Σ X .

D. Automated verification
It remains to show Condition CS 5, which we verify using ProVerif. The full set of queries is specified in Appendix 1. We grouped these queries according to whether the postcondition expresses a loss of integrity or a loss of confidentiality. We express the first property as a correspondence property and the second as a reachability property known as weak secrecy. For the first kind, we verify that any event matching some pattern e was preceded by an event matching a pattern e 1 . Any trace with an event matching e but not e 1 could be mapped to one where such integrity violation events are specifically marked; these would be the actual events in Σ X . For the second kind, weak secrecy is expressed as usual. The attacker can demonstrate the ability to correctly input a secret message (in this case, the content of an email) in a subprocess. Upon success, the subprocess can be reduced to an event. We analyze the reachability of this event.
During the modeling process, we found two bugs in the IA model. First, in the IA model, Cpipq implies Cpdq if d resolves to ip, but not vice versa. As Cpipq does not represent IP-level attacks, but a compromise of the service identified by ip, this ought to be the case. Without this rule, all rules that concern routing, name resolution or application compromise break down, as they identify the service with the domain it runs on. Luckily, this does not invalidate Speicher et al.'s result, as an inconsistency between the corruption of an IP and a domain can only come from (a) missing or inconsistent information in the property graph, e.g. domains d 1 and d 2 linked to different countries but resolving to the same IP, or (b) from an inconsistent initial network attacker state. We confirmed with the authors that neither condition was met.
The second bug concerns the DNSSEC protocol. DNSSEC requires resolver-side signature validation. This is not always the case for resolvers run by ISPs, but a realistic future scenario to investigate. By contrast, local resolvers (e.g. on clients or services like mail) rely on the ISP's validation during (recursive) resolving and will, at least for the near future, not validate signatures themselves. r dns´route´res [52], however, assumes that this is the case, i.e. that DNSSEC is an effective countermeasure against domain poisoning attacks mounted between the local (recursive, usually non-validating) resolver and the ISP's (iterative, validating) resolver. Presumably, this is a bug, or at least an unrealistic assumption.
To solve the first problem, we added a rule turning Cpdq into Cpipq and use Cpipq in all other rules, instead of Cpdq. To solve the second problem, we altered the rule by deleting the nDNSSEC predicate from the precondition. The changes are highlighted in Appendix A.
ProVerif proves all queries automatically and thus the last condition, CS 5. We used ProVerif version 2.02pl1. On an Intel i7-9750H CPU with 16 GB RAM, the analysis took 9.92s. This concludes our proof for the symbolic soundness.

E. Modeling Challenges
We take the opportunity to discuss some modeling challenges that we encountered and that are specific to our methodology.
The first is the modeling of the infrastructure attacker, who is less powerful than ProVerif's standard network attacker. It can only observe communication if the corresponding route has been compromised. Our first approach used private channels to model non-corrupted transfer of messages. We noticed ProVerif running into termination problems during the resolution. We minimized our model to three parties and found the issue to be ProVerif's internal representation of private channels as Horn clauses. This is because private channels are synchronous, as opposed to free (public) channels. 6 Routing in the Internet is actually asynchronous, so we model secret channels using 2-ary fact symbols req packet, ans packet and the following reduction: get req packetpx, req packetpx, yqq " y.
(The reductions for ans packet are analogous). All parties apply the function symbol with a shared key in the first parameter, to represent communication on that channel. The keys are built over names representing the IP addresses of the communicating parties, as well as a freshly chosen source port (sender) and the publicly known target port. To corrupt a key, the adversary claims the entity as part of its domain. Additionally, the adversary may choose some AS under its control and claims it to be part of the IP route between the communicating parties. With the corruption of this AS, the route is also seen as corrupted and the adversary can claim the key. This in-transit AS corruption model is very similar to the threat model described in the IA model.
The second challenge is how to structure the process such that information about corruption at the routing level is transmitted to processes that represent the resolution or application layer. As an example, imagine the adversary compromising an AS. All service providers affected would need to be informed that they can now output their keys. First attempts with private channels lead to non-termination. Instead, we restructured the process so that an AS compromise is a subprocess of the lower layer. Each entity needs to be compromised separately, but raises the same event Cpasq.
The third challenge is the size of the model. Using ProVerif's pretty printing, the process counts 360 lines, which is unusually large. The queries alone take about 47 lines. The most recent ProVerif release 2.02pl1 improved the verification time from 4 minutes (with 2.01) to about ten seconds. Hence we do not see a reason why the model could not be extended to cover Speicher et al. 's complete model at a reasonable level of abstraction. Nevertheless, a full-blown model of TLS could bring ProVerif to its limits. We suspect the model size is the reason why resolution takes unusually long -typically, ProVerif's analysis takes seconds or does not terminate at all. Disabling either the DNSSEC or DNS processes supports our suspicion that, the model size has a strong impact on the verification time, even though the models are relatively simple. A potential remedy is techniques for vertical and parallel composition (e.g. [20], [15], [27]), which could potentially be used to derive conditions for the composition of IA models.

IX. CONCLUSION
We introduced the first formal approach to justify vulnerability analysis and risk assessment techniques that operate on an Internet-wide scale. We provided a formal methodology to analyze a given model with off-the-shelf verifiers and demonstrated the applicability of our approach for symbolic soundness w.r.t. a real-world IA model. The protocol transformations and modeling tricks to represent infrastructure attackers in the Dolev-Yao model might be of independent interest for protocol analysis, e.g. for the analysis of p2p protocols.
We identify two main limitations: first, the verification of symbolic completeness requires either true 7 support for liveness in existing verifiers, or syntactical conditions that ensure that liveness can be concluded from reachability properties. We speculate that the reason for the lack of support is less in the technical challenges they pose, but the lack of a use case. Processes are expected to specify how a 'good state' can be reached.
The second limitation is the size of the model. We are confident that a holistic analysis of multiple protocols acting in parallel can be conducted for the whole of Speicher et al.'s model, but what if we want to include a full-grown model of different versions of TLS and IPsec? A deeper exploration of protocol composition in light of the infrastructure attacker and IP-like communication may yield a refined verification methodology and perhaps even composition results for IA models.

A. ProVerif queries
In this section, we will present the complete threat model described in [52]. Hence, the following will be freely, but completely cited from [52], except for the modifications marked in bold orange.
We will give each rule, followed by the intuition of what kind of attack it represents.

1) Initially Compromised Nodes:
Rule A.1r init´loc in [52] . All autonomous systems, IPs and domains associated to the attacking country are initially under control of the attacker.
x P AS Y IP Y Dom cn P Cntry x LOC ÝÝÑ n Cpcnq Cpxq Rule A.2 -r init´as [52]. If an AS is under the control of the attacker, any IP which is part of the AS is also under control of the attacker. [52]. If an IP is under the control of the attacker, any domain that resolves to it (even if the attacker cannot interfere with the resolution) is also under the control of the attacker.
Rule A.4 -r init´ip (this rule is new). If a domain is under the control of the attacker, any IP it resolves to (even if the attacker cannot interfere with the resolution) is also under the control of the attacker.

2) Attacks via Routing:
Rule A.5r injection [52] . If the attacker controls an AS which transfers packets from a domain m to some IP address belonging to n and this particular connection is not secured via the VPN mitigations, we assume that the integrity of the communication from m P Dom to n P Dom is compromised. 3) Integrity of domain/MX resolution: Rule A.6r dns´ns [52] . If the attacker controls any name server that could be queried during resolution, we consider the integrity of the domain name resolution compromised.
Although unspecified by RFC 3207, name servers commonly attach an A record whenever they respond to a resolution request with an DNS entry pointing to another name server [28]. This speeds up the resolution and has the pleasant side-effect that the integrity of the resolution does not depend on whether these authoritative the integrity of the resolution of the domain names of the name servers requested, hence the transitive rule for I DNS is not at the attacker's disposal.
Rule A.7r dns´res [52] . If the attacker controls the resolver of a domain, we consider the integrity of any domain name resolution this domain attempts compromised. (Technically, r is an IP address, but we simplified this and the following rule for presentation.) d, e P Dom i P IP d RES ÝÝÑ i Cpiq I DNS pd, eq Rule A.8 -r dns´route´res [52] . If the attacker controls the route from a domain to the resolver this domain uses, we consider the integrity of any domain name resolution this domain attempts compromised , unless the integrity of the resolution is guaranteed by DNSSEC.
Rule A.9r dns´route´ns [52] . If the attacker controls the route from a resolver to some authoritative name server potentially queried during resolution, we consider the integrity of the resolution for this domain name compromised, unless the integrity of the resolution is guaranteed by DNSSEC. Rule A.10r compromise [52] . If a mail server is already compromised, e.g., if it is hosted by an adversarial country, the attacker can compromise the confidentiality of the communication between two mail providers.  [52] . If the sender does not enforce strict host validation, e.g., she is using optimistic STARTTLS, and DANE is not deployed, the attacker can compromise the confidentiality of the communication between two mail providers by intercepting packets on the route between their respective mail servers. unconfpd, eq

B. Lemmas
Before proving Theorem 3, we present the proofs to the two process transformations from Section VIII-B .
Proof of Lemma 2. We can show that for every trace of the process inpvq.Q 1 , the same trace can be produced by Q. In the first process, the adversary has to choose what term it binds to the free variable v in the beginning. Therefore, it needs to deduce T from the frame, s.t. νE.δ $ t. Comparing to Q, we can deduct the same term T by replacing inpvq.Q 1 with Q in the same configuration. Since no rule of our operational semantics deletes any information from the frame, we are able to deduce T at any point during the process execution of Q. This allows us to substitute v with T in both processes, leading to the same set of traces (since the rest of the processes is the same by construction.) Proof. To proof Lemma 1, we start by applying (repl) (see Figure 4) Ý Ñ PN times to the process !inp Ý Ñ v q.P q and get a new process Ñ v in the right process of Lemma 1 are substituted by public names provided by G. We apply the rule (in) also Ý Ñ PN times on Q and the adversary can input the same public names as provided by G since all public names are deducible from the frame. With this transformation of Q we get exactly Hence, we can conclude that Proof of Theorem 3. First, we rearrange the ||-quantification in FpGq (see Figure 6), so that Ý Ñ p consists of all assignments to the meta-variables 8 x, y and z. (By definition, || is associative and commutative.) For the reader's convenience, we index the applied-π variables with the meta-variable they replace. Figure 6). Therefore, by applying Lemma 1 we get: Note that all variables are uniquely named. We can hence exhaustively apply Lemma 2 to P to push all variables in Ý Ñ v to the inside far enough that the resulting process P 1 proto equals P (compare with full model in Appendix C.). Verifying the syntactical equivalence, we obtain: It covers network of clients and servers running the SMTP , DNS and DNSSEC protocols in a setting that civers a simplified version of inter -AS communication . Hence the attacker must corruption communication channels before being able to eavesdrop .

Notes :
We use 9 private constructor symbols , 6 for modeling communication that is secure until corruption , and 4 to deal with state that is secure until corruption . ** Communication :** The protocol for establishing a communication channel is as follows . Say A wants to communicate with B.

At initialization time , A broadcasts information about himself : IP , domain ,
AS , depending on the context , association of an abstract provider (e.g., "I am a mail server of google ") . This information is bundled in transparent constructors , i.e., constructors that can be deconstructed without any additional secrets . Their purpose is to keep the model maintainable , and they are marked with a ' _info ' suffix . Their type is ' service '. 2. ( same for B ) 3. A is instructed by the adversary whom to communicate with ---this is the standard way of modeling arbitrary communication patterns . The communication partner is identified by a term of type ' service ' as output in step 1. $ˆ1 $ 4. ( same for B ) 5. A choses a source port and uses ' c_communicate_src_port ' to communicate it to B . The function symbol is private , but it has a destructor for the source port , meaning that this information is revealed to the attacker . It does not have a destructor for the description of the target service , which is admittedly unintuitive , but was necessary to speed up verification time . As this information is shared at initialization time , it is always available to the attacker anyway . We typed this parameter ( type ' service ') , so we can ensure that the function symbol is indeed used that way . 6. B unpacks this source port using the destructor for ' c_communicate_src_port '. 7. Then the source ports are exchanged in the other direction , B repeats step 5 , but for the function symbol ' r_communicate_src_port '. 8. A receives the source port with the destructor for ' r_communicate_src_port '. 9. Now both parties can build the key that identifies these channels with the function symbol ' chanbuilder '. There are , in fact , two channels , one for messages from A to B , and another for messages from B to A. A party that knows the channel (i.e., a ' chanbuilder -' term , i.e., a term of type 'chan ') can obtain the message on this channel using the destructor ' get_req_packet '.
$ˆ1 $ The exception is the SMTP client process , in which the attacker supplies only the provider (e.g., " google . com ") , as this is the information that the SMTP client has in the real -world (e.g., through the To : field in the email ). Instead , the IP and domain are obtained using the DNS resolver process .
There are five private function symbols for communicating the source port that way , one for every role in the protocol , plus the ' chanbuilder ' function symbol that sets up the channel ( of type 'chan ') . Why is such a complicated protocol necessary ? As outlined in the paper , we use the ' chanbuilder ' terms to establish private -but -asynchronous channels . Hence the need for ' chanbuilder ' to be private . As in the IP protocol , the channel is identified by source and destination IP and port . Hence , these need to be communicated to set up that channel . In the IP protocol , this is part of a handshake . An alternative and seemingly more natural modeling would be to allow to extract the source port from a ' chanbuilder '-term , however , in that modeling , a channel could only be corrupted once the first message has been sent . Our modeling ensures that a channel can be corrupted before the first message is being sent . This explains the need to send the source port before the first message . The message that communicates the source port is in a private constructor to ensure authenticity , so that a channel cannot be manipulated * before * it is corrupted . The terms within that constructor are public or can be computed . We have five different versions of this constructor , one for each party , to again improve verification time . This is a valid modeling choice because in the real world , the message that communicates the source port identifies the intended protocol type and role of the sender via the destination port .
** Storage **: The four remaining private function symbols are used instead of a global storage ( we use ProVerif 's ' table ' feature only for the publicly known public keys of DNSSEC root servers ). They represent local database entries created on initiasation .
-' register_server ' binds an SMPT servers domain to an IP . This is only used by the authoritative nameserver , where it represents its local registration DB . They are generated in the top -level process upon initalisation , where they are controlled by the attacker , but cannot be changed later . It is used to answer 'A '-requests . -' register_provider ' binds providers ( the part of email addresses after the "@ ") to the domains providing SMTP services for them . It is set up just like ' register_server ' but is used to handle 'MX ' -requests . -' register_ns ' binds nameserver to their public keys . ' register_ns ' terms are used by the root server to provide the public key of the authoritative nameserver directly below it . They , again , correspond to a local registration database , are used nowhere else and are controlled by the attacker upon initialisation , but not later . -' valid_prov ' marks a valid provider , e.g., " google . com ". This corresponds to the public ( or the part of the public covered when Speicher et al consider , e.g., the Top -10 providers ) knowing which provider they use .
There are at least two other established ways of implementing a local store . First are ProVerif 's tables , which implements a key / value store . (* global names *) free CLIENT_PORT : port . free SERVER_PORT : port . free RES_PORT : port . free NS_PORT : port .