Programs as Actual Causes: A Building Block for Accountability

Protocols for tasks such as authentication, electronic voting, and secure multiparty computation ensure desirable security properties if agents follow their prescribed programs. However, if some agents deviate from their prescribed programs and a security property is violated, it is important to hold agents accountable by determining which deviations actually caused the violation. Motivated by these applications, we initiate a formal study of programs as actual causes. Specifically, we define what it means for a set of programs to be an actual cause of a violation when they are run concurrently with a set of other programs. Our definitions are inspired by prior work on counterfactual-based actual causation [Halpern and Pearl 2005, Halpern 2008] that defines what it means for an event c to be an actual cause of an event e. Considering programs instead of events as actual causes is appropriate in security settings because individual agents can exercise their choice to either execute the prescribed program or deviate from it. We present a sound technique for establishing programs as actual causes. We demonstrate the value of this approach by providing a causal analysis of a representative protocol designed to address weaknesses in the current public key certification infrastructure. Specifically, we analyze causes of authentication failures of a protocol that leverages a set of notaries to address concerns about trust-on-first-use of self-signed certificates.


Introduction
Accurate blame assignment for security violations is essential in a wide range of settings. For example, protocols for authentication and key exchange [20], electronic voting [30], auctions [28], and secure multiparty computation (in the semi-honest model) [11] ensure desirable security properties if protocol parties follow their prescribed programs. However, if they deviate from their prescribed programs and a security property is violated, determining which agents should be blamed and appropriately punished is important to deter agents from committing future violations. Indeed the importance of blame assignment as a building block for accountability in information systems has been recognized in prior work [1,13,19,21,23,27,33]. This paper focuses on the challenge of blameassignment for security violations. Our thesis is that actual causation (i.e., identifying which agents' deviations caused a specific violation) is a useful building block for blame-assignment in decentralized multi-agent systems, including but not limited to security protocols and ceremonies [5].
Actual causation has been studied extensively in philosophy, law, and computer science where much of the definitional activity has centered around the question of what it means for event c to be an actual cause of event e. An answer to this question is useful to arrive at causal judgments for specific scenarios such as "John's smoking causes John's cancer" rather than general inferences such as "smoking causes cancer". (The latter form of judgments are studied in the related topic of type causation [29].) Notably, Hume [18] identified actual causation with counterfactual dependence-the idea that c is an actual cause of e if had c not occurred then e would not have occurred. While this simple idea does not work if there are independent causes, the counterfactual interpretation of actual causation has been developed further and formalized in a number of influential works (see, for example, [3,16,24,25,29,35]). This concept has generated significant interest in philosophy and law in part because of its connection with issues of moral and legal responsibility (see [17,26]). Indeed that is also why we view actual causation as a useful building block for accountability in security settings.
At the same time, formalizing actual causes as a building block for accountability in decentralized multi-agent systems raises new conceptual and technical challenges beyond those addressed in the literature on events as actual causes. Let us consider a simple protocol example. In the movie Flight [10], a pilot drinks and snorts cocaine before flying a commercial plane, and the plane goes into a locked dive in mid-flight. While the pilot's behavior is found to be deviant-he does not follow the prescribed protocol (program) for pilots-it is found to not be an actual cause of the plane's dive. The actual cause was a deviant behavior by the maintenance staff-they did not replace a mechanical component that should have been replaced according to a prescribed protocol.
This example is useful to illustrate several key ideas about blame-assignment that influence the formal development in this paper. First, it highlights the difference between deviance and actual causes-a difference also noted in prior work on actual causation. This difference is important from the standpoint of accountability. In particular, the punishment for deviating from the prescribed protocol could be suspension or license revocation whereas the punishment for actually causing a plane crash in which people died could be significantly higher (e.g., imprisonment for manslaughter). Second, the example motivates us to hold accountable agents who exercise their choice to execute a deviant program that actually caused a violation. Thus, we focus on formalizing programs (executed by agents) as actual causes of violations rather than individual events as formalized in prior work. Finally, it illustrates the importance of the actual interactions among agents for a violation to occur in a decentralized multi-agent system with non-deterministic execution semantics. For example, had the maintenance staff replaced the faulty component before take-off, the plane would not have crashed. The actual interaction structure thus plays a significant role in our formalization unlike prior work on actual causation [14,16].
The central contributions of this paper are the following: We initiate a formal study of programs as actual causes. Specifically, we define what it means for a set of programs to be an actual cause of a violation when they run concurrently with a set of other programs. We also present a sound technique for establishing programs as actual causes building on prior work on proving security properties of protocols [4,8]. We demonstrate the value of this approach by providing a cause analysis of a representative protocol designed to address weaknesses in the current public key certification infrastructure.
In more detail, our formalization of programs as actual causes proceeds in three stages. The first stage captures two conditions. The Occurrence condition ensures that a safety property was violated on the log. The log records what programs actually executed and how they interacted. This model of a log is appropriate in settings where executed programs are available for analysis during forensics. The Necessity condition ensures that in a counterfactual scenario where all actually executed programs are replaced by the corresponding norms (i.e., the protocol specified ideal programs), the violation goes away on all resulting traces.
The second stage identifies a set X of the actual programs as the suspected cause by requiring three conditions. The Closure condition ensures that every program that interacted with programs in X on the log is also in X. The Sufficiency condition requires that all traces resulting from the execution of X in conjunction with the norms for the other programs restores the violation so long as the programs in X interact in a way consistent with the log. Finally, the Minimality condition requires that no subset of X satisfies Closure and Sufficiency.
The third stage further separates the set X into X d (the actual causes) and X p (the progress enablers). Informally, the actual values sent by the programs in X p are irrelevant to the violation-they merely serve to enable the progress of other programs that is essential for the violation. Roughly, this idea is formalized by replacing messages received by X d from X p by dummy values. An additional Sufficiency' condition requires that the violation is restored under this transformation so long as the programs in X d interact in a way consistent with the log. A Minimality' condition requires that no subset of X d satisfies Sufficiency'.
Our nearest neighbor is a treatment of actual causation by Halpern and Pearl [14,16]. There are analogies between their conditions of Occurrence, Necessity, Sufficiency, and Minimality and our corresponding conditions in the first two stages. However, there are some important points of difference. First, in our non-deterministic, interactive program setting, it is critical to ensure that all interacting agents are identified in the Closure condition and the actual interactions of the suspected causes are held fixed as we move from Occurrence to the Sufficiency condition. There is no analogous concept in the work of Halpern and Pearl. Second, we exploit special characteristics of our security settings to simplify the definition. Specifically, in the Necessity condition when considering counterfactuals (alternative hypothetical scenarios in which the violation does not occur), it is essential to restrict the set of hypothetical scenarios to avoid counter-intuitive cause determinations. Halpern [14] recognizes this problem and considers only "more normal worlds" in his definition. While it may be challenging to figure out how to rank worlds according to normality in certain application domains, our insight is that the protocol-specified prescribed programs provide a natural basis for constructing such a ranking function. Finally, our third stage enables us to separate out the programs in X d whose information flows are causally related to the violation from the programs in X p who are just progress enablers but do not contribute relevant information flows. This distinction is important in security settings but is not considered by Halpern and Pearl.
The rest of the paper is organized as follows. Section 2 describes a representative example which we use throughout the paper to explain important concepts. Section 3 gives formal definitions for programs as actual causes of security violations. We apply the cause analysis to the running example in Section 4. We survey additional related work in Section 5 and conclude in Section 6.

Motivating example
In this section we describe an example protocol designed to increase accountability in the current public key infrastructure. We use the protocol later to illustrate key concepts.
Security protocol. Consider an authentication protocol in which a user (User) authenticates to a server (Server) using a pre-shared password over an adversarial network. User sends its user-id to Server and obtains a key signed by Server. However, User would need inputs from additional sources when Server sends its public key for the first time in a protocol session to verify that the key is indeed bound to Server's identity. In particular, User can verify the key by contacting multiple notaries in the spirit of Perspectives [34]. For simplicity, we assume User verifies Server's public key with three authorized notaries-Notary1, Notary2, Notary3-and accepts the key if and only if the majority of the notaries say that the key is legitimate.
The prescribed programs for Server, User and Notary impose certain requirements on their behavior: (i) Server stores User's password in a hashed form in a secure memory location (ii) User requests access to the account by sending an encryption of the password (along with its identity and a timestamp) to Server after verifying Server's public key with all notaries. User verifies that the majority of the notaries attested to the correctness of the key (iii) The notaries retrieve the key from their databases and attest the key correctly (iv) Server decrypts and computes the hashed value of the password (v) Server then matches the computed hash value with the previously stored value in the memory location when the account was first created; if the two hash values match, then Server grants access to the account to User.
Security property. The prescribed programs in our example aim to achieve the property that only the user who created the account and password gains access to the account.
Compromised Notaries Attack. We describe an attack scenario and use it to illustrate nuances in formalizing programs as actual causes: User and Server execute norms. User sends an access request to Server. Adversary intercepts the message and sends a public key to User pretending to be Server. User checks with Notary1, Notary2 and Notary3 who falsely verify Adversary's public key to be Server's key. Consequently, User sends the password to Adversary. Adversary then initiates a protocol with Server and gains access to User's account.
First, notice that the deviants in this example are Adversary, Notary1, Notary2 and Notary3. Analogous to Hume's notion of counterfactual-based causation, our definition includes a necessity condition that captures the idea that there exists a hypothetical scenario in which the violation goes away. Specifically, we require that when Adversary performs no actions and the notaries, User, and Server follow their protocol-specified programs (norms), the violation goes away.
Second, notice that the deviant programs are not sufficient for the violation to occur without the involvement of User and Server. We thus seek a notion of sufficiency in defining a set of programs as a joint actual cause for the violation. Joint causation is also significant in legal contexts [31]. For instance, it is useful for holding liable a group of agents working together when none of them satisfy the cause criteria individually but together their actions are be found to be a cause. In addition, note that any strict superset of the set {Adversary, Notary1, Notary2, Notary3, User, Server} while being sufficient for the violation contains redundant programs. We will thus impose a minimality requirement on the set of actual causes to remove redundant programs from it.
Third, another nuance in defining the notion of sufficiency is to constrain the interactions among the programs in the actual cause set in a manner that is consistent with their actual interaction as recorded on the log. This constraint on interactions is quite subtle to define: if the constraint is too weak then the violation does not reappear in all traces thus breaking the sufficiency condition; if it is too strong it leads to counter-intuitive cause determinations. For example, a weak notion of consistency is to require that each program locally executes the same prefix in sufficiency as it does on the log. This notion does not work because for some violations to occur the order of interactions among threads is important. A notion that is too strong is to require matching of the total order of execution across all threads. We present a formal notion of log consistency in the next section that balances these competing concerns.
Finally, note that while all three notaries' actions are required for the sequential User to progress (otherwise it would be stuck waiting to receive a message) and the violation to occur, the actual message sent by one of the notaries is irrelevant since it does not affect the majority decision in this example. Thus, separating out programs who are progress enablers from those who provide information that cause the violation is useful for fine-grained causal determination. This observation motivates the final piece of our formal definition. It also helps us identify independent causes, i.e., different sets of programs that independently caused the violation. In our example, we get three different independent causes depending on which notary is treated as a progress enabler.

Actual Cause Definition
We introduce our model in Section 3.1, define auxiliary notions (like log consistency) in Section 3.2, and present the formal definition of programs as actual causes in Section 3.3.

Model
We model programs in a simple concurrent language, which we call L. The language contains sequential expressions, e, that execute concurrently in threads and communicate with each other through send and recv commands. Terms, t, denote messages that may be passed through expressions or across threads. Variables x range over terms. An expression may do one of the following: execute a primitive function ζ on a term t (written ζ(t)), sequentially compose two expressions (written x = e 1 ; e 2 ), check for the truth of a boolean expression (written assert(e)) and send or receive a message (written send(t) and recv(), respectively).
Following standard models of protocols, send and recv are untargeted in the operational semantics: A message sent by a thread may be received by any thread. Targeted communication may be layered on this basic semantics using cryptography. For readability in examples, we provide an additional first argument to send and recv that specifies the intended target (the operational semantics ignore this intended target). Expression send(t) always returns 0 to its continuation. Primitive functions ζ model thread-local computation like arithmetic and cryptographic operations. Primitive functions can also read and update a threadlocal state, which may model local databases, permission matrices, session information, etc. We assume that there is an identity primitive function that returns its argument. This function applied to t is also written t. If the expression e in assert(e) evaluates to a non-true value, then its containing thread gets stuck forever. Each atomic expression is labelled with a unique line number, written b. Line numbers help define logs later. We omit line numbers when they are not relevant. As an example, the following expression receives a message, generates a nonce (through a primitive function new) and sends the concatenation of the received message and the nonce on the network to the intended recipient j. m = recv(); //receive message, bind to m n = new(); //generate nonce, bind to n send(j, (m, n)); //send (m, n) to j For the purpose of this paper, we limit attention to this simple expression language, without recursion or branching. Our definition of actual cause is general and applies to any formalism of (non-deterministic) interacting agents, but auxiliary definitions such as the log, synchronization and log consistency must be modified appropriately.
Operational Semantics. The language L's operational semantics define how a collection of threads execute concurrently. Each thread T contains a unique thread identifier i (drawn from a universal set of such identifiers), the executing expression e, a local stack and a local store. A configuration C = T 1 , . . . , T n models the threads T 1 , . . . , T n executing concurrently. Our reduction relation is written C → C ′ and defined in the standard way by interleaving small steps of individual threads (the reduction relation is parametrized by a semantics of primitive functions ζ). Importantly, each reduction can either be internal to a single thread or a synchronization of a send in one thread with a recv in another thread.
We make the locus of a reduction explicit by annotating the reduction arrow with a label r. This is written C r − → C ′ . A label is either the identifier of a thread i paired with a line number b, written i, b and representing an internal reduction in thread i at line number b, or a tuple i s , b s , i r , b r , representing a synchronization between a send at line number b s in thread i s with a recv at line number b r in thread i r . Labels i, b are called local labels and labels i s , b s , i r , b r are called synchronization labels.
An initial configuration can be described by a triple I, E, Σ , where I is a finite set of thread identifiers, E : I → Expressions and Σ : I → Stores. This defines an initial configuration of |I| threads with identifiers in I, where each thread contains an empty stack, thread i contains the expression E(i) and thread i contains the store Σ(i). In the sequel, we identify the triple I, E, Σ with the configuration defined by it. We also use a configuration's identifiers to refer to its threads.

Logs and their projections
To define actual causation, we find it convenient to introduce the notion of the log of a trace, which is just the sequence of labels on the trace.
The letter l denotes logs. We need a few more straightforward definitions on logs in order to define actual causation. In the sequel, X, Y, Z denote sets of thread identifiers. A sublog of l = r 0 , . . . , r m is a subsequence of r 0 , . . . , r m .

Definition 3 (Closed set of thread identifiers). A set of thread identifiers
X is said to be closed on log l if for every synchronization label i s , b s , i r , b r ∈ l, i s ∈ X if and only if i r ∈ X.
Intuitively, X is closed on l if threads in X synchronize only amongst themselves according to l.
Definition 4 (Local projection of a log). The local projection of a log l with respect to a thread identifier i, written l ↓ i , is the sublog of l containing all local labels whose thread identifier is i. Formally, Definition 5 (Synchronization projection of a log). The synchronization projection of a log l with respect to a set of thread identifiers X, written l| X , is the sublog of l containing synchronization labels from l both of whose thread identifiers are in X. Formally, A log l ′ is called consistent with a log l relative to a set of thread identifiers X if X is closed on l ′ and the local and synchronization labels of threads in X are identical (and identically ordered) in l and l ′ . This is formalized below.
Definition 6 (Log consistency). A log l ′ is said to be consistent with a log l relative to a set of thread identifiers X if the following hold:

Programs as Actual Causes
Our goal is to define actual causes of the violation of an expected security property. By property in this paper we mean any safety property of labelled traces that is closed under permutation of reductions that are unrelated to each other in Lamport's "happens-before" relation [22]. We use ϕ V to denote the complement of such a property (i.e., ϕ V is the set of property-violating traces).
Consider a trace t starting from the initial configuration C 0 = I, A, Σ . Suppose t ∈ ϕ V , so this trace violates the safety property ¬ϕ V . Our definition of actual causation identifies a subset of the threads I as the cause of the violation. To do this, we employ a set of hypothetical counterfactual scenarios, in which subsets of the programs A(i), i ∈ I are replaced by norms or the correct, prescribed programs. Consequently, we assume that we are provided a second function N : I → Expressions such that N (i) is the program that ideally should have been executing in the thread i. Note that for some i, A(i) and N (i) may be equal, but A(i) may still have contributed to the violation in collaboration with other threads j for which A(j) = N (j). For each i, we call N (i) the norm for thread i and A(i) the "actual" for thread i.
We formalize a violation and the corresponding norms in a violation structure, to which our definition of actual causation applies. We impose two conditions on a violation structure. First, there must actually be a violation, else looking for causes is meaningless. We call this condition occurrence. Second, in the extreme counterfactual world where we execute norms only, there should be no possibility of violation. We call this condition necessity. Conceptually, necessity says that the reference standard (norms) we employ to define causes is reasonable.
Definition 7 (Violation structure). A violation structure is a tuple V = I, A, Σ, N , ϕ V , t such that t is a trace starting from I, A, Σ and the following two conditions hold: When considering counterfactuals, we often replace the actuals in a subset Y of the threads I with their norms. The following definition captures the resulting initial configuration.

Definition 8 (Normification). Given a violation structure
Armed with these definitions, we are now in a position to formally define programs as actual causes. Our definition applies in two phases. The first phase identifies suspected causes. Technically, a suspected cause is a minimal, closed set of threads that can account for the violation, even if all other threads are replaced by norms. In the second phase, we refine this set into actual causes and progress enablers. The latter contribute only indirectly to the cause by enabling the actual causes to make progress; the exact values transmitted by progress enablers are irrelevant.
Our Phase 1 definition below determines suspected causes. It contains two conditions. The sufficiency condition tests that the suspected causes, when combined with norms for the remaining threads, suffice to recreate the violation. Technically, we consider all traces from a normified counterfactual, in which the candidate suspected causes (called X in the definition) follow the same sequence of reductions as in the original trace. A key criteria is that X be closed on the violating trace's log. This is important, because any thread that communicates with a suspected cause may have at the least enabled progress of the latter and, hence, contributed to the violation. The minimality condition tests that the identified suspected causes contain no redundant threads.
Definition 9 (Suspected Cause of Violation: Phase 1). Let V = I, A, Σ, N , ϕ V , t be a violation structure and l = log(t). We say that X ⊆ I is a suspected cause of the violation V if the following hold: Let T be the set of traces starting from C ′ 0 that are log-consistent with l relative to X. Then, T is non-empty and T ⊆ ϕ V . 3. (Minimality) No proper subset X ′ of X satisfies conditions 1 and 2.
The Phase 1 definition above identifies a minimal set X of threads, which is sufficient to cause the violation and does not interact with other threads (called Y ). In the Phase 2 definition below, we further partition X into X d (actual cause) and X p (progress enablers) such that the threads in X p contribute only towards the progress of other threads that cause the violation. In other words, the set X p contains all threads whose actual transmitted values are irrelevant.
Briefly, here's how our Phase 2 definition works. We first pick a candidate set X d ⊆ X (where X is the suspected cause set identified in Phase 1) and define X p = X\X d . We consider counterfactual traces obtained from initial configurations in which threads from X p (the hypothesized progress enablers) are completely dropped and, instead, any inputs that threads of X d received from X p are replaced by arbitrary dummy values and, additionally, the synchronizations within X d are the same as in the original violating trace. If a violation appears in all such counterfactual traces, then the partition of X into X d and X p is a good candidate. Of all such good candidates, we choose those with minimal X d (or, equivalently, maximal X p ).
The key technical difficulty in writing this definition is replacing values communicated from X p to X d with arbitrary dummy values. While there are many ways to do this, we choose a simple method: We syntactically transform initial expressions of threads in X d , replacing every recv(), which synchronized with an expression in X p , with a dummy value. Since our communication model is synchronous, we must also erase all send() expressions from threads in X d , if the recipient was in X p . The following definition formalizes this idea. It defines a new initial configuration obtained by replacement with dummy values in X d , removal of X p and normification of threads outside X d and X p . The function f supplies dummy values for use in replacement. In the Phase 2 definition, we quantify universally over this function.
Definition 10 (Dummifying transformation). Let V = I, A, Σ, N , ϕ V , t be a violation structure, X d , X p , Y be disjoint subsets of I, l = log(t) and f : Definition 11 (Actual Cause of Violation: Phase 2). Let V = I, A, Σ, N , ϕ V , t be a violation structure and l = log(t). Let X be a suspected cause of the violation V determined by Definition 9. We say that X d ⊆ X is an actual cause of the violation V if the following hold: More than one minimal set X d may satisfy the above Phase 2 definition for a given violation V . Every such X d is deemed an independent actual cause of the violation.

Causes of Authentication Failures
In this section, we model an instance of our running example based on passwords (Section 2) to demonstrate our definition of actual cause. As explained in Section 2, we consider a protocol session where User, Server and multiple notaries interact over an adversarial network to establish access over a passwordprotected account. We describe a formal model of the protocol in our language, examine the attack scenario from Section 2 and provide a cause analysis using the definitions from Section 3.

Protocol Description
We consider our example protocol with six threads named {Server, User, Adversary, Notary1, Notary2, Notary3}. A relevant part of the norms for all these threads, except Adversary, are shown in Figure 1. Adversary's norm is empty, because in an ideal world, Adversary should not participate. (In our appendix, we demonstrate the cause analysis with more threads which do not interact with these six threads and are filtered out by our Phase 1 definition. We also give the complete proof considering timestamps and the account creation phase.) The norms in Figure 1 assume that User's account (called acct in Server's norm) has already been created and that User's password, pwd is associated with User's user id, uid. This association (in hashed form) is stored in Server's local state at pointer mem. The norm for Server is to wait for a request from an entity, respond with its (Server's) public key, wait for a username-password pair encrypted with that public key and grant access to the requester if the password matches the previously stored value in Server's memory at mem. To grant access, Server adds an entry into a private access matrix, called P . (A separate server thread, not shown here, allows User to access its account if this entry exists in P .) The norm for User is to send an access request to Server, wait for the server's public key, verify that key with three notaries and then send its password pwd to Server, encrypted under Server's public key. On receiving Server's public key, User initiates a protocol with the three notaries and accepts or rejects the key based on the response of a majority of the notaries. For simplicity, we omit a detailed description of this protocol between User and the notaries that authenticates the notaries and ensures freshness of their responses. These details are included in our appendix.
Each notary has a private database of (public key, principal) tuples. The notaries' norms assume that this database has already been created correctly. When User sends a request with a public key, the notary responds with the principal's identifier after retrieving the tuple corresponding to the key from its database. (In this example, we identify threads with principals.) Notation. The norms in Figure 1 use several primitive functions. Enc(k, m) and Dec(k ′ , m) denote encryption and decryption of message m with key k and k ′ respectively. Hash(m) generates the hash of term m. Sig(k, m) denotes message m signed with the key k, paired with m in the clear. pub key i and pvt key i denote the public and private keys of thread i, respectively. For readability, we include the intended recipient i and expected sender j of a message as the first argument of send(i, m) and recv(j) expressions. As explained earlier, i and j are ignored during execution and the adversary, if present, may capture or inject any messages.
Security property. The security property, ¬ϕ V , of interest to us is that if at time u, a thread k is given access to account a, then k owns a. This can be formalized by the following logical formula: ∀u, k, a. (a, k) ∈ P (u) ⊃ Acct.user(a, k, u) Here, P (u) is the state of the access control matrix P at time u and the predicate Acct.user(a, k, u) holds if the thread k owns account a at time u. We assume that User, not Adversary, owns account acct. (We use this logical formalization of the property in establishing the actual causes using our definition. Specifically, we use a program logic to establish the sufficiency' and necessity conditions.)
It is instructive to understand the proof of this theorem, as it illustrates our definitions of causation. We verify that V is a violation structure and that our Phase 1 and Phase 2 definitions yield exactly the three values for X d mentioned in the theorem. To check that V is a violation structure, we must verify the occurrence and necessity conditions from Definition 7. For occurrence, we must show that t ∈ ϕ V . This is clear because at the end of the trace, (acct, Adversary) ∈ P , but by our assumption, User, not Adversary owns acct. For necessity, we show that any trace starting from I, N , Σ cannot be in ϕ V , i.e., any such trace has the invariant (2) [Security property]. To prove this, we can use any sound program logic. In particular, we use the logic of Garg et al. [8]. Our proof, in fact, shows the stronger property that (2) is an invariant even when the six norms execute concurrently with any number of standard Dolev-Yao adversaries (we assume that encryption is non-malleable). This is just a standard proof of protocol correctness with a program logic, so we defer its details to our appendix.
Phase 1: Phase 1 (Definition 9) determines X = I and Y = I\X = {}. This is easily proved: I contains a single connected component in the synchronization graph induced by l, so closure of X on l forces X = I or X = {}. If X = {}, then Y = I, so in the sufficiency condition, we would have to produce a violation using norms for all six threads, which we proved impossible in the necessity condition above. Hence, X = I. Phase 2: Phase 2 (Definition 11) determines three independent actual causes for X d : {Adversary, User, Server, Notary1, Notary2}, {Adversary, User, Server, Notary1, Notary3}, and {Adversary, User, Server, Notary2, Notary3}. These are symmetric, so we only explain why X d = {Adversary, User, Server, Notary1, Notary2} satisfies Definition 11. We show that (a) This set X d satisfies sufficiency', and (b) No proper subset of X d satisfies sufficiency' (minimality').
We start with (a). By definition, X p = X\X d = {Notary3}. Fix any dummifying function f . We must show two things. First, there is a trace from dummify(V, X d , X p , f ), whose log is consistent with l relative to X d . Second, any such trace is in ϕ V . The first statement is easily established by mimicking the execution in l starting from dummify(V, X d , X p , f ). The only potential issue is that on line 8, A(User) (which equals N (User) from Figure 1) synchronizes with Notary3 according to l, but Notary3 does not exist in dummify(V, X d , X p , f ). However, in dummify(V, X d , X p , f ), the recv() on line 8 in A(User) is replaced with a dummy value, so the execution from dummify(V, X d , X p , f ) progresses. Subsequently, the majority check on line 9 succeeds as in l, because two of three notaries (Notary1 and Notary2) still attest the Adversary's key.
The second statement -that every trace starting from dummify(V, X d , X p , f ), whose log is consistent with l relative to X d , is in ϕ V -is the most non-obvious part of our proof. This statement quantifies over a select set of traces, but not all, so we cannot directly use the program logic. Instead, we use the program logic to establish certain invariants and combine those invariants with our knowledge of l. Fix a trace t ′ with log l ′ . Assume l ′ consistent with l relative to X d . We show that t ′ ∈ ϕ V as follows.
1. Since l ′ is consistent with l relative to X d , Server must execute line 9 of its program N (Server) in t ′ . Consequently, at some point of time, the access control matrix P contains (acct, J) for some J. 2. We prove an invariant of N (Server) that if it writes (x, J) to P , then J is the third component of a tuple obtained by decrypting a message received on line 3. 3. Since l ′ is consistent with l relative to X d , and on l Server, 3 synchronizes with Adversary, 8 , J must be the third component of an encrypted message sent on line 8 of A(Adversary).

We prove an invariant of A(Adversary)
that the third component of the message sent on line 8 is exactly the term "Adversary". (This is easy to establish, as the term "Adversary" is hardcoded on line 7.) Hence, J = Adversary. 5. This immediately implies that t ′ ∈ ϕ V since (acct, Adversary) ∈ P , but by assumption, User, not Adversary owns acct.
) and, hence, on any counterfactual trace cannot write to P , thus precluding a violation. Therefore, Server ∈ X ′ d . By sufficiency', for any f , the log l ′ of at least one trace t ′ of dummify(V, X ′ d , X ′ p , f ) must be consistent with l relative to X ′ d . This means that in t ′ , the assertion on line 5 of N (Server) must succeed and, hence, on line 4, the correct password pwd must be received by Server, independent of f . This immediately implies that Adversary (which sends that password on l) must be in X ′ d , else some dummified executions of Server will have the wrong password and the assertion on line 5 will fail.
Extending this logic further, we now observe that because Adversary forwards a password received from User (line 3 of A(Adversary)) to Server, User ∈ X ′ d (otherwise, some dummifications of line 3 of A(Adversary) will result in the wrong password being sent to Server, a contradiction). Since User ∈ X ′ d and l ′ must be consistent with l relative to X ′ d , the majority check on line 9 of N (User) must also succeed. This means that at least two of {Notary1, Notary2, Notary3} must be in X ′ d , else the dummification of lines 6-8 of N (User) will cause the assertion check to fail for some f . Since X ′ d ⊆ X d , these two threads must be {Notary1, Notary2}. At this point we have established that each of {Adversary, User, Server, Notary1, Notary2} is in X ′ d . Hence, X ′ d = X d .

Related Work
Currently, there are multiple proposals for providing accountability in decentralized multi-agent systems [1,2,6,7,12,13,19,21,32]. Although the intrinsic relationship between causation and accountability is often acknowledged, the foundational studies of accountability do not explicitly incorporate the notion of cause in their formal definition or treat it as a blackbox concept without explicitly defining it. Our thesis is that accountability is not a trace property since evidence from the log alone does not provide a justifiable basis to blame agents.
On the other hand, prior work on actual causation in analytical philosophy and AI has considered counterfactual based causation in detail [3,15,16,25,29,35]. These ideas have been applied for fault diagnosis where system components are analyzed, but these frameworks do not adequately capture all the elements crucial to model a security setting. Executions in security settings involve interactions among concurrently running programs in the presence of adversaries, and little can be assumed about the scheduling of events.

Accountability
Küsters et al [21] define a protocol P with associated accountability constraints that are rules of the form: if a particular property holds over runs of the protocol instances then particular agents may be blamed. Further, they define a judge J who gives a verdict over a run r of an instance π of a protocol P , where the verdict blames agents. Instances of P are non-deterministic processes with concurrently executing programs. In their work, Küsters et al assume that the accountability constraints for each protocol are given and complete. They state that the judge J should be designed so that J's verdict is fair and complete w.r.t. these accountability constraints. They design a judge separately for every protocol with specific accountability property. In contrast, our cause definition provides a semantic basis for arriving at such accountability constraints, thereby providing a justification for the blame assignment suggested by those constraints. Our actual cause definition can be viewed as a generic judging procedure that is defined independent of the violation and the protocol. In Küsters et al.'s framework, it is desirable that a judge give "minimal" verdicts and not blame agents who deviate in a manner that is not relevant to the violation. However, there is no formal definition for a verdict being minimal. We believe that using our cause definition as the basis for accountability constraints would ensure the minimality of verdicts.
Backes et al [1] define accountability as the ability to show evidence when an agent deviates. The authors analyze a contract signing protocol using protocol composition logic and prove certain properties about the protocol. In particular, the authors consider the case when the trusted third-party acts dishonestly and prove that the party can be held accountable by looking at a violating trace. This work can be viewed as a special case of the subsequent work of Küsters et al. where the property associated with the violating trace is an example of an accountability constraint.
Feigenbaum et al [6,7] also propose a definition of accountability that focuses on linking a violation to punishment. They use Halpern and Pearl's definition [15,16] of causality in order to define mediated punishment, where punishment is justified by the existence of a causal chain of events in addition to satisfaction of some utility conditions. We think that the use of causality in that setting is an apt choice. The underlying ideas of our cause definition could be adapted to their framework to instantiate the causality notion that is currently used as a black box in their definition of mediated punishment. One key difference is that we regard programs as causes of violations while they establish a causal chain between violation and punishment events. While the event-based view is suitable for their work, we discuss in Section 1 why that view is not suitable for our purposes. Jagadeesan et al [19] provide a definition of accountability in the context of authorization in distributed systems. Their analysis models an auditor as an honest agent of the protocol and uses game-based logics in order to study the tradeoffs between the requirements for honest agents and the audit protocols. The auditor considers the actions of agents in the protocol and can assign blame to the agents deviating from the protocol. In contrast, in our work, we consider a trace-based model where a violation is detected on a finite trace and reason about an agent's program being a cause of the violation (not just a deviant).
Haeberlen et al [13] provide a definition of accountability in distributed systems. Their system, PeerReview, maintains a record of all nodes' actions and provides non-repudiable evidence when a node deviates from its local protocol. The 'violation' occurs when a node does not respond to a message as expected by the protocol or sends a message not prescribed by the protocol. The motivation of this work differs from ours as we try to find causes of a global violation of a protocol specification. We differentiate between deviance, which occurs when an agent does not follow its locally specified program and a global violation, which occurs when a protocol property is not satisfied.

Causation for blame assignment
The work by Barth et al [2] provides a definition of accountability that uses the much coarser notion of Lamport causality. Lamport causality is related to closure in Phase 1 of our definition. However we use minimality checks and filter out progress enablers in Phase 2 to obtain a finer determination of actual cause.
Gössler et al [12] use causation to link deviation of local specification by individual components of the system with the violation of the global specification, i.e., system failure. They treat components as black boxes which have local contracts specifying the desired behavior and model each component as a labelled transition system. The authors consider a trace-based model and reconstruct traces by replacing prefixes of traces containing actions of faulty components by outputs which would have arisen had the components followed their contracts. An important distinction from our formalization is that they consider alternative scenarios where inputs and outputs of components can be constrained, without taking into effect all interactions. It is not possible to construct alternate traces where faulty components interact with other components in a manner different from that on the log. Preserving the interaction structure on the log is crucial for our definitions.
Wang et al [32] describe a counterexample to Gössler et al's work [12] where all causes are not found because of not being able to completely capture the effect of one component's behavior on another's. Wang et al [32] propose an approach similar to Gössler et al's for determining blameworthy components in fault diagnosis. However, they differ in the manner of reconstructing traces and finding causes. Here too, alternate traces cannot be generated since components are considered black box.

Conclusion
We have presented a first attempt at defining what it means for a set of programs to be an actual cause of a violation of a security property. This question is motivated by security applications where agents can exercise their choice to either execute a prescribed program or deviate from it. While we demonstrate the value of this definition by analyzing a set of authentication failures, it would be interesting to explore applications to other protocols in which accountability concerns are central, in particular, protocols for electronic voting and secure multiparty computation in the semi-honest model. Another challenge in security settings is that deviant programs executed by malicious agents may not be available for analysis; rather there will be evidence about certain actions committed by such agents. A generalized treatment accounting for such partial observability would be technically interesting and useful for practical applications. Protocol Description We consider our example protocol with nine threads named {Server1, User1, Adversary, Notary1, Notary2, Notary3, Notary4, Server2, User2}. The norms for all these threads, except Adversary are shown in Figure 3 and 4. The Adversary's norm is empty, because in an ideal world, the Adversary should not participate. In this case study, we have two servers (Server1, Server2) running the protocol with two different users (User1, User2) and each server allocates account access separately.
The norms in Figures 3, 4 assume that User1's and User2's accounts (called acct 1 and acct 2 in Server1's and Server2's norm respectively) have been created already. User1's password, pwd 1 is associated with User1's user id uid1. Similarly User2's password pwd 2 is associated with its user id uid2. User1 generated pwd 1 associated with acct 1 and User2 created pwd 2 associated with acct 2 . This association (in hashed form) is stored in Server1's local state at pointer mem 1 (and at mem 2 for Server2). The norm for Server1 is to wait for a request from an entity, respond with its public key, then wait for a password encrypted with that public key and grant access to the requester if the password matches the previously stored value in Server1's memory at mem 1 . To grant access, Server1 adds an entry into a private access matrix, called P 1 . (A separate server thread, not shown here, allows User1 to access its resource if this entry exists in P 1 .) The norm for User1 is to send the password pwd1 to Server1, encrypted under Server1's public key and not share the password with any other agent. On receiving Server1's public key, User1 initiates a protocol with the three notaries and accepts or rejects the key based on the response of a majority of the notaries.
The norm for User2 is the same as that for User1 except that it interacts with Server2. Note that User2 only verifies the public key with one notary, Notary4.
The norm for Server2 is the same as that for Server1 except that it interacts with User2.
Each notary has a private database of (public key, principal) tuples. The norms here assume that this database has already been created correctly. When User1 or User2 send a request with a public key, the notary responds with the principal's identifier after retrieving the tuple corresponding to the key in its database. (Note that, in this simple example, we identify threads with principals, so the notaries just store an association between public keys and their threads.)

Preliminaries
Notation The norms in Figures 3, 4 use several primitive functions. pub key i and pvt key i denote the public and private keys of thread i, respectively. For a given (public or private) key k, Inv(k) denotes the corresponding private or public key for k. For readability, we include the intended recipient i and expected sender j of a message as the first argument of send(i, m) and recv(j) expressions. As explained earlier, i and j are ignored during execution and the adversary, if present, may capture or inject messages. P 1 (u) and P 2 (u) denotes the tuples in the permission matrices at time u. Initially P 1 and P 2 do not contain any access permissions.

Action Predicates and terms
-Send(i, j, m) @ u holds if thread i sends message m to thread j at time u. Assumptions: (A1) We are interested in security guarantees about honest users who create accounts by interacting with the server and who do not share the generated password or user-id with any other principal except for sending it according to the roles specified in the norms. (A2) HonestThread(User1, N (User1)) (A3) HonestThread(Adversary, A(Adversary)) A principal following the protocol never shares its keys with any other entity. We also assume that the encryption scheme in semantically secure and nonmalleable. Since we identify threads with principals therefore each of the threads are owned by principals with the same identifier, for instance Server1 owns the thread that executes the program N(Server1). (Start1) where i refers to all the threads in the set described above.
Security property The security property of interest to us is that if at time u, a thread k is given access to account a, then k owns a. Specifically, in this example, we are interested in the a = acct 1 and k = User1. This can be formalized by the following logical formula, ¬ϕ V : Here, P 1 (u) is the state of the access control matrix P 1 for Server1 at time u. (We use this logical formalization of the property in establishing the actual causes using our definition. Specifically, we use a program logic to establish the sufficiency' and necessity conditions.) Attack As an illustration, we model the "Compromising Notaries (Man in the Middle)" violation of Section 2. In this attack scenario, User1 and Server1 execute norms. User1 sends an access request to Server1 which is intercepted by Adversary who sends its own key to User1 (pretending to be Server1). User1 checks with the three notaries who falsely verify Adversary's public key to be Server1's key. Consequently, User1 sends the password to Adversary. Adversary then initiates a protocol with Server1 and gains access to the User1's account. Note that the actual programs of the three notaries attest that the public key given to them belongs to Adversary. User2, Server2 and Notary4 execute their norms in order to access the account acct 2 as well.
In the property-violating trace, User1, Server1, User2, Server2 and Notary4 execute their norms and the expressions executed by Adversary and the three deviant notaries are shown in Figure 5. Thus, the initial configuration has the programs: For this attack scenario, the concrete trace we consider is any arbitrary interleaving of the logs for X = {Adversary, User1, Server1, Notary1, Notary2, Notary3} and Y = {Server2, User2, Notary4} shown in Figure 6. Any such interleaved log is denoted l in the sequel.
Phase 1: The closure condition of Phase 1 (Definition 9) can be satisfied by the following four values of X: X 1 = I, X 2 = {}, X 3 = {Notary4, Server2, User2} and X 4 = {Adversary, User1, Server1, Notary1, Notary2, Notary3}. When X = X 2 or X = X 3 , norm(V, X, Y ) contains only norms for all nine threads. We have already established in necessity that starting from all nine norms, we cannot obtain a violation, so sufficiency cannot be satisfied for these two values of X. That leaves only X = X 1 and X = X 4 . We now show that X = X 4 satisfies sufficiency. (Since X 4 ⊆ X 1 , minimality then implies that the X determined by Definition 9 must be X 4 .) Following the statement of sufficiency, let T be the set dummify(V, X ′ Expanding the steps: We adapt the definitions from the proof of secrecy for Kerberos by Garg et al [9] for a framework based on asymmetric encryption. Some of these definitions are given in Figure 7. For more details, we refer the reader to [9]. Here K denotes a set of keys. OwnedIn(i, S) means that thread i in in set S, OrigRes(s, S) means that the thread which created the term s lies in set S, KeyRes(K, S) means that the inverse key corresponding to each key in set K is known only to threads in S. KORes(s, K, u) combines the previous two predicates, SendsSafeMsg(i, s, K) means that if thread i sends s in a message, then all occurrences of s in that message are protected by keys in Inv(K) i.e. the private keys corresponding to the public keys in K. SafeNet(s, K, u) means that prior to time u, every thread protects s in all messages it sends using keys in Inv(K). Figure 7 also lists two axioms (POS) and (NET) from prior work. We introduce an additional axiom called (NM). This axiom (assuming non-malleability) states that if only principals in set P had access to the corresponding private keys for set K and have knowledge of terms in s, then if a message m containing secret s is encrypted under a key k ∈ K and sent at time u, then at a prior time u ′ some principal in P must have sent the message on the network.
We prove that if access permission (acct 1 , k) is added in P 1 for principal k, then k = User1.