Steve Kremer

Robert Künnemann

Graham Steel

Universally Composable Key-Management

Keywords: Key management, Security APIs, Universal Composability Management . . . . . .

We present the first key-management functionality in the Universal Composability (UC) framework. It allows the enforcement of a wide range of security policies and can be extended by diverse key usage operations with no need to repeat the security proof. We illustrate its use by proving an implementation of a Security API secure with respect to arbitrary key-usage operations and explore a proof technique that allows the storage of cryptographic keys externally, a novel development in the UC framework.

Introduction

Security critical applications often store keys on dedicated hardware security modules (HSM) or key-management servers to separate highly sensitive cryptographic operations from more vulnerable parts of the network. Access to such devices is given to protocol parties by the means of Security APIs. Examples of such APIs are the RSA PKCS#11 standard [RSA04], IBM's CCA [CCA06] and the trusted platform module (TPM) [TCG07] API. Building on the work of Longley and Rigby [LR92] and Bond and Anderson [BA01] on API attacks, several recent papers have investigated the security of APIs on the logical level, often using symbolic techniques for protocol analysis, e. g., [BCFS10,CKS07,DKS10]. More recent work has tried to define appropriate security notions for APIs in terms of cryptographic games [CC09,KSW11]. This has two major disadvantages: first, it is not clear how the security notion will compose with other protocols implemented by the API, and second, it is difficult to see whether a definition covers the attack model completely, since the game can be tailored to a design. For example, the security game may not permit re-importing wrapped keys [CC09]. This illustrates that game-based definitions are very difficult to get right in this domain. Since security APIs are first and foremost used as building blocks in other protocols, composability is crucial. In this work, we will follow the more general approach to API security of Kremer et al. [KSW11], but using a framework that allows for composition.

Composability can be proven in frameworks for simulation-based security, such as Universal Composability (UC) [Can05]. The requirements of a protocol are formalized by abstraction: an ideal functionality computes the protocol's inputs and outputs securely, a 'secure' protocol is one that emulates the functionality. Simulation-based security naturally models the composition of the API with other protocols, so that proofs of security can be performed in a modular fashion.

Over time a number of shortcomings have been found in the UC framework, leading to the contribution of other frameworks in the same spirit [BDHK07,HS11,Küs06,MR11]. Some particular weaknesses of the UC framework are the following: First, it is assumed that sessions of running protocols are identifiable by a (pre-established) session identifier, abbreviated as sid , although it is possible to define composition on protocols without such identifiers. For a Security API, one could argue that a serial number constitutes such an identifier. Still, the identifier is part of every incoming and outgoing message, which is a rather unrealistic modelling of locality information. Second, adaptive corruption of parties, or of keys that produce an encryption, provokes the well-known commitment problem [Hof08], so we will have to place some limitations on the types of corruptions that can occur. We therefore restrict the environment to avoid these problems. Third, the proof of the composition theorem is flawed due to an inadequate formulation of the composition operation [HS11], though here the authors remark that, "none of the objections we raise point to gaps in security proofs of existing protocols. Rather, they seem artifacts of the concrete technical formulation of the underlying framework.". We employ UC despite its shortcomings, because it is well-studied and hence provides a common ground for transferring this first approach on modelling key-management to other frameworks.

Contributions. We present, to the best of our knowledge, the first composable definition of secure key-management in form of a key-management functionality F KM . It assures that keys are transferred correctly from one Security API to another, that the policy is respected and that operations which use keys are computed correctly. The latter is achieved by describing operations unrelated to key-management by so-called key-usage functionalities. F KM is parametric in the policy and the set of key-usage functionalities, which can be arbitrary. This facilitates revision of security devices, because changes to operations that are not part of the key-management or the addition of new functions does not affect the UC emulation proof. In order to achieve this extensibility, we investigate what exactly a "key" means in simulation-based security. Common functionalities in UC do not allow two parties to share the same key, in fact, they do not have a concept of keys, but a concept of 'the owner of a functionality' instead. The actual key is kept in the internal state of a functionality, used for computation, but never output. Dealing with key-management, we need the capability to export and import keys and we propose an abstraction of the concept of keys, that we call credentials. The owner of a credential can not only compute a cryptographic operation, but he can also delegate this capacity by transmitting the credential. We think this concept is of independent interest, and as a further contribution, subsequently introduce a general proof method that allows the substitution of credentials by actual keys when instantiating a functionality. Some aspects of the ideal functionality F crypto by Küsters et al. [KT11] are similar to our key-management functionality in that both provide cryptographic primitives to a number of users and enjoy composability. However, the F crypto approach aims at abstracting a specified set of cryptographic operations on client machines to make the analysis of protocols in the UC model easier, and does not address key-management nor policies.

Limitations. The key-management functionality is tightly coupled with a functionality F KW used to transfer keys from one device to another. This functionality describes a deterministic authenticated symmetric encryption scheme that is secure against key-dependant messages. While deterministic, symmetric authenticated encryption is indeed typically used to transfer keys (see, e. g., RFC 3394), it restricts the analysis to security devices providing this kind of encryption. We

have not yet covered asymmetric encryption of keys in F KW (as opposed to asymmetric encryption of user-supplied data), although F KW could in theory be altered to support this.

A key-management functionality

In this section we introduce our key-management functionality F KM . We will work in the 2005 version of Universal Composability (UC) framework [Can05], described briefly below. We do not want to hard code the cryptographic operations, which are orthogonal to the key management part that can be provided by our security API. Therefore we introduce the notion of key-usage functionalities. Finally, we will discuss the formalization of security policies, which define the expected security guarantees. At the end of this section we give a detailed description of the key-management functionality F KM .

Universal Composability

In the UC framework, the security goal of a protocol is specified by a so-called ideal functionality, which acts as a third party and is trusted by all participants. A set of users, the protocol parties, as well as a distinguished user, the adversary, interact with the functionality using private, authenticated channels. Using the inputs of the parties, the ideal functionality defines a secure way of computing anything the protocol shall compute, explicitly computing the data that is allowed to leak to the attacker. For instance, a secret channel is specified as a functionality that takes a message from Alice and sends it to Bob, notifying the attacker of the length of the message, which would be leaked if this channel were to be realized using encryption. Each of the parties and functionalities are interactive probabilistic polynomial time (PPT)-in a given complexity parameter η-Turing machines, communicating via tapes. A protocol is a network of interactive PPT Turing Machines that communicate with each other, but receive protocol inputs and send protocol outputs to the environment. Roughly, security of a protocol is expressed as indistinguishability of the protocol from an ideal system. We introduce another party, the environment E, whose role is to distinguish whether it is interacting with the ideal system (users interacting with an ideal functionality) or the real system (users executing a protocol). We say that a protocol π UC-emulates a functionality F if for all attackers interacting with π, there exists an attacker, the simulator Sim, interacting with F, such that no environment can distinguish between interacting with the attacker and the real protocol π, or the simulation of this attack (generated by Sim) and F. Canetti [Can05] showed that it is actually not necessary to quantify over all possible adversaries: the most powerful adversary is the attacker that merely acts as a relay forwarding all messages between the environment and the protocol. This attacker is called the dummy-attacker D. We will denote by EXEC η π,A,E (respectively IDEAL η F ,A,E ) the distribution over traces generated by the execution of the system consisting of the protocol π (respectively a set of users interacting with the ideal functionality F), the adversary A and the environment E. (EXEC η π,A,E ) η and (IDEAL η F ,A,E ) η denote the families of distributions (ensembles) indexed by the complexity parameter η. We denote by (D 1 ) η ≈ (D 2 ) η the usual notion of indistinguishability of ensembles. This allows us to define UC realizability.

Definition 1 (UC realization). Let π and F be PPT Turing machines. π UCemulates

F, denoted π ≤ UC F, if ∃S. ∀E : (EXEC η π,D,E ) η ≈ (IDEAL η F ,Sim,E ) η
Canetti [Can05] has also shown that this notion of security is compositional and that ideal functionalities can be replaced by their realization in an arbitrary context, while preserving security properties. In some cases, in particular to handle some forms of key corruption, we will have to assume conditions on the environment. Then, of course, composition is limited to environments where those conditions can be guaranteed to hold.

Definition 2 (Conditional UC realization). Let π and F be PPT Turing machines. π UC-emulates

F under condition C, denoted π ≤ C UC , F) if ∃S. ∀E : Pr[EXEC η π,D,E = 1|C] -Pr[IDEAL η F ,Sim,E = 1|C]
is negligible in η and C is the event that the view of E fulfils some predicate.

Global Structure

One of the main problems in key-management is that a distributed system of security tokens ST 1 . . . ST m has to implement a security policy globally: ST 1 . . . ST m should behave like a global key-storage device that everyone can access securely and that assures that the policy is not violated. We use the concept of UC emulation to express exactly that. We define a key-management functionality F KM , detailed below in Listing 1.1, which is an abstraction of our expectation of key-management.

In Figure 1, we sketch how ST 1 ,. . . ,ST m UC-emulate the functionality in a network with an environment E, a dummy attacker D, respectively a simulator S and a number of other functionalities (depicted as circles) that will be presented below. The environment accesses the security tokens, respectively F KM through dummy users ϕ i and φ i : they take inputs from the environment and send them to the Security API they are connected to (and vice versa). The only difference between ϕ i and φ i is that ϕ i forwards its input to ST i , while φ i forwards it to F KM . These users are needed to hide that in the ideal system the environment interacts with a single machine while in the distributed implementation it interacts with different security tokens.We will denote the network identity of both ϕ i and φ i , with U i and the adversary's network identity with A.

(Cmd,h,m) (Cmd,cred,m) (Cmd,h,m) (Cmd,cred,m) E D ϕ1 . . . ϕm ST 1 . . . ST m F1 • • • F F KW E S φ1 . . . φm ST 1 . . . ST m F1 • • • F F KW
To transfer a key from one security token to another in the real world, the environment instructs, for instance, U 1 to ask for a key to be wrapped. A wrapping of a key is the encryption of a key with another key, the wrapping key, so that it can be transferred from one security token to another without revealing the key. The wrapping key must of course be on both security tokens prior to that. U 1 will receive the wrap from ST 1 and forward it to the environment, which in turn instructs U 2 to unwrap the data it just received from U 1 . In the ideal world, F KM enforces that, if the wrapping that was just sent to U 1 is unwrapped by U 2 , then U 2 gains access to the key that was only available to U 1 , and that attributes associated with that key stay the same. ST 1 and ST 2 have to assure the same properties, as otherwise the environment could distinguish between the real world and the ideal world.

Key-Usage Functionalities

We classify cryptographic operations by whether they operate on user-data (with keys), or on keys (with other keys). We call the latter key-management, the former key-usage. We are specific about how keys are managed: we require the key-management task to be solved using deterministic, authenticated, symmetric encryption, provided by the functionality F KW (detailed in Appendix A). However, for key-usage operations we do not care for much more than their correct implementation, thus keeping F KM extensible by all kinds of cryptographic primitives.

In UC, a cryptographic operation is specified by a functionality F, a fact that we will exploit for the definition of F KM . Let F 1 ,. . . ,F l be the key usage functionalities (also depicted in Figure 1). For every key-usage operation, F KM calls the corresponding KU-functionality, receives the response and outputs it to the user. We define F KM for arbitrary key-usage operations, and consider a security token secure, with respect to a certain policy and the implemented KU-functionalities, if it emulates the ideal functionality F KM parametrized by those KU-functionalities. This allows us to provide an implementation for secure key-management with respect to a certain policy, and arbitrary key-usage operations, see Section 3. We achieve composability in the following sense: if a device performs the key-management according to our implementation, it does not matter how many, and which functionalities it enables access to, as long as those functionalities provide the amount of security the designer aims to achieve (cf. Theorem 12). Notably, the KU-functionalities appear on both sides in Figure 1. In Section 4, we show how to make use of the UC Theorem to instantiate a KU-functionality by an implementation that UC-emulates it.

This approach imposes some mild assumptions on the KU-functionalities. The computation of a KU-functionality F must be independent of the value of the caller's identity, as otherwise a response forwarded by F KM might differ from a response forwarded by ST i . Many of the functionalities in, for example, [Can05] bind the roles of the parties, e. g., signer and verifier, to network identities . An implementation of those functionalities usually employs keys. However such functionalities are not caller-independant. They fail to capture the fact that a key allows to pass the capacity to, e. g., generate valid signatures for a certain verification key from one ST to another.Therefore, the privilege to perform an operation must be transferable as some piece of information, which cannot be the actual key, if we want to prove such a functionality to be secure: a signing functionality, for example, that exposes its keys to the environment is not realizable, since the environment could then generate dishonest signatures itself. The solution is to generate a key, but only send out a credential, which is a hard-to-guess pointer that refers to this key. Whoever knows the credential is allowed to sign. Keys not only allow a distinguished party, the owner of the key, to perform operation but also allow delegation of this capacity. Abstraction of 'keys' by 'credentials' is thus more powerful than abstraction of the 'owner of a key' by a 'fixed identity of party that is allowed to sign'. In our scenario, where keys are exported, it is necessary to abstract keys. The requirements on a KU-functionality are formalized by the following definitions.

Definition 3 (caller-independence). A functionality is F caller-independent iff at any point of the execution of F with any environment, if m is a message and id , id are two identities of network parties, different from the adversary, then the distributions of the outputs of F after receiving m from id , respectively id , are the same.

Definition 4 (key-manageable functionality). A functionality F is keymanageable iff it accepts requests of the form (Command, sid , m) for a finite set of commands C containing at least Generate, Corrupt ∈ C and CorruptionStatus ∈ C, and if it is caller independent.

The key-management functionality F KM expects the response to Generate to be of the form (Generate • , sid , credential).

Remark 1: Since keys might be used to wrap other keys, we would like to know how the loss of a key to the adversary affects the security of other keys. When an adversary "corrupts a key" in F KM , he learns the credentials to access the functionalities. The functionalities will not be notified immediately. However, the adversary is able to use the credentials to corrupt the key in the functionality.

Remark 2: We require that the credentials for different KU-functionalities are distinct. It is nonetheless possible to encrypt and decrypt arbitrary credentials using F KW . Suppose a designer wants to prove a Secure API that uses shared keys for different operations secure. One way or another, she would need to prove that those roles do not interfere. For this case, we suggest providing a functionality that combines the two KU-functionalities, and proving that the implementation of the two operations combined UC-emulates the combined functionality. It is possible to assign different attributes to keys of the same KU-functionality, and thus restrict their use to certain commands, effectively providing different roles for credentials to the same KU-functionality. This can be done by specifying two attributes for the two roles and defining a policy that restricts which operation is permitted for a key of each attribute.

Remark 3: Many commonly used UC-functionalities are not caller-independent, often the access to critical functions is restricted to a network party that is encoded in the session identifier. However, it is possible to construct caller-independent functionalities for a large class of UC-functionalities, if the implementation relies on keys but is otherwise stateless. See Section 5 for details.

Policies

Now that all credentials on different Security APIs in the network are abstracted to a central storage, we can describe the implementation of a global policy. Every credential in F KM has exactly one attribute from a set of attributes A.

Definition 5 (Policy). Given the KU-functionalities F i , i ∈ {1, . . . , l} and corresponding sets of commands C i , the policy is a quaternary relation Π ⊂ {F 1 , . . . , F l , F KW }×∪ i∈{1,...,l} C i ∪{New, Wrap, Unwrap, AttributeChange}×A×A such that if (F, C, a, a ) ∈ Π and -C = New, then F KM allows the creation of a new key for the functionality F with attribute a. -F = F i and C ∈ C i , then F KM will accept sending the command C to F, if the handle used is of type F and has the attribute a. -F = F KW and C = Wrap, then F KM allows the wrapping a key with attribute a using a wrapping key with attribute a. -F = F KW and C = Unwrap, then F KM allows the unwrapping of a wrapping annotated with the attribute a using a wrapping key with attribute a.

if C = AttributeChange, then F KM allows the changing of a key's attribute from a to a .

The existence of the latter command implies that a key can have different attributes set for different users of F KM , corresponding to different Security APIs in the real word. Note that a is only relevant for the AttributeChange command. Therefore, attr in F KM maps a user and a handle (U, h) to an attribute, rather than a key-index i = I(U, h).

The policy relation allows us to state exactly how attributes can be changed and what implications they have. It is sufficiently expressive for many policies employed in practice. In Section 3, we will consider a static key-hierarchy as an example. Note that whether F KM and its KU-functionalities can be UC-realized depends both on the policy and the functionalities.

The Key Management Functionality F KM

A detailed description of F KM is given in Listing 1.1. By convention, the response to a query (Command, sid , . . .) is always of the form (Command • , sid , . . .), or ⊥. One may note that at any time the attacker may send queries on behalf of any corrupted user.

The principle structure of F KM is that of a proxy service to the KU-functionalities. It is possible to create keys (Generate,. . . ), which means that F KM asks the KU-functionality for the credentials and stores them, but outputs only a handle referring to the key. When a command is C ∈ C i is called with a handle and a message, F KM substitutes the handle with the associated credential, and forwards the output to F i , but only if this is in accordance with the policy. The response from F i is forwarded unaltered.

The commands that are important for key-management are handled by F KM itself. It is possible to wrap and unwrap a key. Here, F KM makes use of the keywrapping functionality F KW discussed in Section A (see Listing 1.8 on page 27 for its definition). Note that the user can choose an identifier that is bound to a wrapping in order to identify which key was wrapped. This could, e. g., be a key digest provided by the KU-functionality the key belongs to. If not given explicitly, we assume that F KW only leaks the length of the key that is wrapped, i. e., the leakage function L a (k 1 , k 2 ) returns a bitstring of length |k 2 | drawn from a uniform random distribution for each a, k 1 and k 2 .

When a wrapped key is unwrapped, F KM checks if this key is in its database already. If this is the case, a new handle h for the user U is created and mapped to the same index i that references the credentials and the type of the key. Since it is possible to change a key's attributes using the command (AttributeChange), the pair (U , h ) identifies the key's attribute, instead of the index i.

Key-management is of limited interest without pre-shared keys as it would not allow us to migrate keys from one device to another. Therefore we model a setup phase: Room is a list of users in a secure environment that are allowed to share keys during the set-up phase, which means that the implementation is allowed to use secure channels to transport keys during this phase, but not later. On a physical device this would correspond to pre-installed keys at manufacturing time or installation of keys by an administrator using a trusted machine. Once the setup phase is finished the functionality enters the run phase. During this phase users may create new keys, wrap and unwrap keys, change their attributes and send commands to the key usage functionalities. Note that keys are identified by a pair (user, handle) and all queries are checked against the policy. The adversary A may corrupt handles. The UC framework does not provide a global register for corrupted keys, so to avoid the simulator corrupting handles the adversary did not corrupt unnoticed, the environment can check the corruption status of a handle. Before defining F KM , we will define the relevant parameters describing the network to be modelled.

Definition 6 (Parameters to a Security Token Network). We summarize the parameters of a Security Token Network(cf. 9) as a tuple (Φ, Φ ext , Room, F, Π), where -Φ = {ϕ 1 , . . . , ϕ m } are the dummy users with network identities U 1 , . . . , U m , -Φ ext = {ϕ m+1 , . . . , ϕ m+n } are the external dummy users with identities

E 1 , . . . , E n , -Room ⊂ Φ, -F = {(F 1 , C 1 ), . . . , (F l , C l )}
are key-manageable functionalities with corresponding sets of commands, and F KM ∈ {F 1 , . . . , F l }, and Π is a policy for F Definition 7 (F KM ). With respect to the parameters (Φ, Φ ext , Room, F, Π), F KM is defined in the following listing. In addition, whenever a lookup of I fails, it responds by sending ⊥ to the querier. F KM has one thread per dummy user in Φ.

structure:

I : (u, h) → index #functions mapping user and handle to index type( i ) # maps an index to a functionality credentials(i) #credentials to access functionality attr(u, h) #attribute that policy assigns to a user's handle List of Corruption requests In all phases: sid ) to U and enter phase run phase run: rcv (New,sid ,F ,a) from U ∈ U for some F ∈ {F1, . . . , F l , F KW } . . . #behave as in setup phase rcv (Wrap,sid ,h1,h2,id) from U:

rcv (m1, . . . , m k , U ) from A: if U has been corrupted before proceed like rcv (m1 . . . m k ) from U phase setup: rcv (New,sid ,F ,a) from any U ∈ Room if ((F ,New,a, * )∈ Π) create fresh h,i; update I such that I(U, h) → i snd (Generate,sid ) to F ; rcv (Generate • ,sid ,s) from F save credentials ( i):=s, attr (U, h):=a, type(i):=F snd (Generate • , sid , h) to U else snd ⊥ to U rcv (Share, sid , (U1, h1), (U2, h2)) from U1 ∈ Room if I(U2, h2) does not exist and U2 ∈ Room I(U2, h2):=I(U1, h1) snd (Share • ,sid ) to U1 else snd ⊥ to U1 rcv (FinishSetup) from any U ∈ Room send (FinishSetup • ,
if (F KW , "Wrap",attr(U,h1),attr(U,h2))∈ Π snd (Wrap,sid ,credentials(I(U, h1)), <attr(U,h2),type(I(U, h2)),id>,credentials(I(U, h2))) to F KW rcv (Wrap • , sid , c) from F KW snd (Wrap • , sid , c) to U else snd ⊥ to U rcv (Unwrap,sid ,h1, w, a, type, id) from U: if (F KW , "Unwrap",attr(U,h1),a)∈ Π snd (Unwrap,sid ,credentials(I(U, h1)),<a,type,id>,w) to F KW rcv (Unwrap • , sid , m) from F KW if i exists such that type(i )=type and credentials(i )=m create fresh h ; I(U,h ):=i If (a = attr(U,h1)) and (type(I(U, h1)),"AttributeChange",attr(U,h1),a)∈ Π attr (U,h ):=a else #corrupted create fresh h ,i type(i ):=type; credentials(i ):=m; attr(U,h ):=a; I(U,h ):=i snd (Unwrap • , sid , h ) to U else snd ⊥ to U rcv (AttributeChange, sid , h, a new) from U: if (type(I(U, h)),''AttributeChange'',attr(U,h),a new)∈ Π attr (U,h):=a new else snd ⊥ to U rcv (Command,sid ,h,m) from U, for Command ∈ Ci if (type(I(U,h))=Fi and (type(I(U,h)), Command, attr(U,h), * )∈ Π) snd (Command, sid , credentials(I(U,h)),m) to Fi rcv (Command • , sid , m) from Fi; snd (Command • , sid , m) to U else snd ⊥ to U rcv (Corrupt,sid ,(U,h)) from A snd (Corrupt • , sid , credentials(i)) to A; save corruption request for (U, h) rcv (CorruptionStatus,sid ,h) from U if corruption request for (U, h) was saved snd (CorruptionStatus • ,sid ,Corrupted) to U else snd ⊥ to U ¥ Listing 1.1. A key-management functionality F KM
In standard UC, proving that a network of security tokens UC-realizes F KM in the F 1 , . . . , F l , F KW would not be strong enough for our purposes, because the environment could not access the KU-functionalities directly. A signature functionality, for example, might provide an interface to verify signatures to users that do not have a Security Token. Instead, we define a protocol in which those functionalities interact and a number of external users (Φ ext ) has direct access to the KU-functionalities. Technically, this protocol is modelled as a network, not as a functionality (although the protocol machines are, in fact, functionalities).

Definition 8 (F KM -Network). The network F KM -Net (Φ,Φ ext ,Room,F ,Π) is the network where all φ ∈ Φ are dummy parties to F KM (instantiated for the same parameters), which itself communicates (via subroutine input tapes) with all F ∈ F and F KW . Additionally, every external dummy user φ ext ∈ Φ ext allows the environment to adress each F ∈ F.

Definition 9 (Security Token Network). Given an implementation of keymanagement ST and parameters (Φ, Φ ext , Room, F, Π), we define the Security Token Network STN ST,Φ,Φ ext ,Room,F ,Π as the network where m = |Φ| dummy users φ ∈ {1, . . . , m} are each connected to a Security Token ST i , and each ST i is connected to all F 1 , . . . , F l , to F KW and to F SIMT . Additionally, each external dummy user ϕ ext ∈ Φ ext is connected to each F ∈ F.

Definition 10 (Secure Key-Management). An Security Token ST is secure

(under condition C) with respect to (Φ, Φ ext , Room, F, Π) iff STN ST,Φ,Φ ext ,Room,F ,Π UC-emulates F KM -Net (Φ,Φ ext ,Room,F ,Π) (under condition C).
A protocol π F KM -Net that calls F KM -Net (Φ,Φ ext ,Room,F ,Π) is subroutine respecting, i. e., the sub-parties of F KM -Net (Φ,Φ ext ,Room,F ,Π) , in particular the KU-functionalities, exchange input/output only with parties (the external dummy users Φ ext ) or sub-parties (F KM ) of F KM -Net. This is a neccesary condition for the Universal Composition Theorem. In consequence, for very π and ST secure with respect to (Φ, Φ ext , Room, F, Π), π F KM -Net/STN UC-emulates π F KM -Net .

Realizing key-management for static key-hierarchies

To illustrate our definition and demonstrate its usefulness, we now implement a Security API which allows arbitrary key-usage functionalities and a policy that enforces a hierarchical key-structure. The policy guarantees that corruption of lower-level keys does not impair the security of higher-level keys. We stress that our implementation describes a way to implement a Security API for keymanagement that is independent of the key-usage functions it provides. Extending F KM and the implementation by a new KU-functionality does not require a new proof.

The implementation of a secure token ST is, like F KM , based on the keywrapping functionality F KW . We assume a secure environment for the set-up phase, permitting all users in the set Room to generate keys and share them among each others. This is implemented by the functionality F SIMT , defined in Listing 1.2 below. This secure channel is only used during the set-up phase.

F SIMT is designed after F SIMT from [Can05], with two differences: (i) there is no corruption, because we want to simulate a secure set-up phase, and nothing more; (ii) the adversary is not notified when a message is sent. The implementation ST is inspired by the implementation introduced in [KSW11]. There is an improvement that became apparent during the proof of UC emulation (Theorem 12 below). Namely, when unwrapping with a corrupted key, F KM checks the attribute that is going to be assigned to the (imported) key against the policy, instead of just accepting that a corrupted wrapping-key might just import any wrapping the attacker generated. This prevents, for example, that a corrupted wrapping-key of low security creates a high-security wrapping-key by unwrapping dishonestly produced wrappings. This detail in the definition of F KM enforces a stronger implementation than the one in [KSW11]: ST validates the attribute given with a wrapping, enforcing that it is at least sound according to the policy, instead of blindly trusting the authenticity of the wrapping mechanism. Hence our implementation is more robust.

Definition 11 (ST ). Given parameters (Φ, Φ ext , Room, F, Π), the ST that is connected to the dummy-user ϕ i with identity U i is defined in the following listing. In addition, whenever a lookup to List fails, or a response does not match the pattern in rcv, ST sends ⊥ to the querier. ST is single-threaded. We now show that ST implements the following static key-hierarchy policy. We define this policy as the relation that consists of all 4-tuples (F,Cmd,attr 1 ,attr 2 ) such that the conditions in one of the lines in the following table hold. Note that we omit the "=" sign when we mean equality and "*" denotes that no condition has to hold for the variable.

(Generate • ,sid ,cred) from F save (h,F, a, cred) snd (Generate • , sid , h) to Ui rcv (Share, sid , (Ui, h1), (Uj, h2)) from Ui if h1 is in List and U2 ∈ Room snd (Send,(ST i, ST 2, sid ), ((Uj, h2),type(h1),attr(h1), credentials (h1))) to F SIMT if rcv (Sent,(ST 2, ST i, sid ),⊥) from F SIMT snd ⊥ to Ui else snd (Share • ,sid ) to U1 rcv (Sent, (ST j , ST i, sid ),((U, h), type, a, cred)) from F SIMT if h is not in List yet add (h,
F Cmd attr 1 attr 2 F KW New > 0 * = F KW New 0 * * AttributeChange a a F KW Wrap > 0 attr 1 > attr 2 F KW Unwrap > 0 attr 1 > attr 2 F i C ∈ C i 0 *
(where a ∈ N)

Cortier and Steel have shown that a policy enforcing a static key-hierarchy can give the following guarantee: If an attacker leans a key of a certain security level a (the attribute in our case), he might learn any data of security level strictly smaller than a, but nothing more [CS09]. Transferring their result to our framework remains ongoing work.

We can now state our UC-emulation theorem which is depicted in Figure 1.

Theorem 12. ST is secure with respect to any parameters (Φ, Φ ext , Room, F, Π), where Π describes a static-key hierarchy.

Proof sketch. We prove that an invariant holds for all sequences of messages that the environment sends to the network STN ST,Φ,Φ ext ,Room,F ,Π as ST F1...F l . Assuming that the invariant is preserved for a smaller sequence of messages, we show that it is also preserved after the next message is processed. The heart of the invariant is the consistency of the internal state of F KM and the "global state" of the ST i , e. g., that for all internal indexes i = I(U i , h) in F KM , we have that, on ST i , credentials(i) and credentials(h) are equally distributed, attr(i) = attr(h), and that F KM and all ST i ∈ Room leave the set-up phase at the same time. We further need to preserve other properties, for example that the internal states of the functionalities F 1 . . . F l in both worlds are equally distributed and credentials of wrapping keys stay secret. An intuition why state consistency holds is the following: The credentials and attributes are only written by an (Unwrap) or by a (New) query. (New) is trivial to verify, so we look at (Unwrap). F KW only allows (Unwrap, sid , h, a, c) if c has been produced by a (Wrap, sid , h, a, m) query. By the fact that the internal handles of F KW cannot be guessed and never leave the device, we can guarantee that query came from an ST i . This means especially that the bound attribute a is the saved attribute, so we can guarantee attr(i) = attr(h). Furthermore, by the fact that the credentials constitute the message m, we can assure that the credentials are drawn from the same distribution. Intuitively, if we assume the internal state of a KU-functionality to be equally distributed in both worlds, we can conclude from state consistency that every command for this KU-functionality behaves just the same in both worlds, in particular since the credentials are equally distributed. See Appendix B for the full proof.

The Theorem specifies how to use key-wrapping to implement a key-hierarchy. Due to its generality, it is simple to add new features to a Security API, such as digital signatures, without having to prove anything about the interaction of the new feature with other KU-functionalities. As long as the token's key-management is implemented according to ST , the proof does not need to be redone. In this sense, Theorem 12 allows us to extend a token with arbitrary KU-functionalities -as long as they can be implemented individually, which is the subject of the next section.

We will briefly discuss the runtime of ST in detail. ST maintains a configuration of size O(η • q), where q is the number of keys stored, which is at most as large as the number of New or Unwrap queries received so far. For each query received, the configuration grows at most by the length of one entry in the database, i. e., by O(η), performs O(η) steps of computation (since a credential of length in O(η) might be transmitted) and at most one subroutine-call (i. e.input to another functionality) is made.

Note that the notion of polynomial-boundedness of a protocol does not transfer well from one simulation-based security framework to another. This is polynomial-time execution according to the definition in the IITM framework [Küs06], because the run-time per activation is bounded by a polynomial in the security parameter, the current input size and the size of the current configuration, while the runtime at any point of the execution is bounded by a polynomial in the security parameter, and the length received on the input-channels to the environment (which would be tagged as "enriching" in this framework). In contrast, the definition in the UC framework requires the runtime at any point of the execution to be bounded by a polynomial in n, where n is the sum of the security parameter η, the number bytes input or output to sub-routines , and n N • η (n N is the number of functionalities called, in our case at most l + 2). This means that the number of input bytes per query needs to be a polynomial in η, since at most one sub-routine output is made per query. This can be reached by altering the definition of F KM and ST such that 1 η needs to be appended to every incoming query, but is ignored. In fact, in the GNUC framework, this is the case for every message transmitted [HS11], thus ST runs in polynomial-time according to the definition in this framework.

Realizing key-usage functionalities

To demonstrate the usefulness of Theorem 12, we will equip a security token ST as shown above with the functionalities F 1 = F Nonce and F 2 = F SIG defined below. The resulting security token ST F Nonce ,F SIG is able to encrypt keys and nonces and sign user-supplied data. It is not able to sign keys, as we consider this task part of the key-management. We suppose that the symbolic results in this paper can be transferred to ST F Nonce ,F SIG without much effort, as by Theorem 12, ST F Nonce ,F SIG can realize key-management for {F Nonce ,F SIG } and a static key-hierarchy policy. This allows for an easier analysis in the context of a protocol. Formal methods could be employed: an approach of using abstractions by UC functionalities to prove computational soundness is presented in [CH06]. It seems promising to derive a computational soundness result for the symbolic model presented in [CS09]. The digital signature functionality is designed after the one described in [KT08] and detailed in Listing 1.4. Note that the functionality offers a command VerificationKey ∈ C SIG that outputs the public part of the key. Effectively, this means that when F SIG is used via F KM and a user sends this command to F KM , using a handle that is of type F SIG , the output contains the verification key. The function VerifyPublic then allows to verify the validity of a signature for a given verification key, without knowledge of the credential. In Section 5, we mention that future work could enable us to produce an implementation ÎSIG such that ÎSIG ≤ UC F SIG from the proof presented in [KT08] for a non-key-manageable signature functionality. Since this is out of the scope of this work, we assume such a ÎSIG .

The F Nonce is an unusual functionality, but demonstrates what can be done within the design of F KM . It models the creation of nonces, tests of equality and two kinds of corruption, one allowing him to learn the value of a nonce, and a second one allows him to create a nonce that is equal to every other nonce, even nonces that have not yet been created. F Nonce might be used to model nonce corruption through weak random number generators or investigate on nonce generation via PRNGs, for example.

(Cmd,h,m) (Cmd,k,m) (Cmd,h,m) (Cmd,cred,m) (Cmd,h,m) (Cmd,cred,m) (ST F1...Fl ) (πl) E A ϕ1 . . . ϕm ST F /I 1 I . . . ST F /I m I F2 F • • • F KW (π1) E A ϕ1 . . . ϕm ST 1 . . . ST m F2 F • • • I F KW (π2) E A ϕ1 . . . ϕm ST 1 . . . ST m F2 F • • • Î F KW E A ϕ1 . . . ϕm ST 1 . . . ST m F2 F • • • F F KW ≤ UC ≤ expl.cor UC ≤ UC Fig. 2.
Simplified sketch of the chain of proofs to show that KU-functionalities can be implemented.

Since it is established that ST F Nonce ,F SIG UC-emulates F KM for F Nonce and F SIG , it is possible to obtain a number of properties in spirit of those proven for a symbolic modelling of a static key-hierarchy policy in [CS09], since the token ST F Nonce ,F SIG provides similar cryptographic operations. Here, however, we investigate how to realize KU-functionalities in general:

A proof technique to realize KU-functionalities Although Theorem 12 offers a great deal of flexibility, the question arises whether the functionalities can be realized in this context. Most notably, ST wraps credentials instead of keys, but the environment sees credentials only in case of corruption. So, is it possible to implement credentials with keys, knowing that the KU-functionalities are in some sense protected by ST? We will introduce a proof technique permitting the substitution of calls to a KU-functionality with a distributed implementation that operates using keys instead of credentials. It is quite generic and allows us to conclude under what circumstances an implementation of key-management and cryptographic operations in a device UC-emulate F KM with a given set of KU-functionalities. It is of further interest, because it gives an answer to the question of how to abstract keys in simulation-based security frameworks like UC.

For distributed Security APIs, the implementation of a KU-functionality F cannot rely on any internal state other than the key. Therefore, we can safely assume that a typical implementation consists of a key-generation algorithm KG and an implementation impl Cmd for each command Cmd in the set of supported commands C. When generating a new key, a Security API creates a key k ← KG(1 η ) and stores it as if it were a credential. When processing a request (Cmd, sid , h, m), assuming that h is a handle to k, the response is computed by impl Cmd (k, m). To model a Secure API that makes this computations, we assume it simulates the following implementation of the functionality locally: Definition 13 (Local implementation). For a functionality F with commands C, given KG and {impl Cmd } Cmd∈C , we define I as follows:

rcv(Generate,sid ) from U snd (Generate • , sid , k ← KG(1 η )) to U rcv (Command,sid,k,m) from U , Command ∈ Cj snd (Command • ,sid ,impl Cmd (k, m)) to U

¥

Listing 1.6. A generic implementation of a key-usage function, I

Given an ITM π, we say that π F /I , i. e., π where every subroutine call to F is is substituted by a call to a locally simulated instance of I, is π with a local implementation of F by I.

From its definition we can see that ST F /I can be implemented using only function calls to the algorithms KG and {impl Cmd } Cmd∈C . It is clear that it is typically impossible to directly UC-emulate F by I, since I exposes the key generated by KG to the environment. A slight modification allows us to use credentials instead of keys. Credentials need to be difficult to guess, but since wrappings of credentials will be visible to the environment, we need to assure that the distribution of length of credentials is similar to the distribution of length of keys.

params: KG with domain K,impl Cmd for each Cmd ∈ C structure: In the following, we will prove that if Î implements a KU-functionality F, then we can substitute calls to F by local computations as defined by I. In a way, this is a reversed version of a joint state theorem, because we implement a functionality with an internal state by distributing the computation across the ST i s. The proof will proceed in three steps which are depicted in Figure 2. Despite having a globally readable register for which parties are corrupted, the UC framework has nothing of the sort for corrupted keys. This is the reason why dealing with key-corruption within UC is rather quirky: Usually, the implementation offers a (Corrupt) query that exposes a key and can only be called by the adversary. The functionality, when receiving the same query, adjusts its behaviour, usually giving the simulator more power, e. g. in the case of encryption, it sends real encryptions instead of fake once, accounting for the knowledge the adversary has obtained. To assure that the simulator corrupts the same keys that the adversary corrupts, a (CorruptionStatus) query allows the environment to see whether a keys was corrupted. If it was not for such a query, many functionalities could be emulated easily with a simulator that corrupts every key from the start.

List: K × K, K corrupted ⊂ K rcv(Generate,sid ) from U save (k ← KG(1 η ), cred ← {0, 1} |k| ) in List; snd (Generate • ,sid ,cred ) to U rcv (Cmd,sid,cred,m) from U , Cmd ∈ Cj search (k,cred)∈ List; snd (Cmd • ,sid ,impl Cmd (k, m)) to U rcv (Corrupt,sid ,cred) from A search (k,cred)∈ List; add k to K corrupted ; snd (Corrupt • ,sid ,k) to A rcv (CorruptionStatus,sid ,cred) from U search (k,cred)∈ List if k ∈ K corrupted : snd (CorruptionStatus
Although a real Security API would never answer a (Corrupt) query, this method works well to model corruption in case that the corruption of one key is independent of the corruption of another. This is different in our case, here is an example: Assume, a key k 2 is wrapped using k 1 and transferred from Security API A to Security API B. Security API B now generates a key k 3 and wraps it with k2, and sends the wrapping to the environment. Now, assume the adversary corrupts the handle (A,1) that points to k 1 . In the real world, the attacker learns all the keys k 1 , k 2 , k 3 . Therefore, the corresponding credentials need to be given to the simulator in the ideal world, but this requires registering which key is wrapped with which key, which is impossible to do for this example, since A, B and C do not have a communication channel except for the environment. To overcome the lack of a global key-corruption register, we need to require that the environment corrupts every key explicitly: Before a key is wrapped with a corrupted key, it has to be corrupted itself.

We define this property with respect to the view of the environment E, i. e., the messages (m 0 ,. . . ,m n ) it sends or receives. Let E t = (m 0 , . . . , m t ) denote the t-prefix of E. Since the environment never addresses a party directly, we define from(m) to be the identity of the party that sent the message either herself, or was instructed by the environment to do so. to(m) is defined similarly. Now it is possible to define the response to the ith message in E as response

E t (i) = min j>i {from(m i ) = to(m j ) ∧ from(m j ) = to(m i ) ∧ ∃k < i : response(k) = i} .
This assumes that there is a response to every query, i. e., in case of an error, F KM responds with ⊥ rather than ignoring the query. In order to tell which handles are corrupted, we need to define which handles point to the same key a given moment t. Given E n = (m 0 , . . . , m n ) we define ≡ 0 to be the empty relation and for all 1 ≤ t ≤ n, we define ≡ t as the least symmetric transitive relation such that 1. ≡ t ⊂≡ t-1 ∪{(U, h), (U, h)}, if m t = (Generate • , sid ,h), to(m t ) = U and ∃s < t : m s = (New,sid ,F ,a,h) ∧from(m s ) = U ∧response E t (s) = t (for any F and a)

2. ≡ t ⊂≡ t-1 ∪ {(U 1 , h 1 ),(U 2 , h 2 )}, if m t = (Share • ,sid ), to = U 1 and ∃s < t : m s =(Share,sid ,(U 1 , h 1 ), (U 2 , h 2 )) ∧ from(m s ) = U 1 ∧ response E t (s)= t 3. ≡ t ⊂≡ t-1 ∪{(U 1 , h 1 ), (U 2 , h 2 )}, if m t =(Unwrap • ,sid ), h 2 ), to(m t ) = U 2 and ∃q, r, s : response E t (q) = r, response E t (s) = t, r < s, m q = (Wrap, sid , h 1 , h 2 , id), with from(m q ) = U 1 , m r = (Wrap • , sid , w), with to(m r ) = U 1 and m s = (Unwrap, sid , h 1 , w, a, type, id), from(m s ) =U 1 where (U 2 , h 1 ) ≡ t-1 (U 1 , h 1 ). 4. ≡ t =≡ t-1 , otherwise.
By definition of F KM , during any execution of F KM and F KW with a view E t , I(U, h) = I(U h ) in F KM iff (U, h) ≡ t (U , h ). Using this relation, we can define a corrupt handle predicate: corrupted E t (U, h) iff either some (U * , h * ), ((U * , h * ) ≡ t (U, h)) were corrupted directly, i. e., there are m i , m j ∈ E t such that response (i) = j, from (m i ) = A, and m i = (Corrupt, sid , (U * , h * )) and m j = (Corrupt • , sid , c) for some c, or via wrapping with a corrupted key, formally:

there are e i , m j ∈ E t such that response (i) = j, from (m i ) = U 1 , and m i = (Wrap, sid , h 1 , h 2 ) and m j = (Wrap • , sid , c) for some c, while (U 1 , h 1 ) ≡ t (U * , h * ) and (U 1 , h 2 ) ≡ t (U, h) for some (U * , h * ) that were corrupted directly. We define the event explicit-corruption to be the event that the view E t = (m 0 , . . . m t ) of the environment at the end of the execution fulfils the following predicate:

∀i ≤ t. m i = (Wrap, sid , h 1 , h 2 , id) ∧ from(m i ) = U ∧ corrupted E i (U, h 1 ) ⇒ corrupted E i (U, h 2 )
Intuitively, this predicate holds if the attacker never uses a corrupt key to wrap an uncorrupted key, i. e., the attacker needs to explicitly corrupt a key in order to wrap it with another corrupted key. Now we show how to substitute a KU-functionality used of several instances by ST with a local implementation I running on all ST individually. Theorem 14. Given the implementation of keymanagement ST from Definition 11 with parameters (Φ, Φ ext , Room, F, Π), let ST F /I be ST with a local implementation of F ∈ F by I.

If (i) Î UC-emulates F and (ii) Pr[k = k |k ← KG(1 η )] is negligible for all k in the domain of KG, then, STN ST,Φ,Φ ext ,Room,F ∪ Î,Π UC- emulates STN ST F /I ,Φ,Φ ext ,Room,F ,Π under condition explicit-corruption.
Proof. In the following, we will abreviate STN ST F /I ,Φ,Φ ext ,Room,F ∪ Î,Π by π l , and STN ST,Φ,Φ ext ,Room,F ,Π by π r . Note that, in π l , the external dummy users ϕ ∈ Φ ext have subroutine access to Î like to any other KU-functionality.

from π l to π1 : The network π1 functions as an intermediate step. It is π l , but with ST instead of ST F /calI , each adressing the same machine running I via sub-routine tapes when F should be adressed. When Sim is supposed to address I for the environment, Sim acts as if it were not present, since it cannot be addressed in the real-world, either. Since I does not have any internal state, there is no difference in the output of ST F /I i simulating I, and ST i calling the machine I in the network. Since no other party is able to address I, there is no environment E that can distinguish between the two networks The second step is more involved: from π1 to π2 In this transition, we will abstract keys by credentials. π2 is defined like π1 , but ST accesses Î instead of I, just like the external dummy users.On that account, we define Sim as follows: It runs D with the following exception. When Sim is instructed to send (Corrupt,sid ,h) to some ST i , it first requests the corresponding credential, i. e., sends (Corrupt,sid ,h) to ST i . It obtains cred from ST i . Then, Sim sends (Corrupt,sid ,cred ) to Î, to obtain the response (Corrupt • , sid , k) and forwards it to E. Sim adds (cred , k) to a list of corrupted credentials and corresponding keys. When E instructs Sim to send a (CorruptionStatus) command to Î, it ignores this message, as A does not answer this response in the real world. When F KW sends the query (Wrap,sid ,ptr ,k,a,cred ) to Sim, Sim substitutes cred by a k that was recorded as (cred , k) while processing a corruption request. It sends (Wrap,sid ,ptr ,k,a, k) to the environment and forwards the response back to F KW .

In order to show that for all E, EXEC E,D,π 1 cannot be distinguished from EXEC E,Sim,π 2 , we will show that throughout the execution, π2 and Sim provide a perfect simulation of π1 and D, as long as the mapping from credentials to keys in Î is a bijection. Assuming that this is the case, we note that the only output that depends on some credentials(h * ) and is visible to the environment is the response to (a) a (Wrap,sid ,h 1 ,h * ,id ) query, (b) a (Command,sid ,h * ,m) query, and (c) a corruption request (Corrupt,sid ,h * ) by the adversary. In case (a) we know that h 1 is a handle to a wrapping key, as otherwise ST would not respond in either execution. The output is a wrapping that, by definition of F KW , contains a random string of the length as credentials(h * ), in case credentials(h 1 ) are in K uncorrupted in F KW . Both credential and key are of the same length (by definition of Î), so the output is equally distributed. It is not possible to exploit that credentials(h * ) is now stored in Encryptions(k) in F KW , since the (Unwrap) query that F KW provided can not be accessed directly, unless credentials(h 1 ) was corrupted. (Recall that, by the definition of F KM , F KW ∈ {F 1 , . . . , F l }.) So, if it is called via (Unwrap), no output is produced, the credentials are stored instead.

In case that credentials(h 1 ) is in K corrupted in F KW , we know that the environment must have asked some U to corrupt a handle that points to this credential, as the credential is needed to corrupt a key in F KW , and the credentials to F KW are difficult to guess. Therefore, since we regard only executions that fulfil the conditions of explicit-corruption, some (U , h ) ≡ (U, h * ) must have been corrupted explicitly. Hence, Sim has an entry (cred , k) such that k is the key matching the credential for h * . Sim forwards (Wrap,sid ,ptr ,k,a,k) for the correct k to the environment, just a D does in π1 . A correct simulation in case (b) is assured by the fact that Î substitutes the credential with the corresponding key before executing impl Command , assuming that the List maintained in Î describes a bijection between credentials and keys. Therefore, in both executions, the output is impl Command (k, m), where k is the key that was drawn using KG and bound to the credential. Case (c) works similarly: Assuming the bijection, by definition of Sim, the environment will receive the key that was created along with the credential. By the assumption that Pr[k = k |k ← KG(1 η )] is negligible for all k, we know that the probability that every k and cred generated in Î is distinct, because the length of this list is bound by the running time of the environment, which is polynomial in η. Thus, the mapping from credentials to keys constitutes a bijection. We note further that the external dummy users in Φ ext can adress the same parties as before, but now Î stores, in addition to the credentials and keys the dummy user generate, the credentials and keys ST generates. Again by the assumption that Pr[k = k |k ← KG(1 η )], we see the probability of an interference of those two groups of parties in Î are negligible. This concludes the proof that EXEC E,D,π 1 can only be distinguished from EXEC E,Sim,π 2 with negligible probability. from π2 to ST F1...F l This follows from the composition theorem provided by the UC framework, and the assumption that Î UC-emulates F. (Note that I and F are subroutine respecting, since they do not adress any sub-parties.

To conclude, we summarize in Corollary 15 which assumptions have to be met by an implementation of ST , F KW and the KU-functionalities in order to form a fully functional Security API that UC-emulates F KM .

Corollary 15. A local implementation ST F1/I1,...,F l /I l ,F KW /π KW of the Security Token described in Definition 11, is secure under condition explicit-corruption ∪ corrupt-before-wrap, with respect to any parameters (Φ, Φ ext , Room, F 1 , . . . , F l , Π), if:

-Π describes a static-key hierarchy, for i ∈ F 1 , . . . , F l , Ĩi UC-emulates F i , and

Pr[k = k |k ← KG(1 η )] is
negligible for all k in the domain of KG, the key-generation used in I i , during the set-up phase, there is a secure channel to realize the secure instantaneous message transfer functionality F SIMT , -KW is a symmetric encryption scheme secure with respect to Definition 18 .

Proof. Because of lack of space we only sketch this proof which is basically a consequence of Theorems 12, 14 and Theorem 16. Let the network π l consist of the functionalities F key-wrapping functionality F KW and U i ∈ U, each connected to a ST F1/I1,...,F l /I l i with U i and Room as parameters. Then, from the transitivity of UC-emulation, Theorem 12 and by inductive application of Theorem 14, it follows that the network π l UC-emulates {F KM ,F KW ,F 1 . . . F l }. Carefully verifying that, by definition of ST and corrupt-before-wrap, the composition theorem can be applied, we substitute F KW with πKW . Finally, the proof that πKW can be locally implemented by π KW according to Definition 1.6 is exactly the proof to Theorem 14, except that it is not necessary anymore to deal with case (a) in the second step ( π1 to π2 ).

Conclusions

We have presented a provably secure framework for key management in the UC model. It would be interesting to extend F KM allow policies to have side-effects. For example, the attribute of a wrapping key or the pay-load key might be altered when wrapping, so a high-security wrapping key could only be used so many times. A number of policies could be implemented to see what security properties they induced and who much they restrict the use of a Security API. In further work, we are currently also developing a technique for transforming functionalities that use keys but are not key-manageable into key-manageable functionalities with implementations in the style of Listing 1.7. This way, existing proofs could be used to develop a secure implementation of cryptographic primitives in a plug-and-play manner. Investigating the restrictions of this approach could teach us more about the modelling of keys in simulation-based security.

In Appendix C we show that a wrapping scheme as described in [KSW11] can be used to realize this functionality, but only when the environment does not corrupt keys which have been used to encrypt before. We avoid the commitment problem by only regarding executions where a key is never corrupted after it has been used to encrypt. Given the view E t = (m 0 , . . . , m t ) of the environment we define the event corrupt-before-wrap to be the following predicate :

∀i ≤ t. corrupted E t (U, h) ∧ m i = (Wrap, sid , h, h ) ∧ from(m i ) = U ⇒ corrupted E i (U, h)
We state the Theorem here. Both the proof and Definitions 17 and 18 can be found in Appendix C.

Theorem 16. If a symmetric encryption scheme KW = (KG, Wrap, UnWrap) is secure with respect to Definition 18, then for the protocol version πKW (see Definition 17), πKW UC-emulates F KW under the condition corrupt-before-wrap.

The interesting part of key-management is dynamic corruption: We would like to know what guarantees we can give in case an attacker learns one or more keys during the protocol run. As opposed to static corruption, an attacker can corrupt a key after it has been used. What does this mean in case of encryption? For one, it means that the attacker is not able to distinguish ideally encrypted ciphertexts from actual encryptions of messages, hence, that he does not learn anything about past encryptions after corruption of a key. This idea bears resemblance to the notion of (perfect) forward secrecy, [Tse07].

However, this property is not needed, in fact, implementations thereof are impractical in the domain of Security APIs. The question of why we are interested in dynamic corruption arises. A small example, the encryption functionality F toy , illustrates that the modelling of dynamic corruption is of interest, although forward-secrecy is not a security goal. It furthermore shows where encryption in connection with dynamic corruption produces a situation where existing frameworks for simulation-based security prove to be useless -the so-called commitment problem. F toy has a master and a slave key. The corruption of the master key leads to the corruption of the slave key, but not vice versa. In reality, the slave key might have been derived from the master key in some deterministic way, maybe using a hash function.

¥

Listing 1.9. A toy example of an encryption system F toy Imagine an implementation of F toy , say π. Let E send a number of (Enc, k, m i ) queries, and receive something that looks like encryptions. The simulator Sim does, by definition of F toy , not learn the messages m i . The environment sees a number of encryptions of the null-string. Now, upon corruption of k, the simulator has to produce a key that allows to open the emitted encryptions to the messages m i . If we assume some bound b(n) on the length of the key, i. e., the cardinality of the key space is at most 2 b(n) . Still, the environment can produce random messages of a total length greater than b(n). Therefore, there is no key that would open the encryptions independent of the value of m i to the correct values upon corruption. [Hof08] shows the impossibility of a realization of selective decommitment. This means that encryption needs to be non-committing to work in the setting of dynamic corruption, so it is possible to circumvent this problem, but at the cost of of having to updating the key regularly [CHK04], having a key-size larger than the message space [CDNO97] or require interaction with the receiver to communicate[DN00]. All of this is impractical for our purposes, as encryption in Security APIs is typically needed to not be efficient for a possibly large number of messages encrypted with the same key, without on-line communication to the recipient. This is the scenario we have to deal with. We would like to use traditional, efficient encryption systems.

While practical considerations make realizing F toy more difficult in this regard, they are forgiving in another: In F toy , we do not mind if an intruder learns about the content of already produced ciphertexts when corrupts the slave key. But we do want to assure that past and future ciphertexts generated using the master key stay secret -in contrast to the idea of forward secret encryption. Unfortunately, it seems that we are not able to express non-forward secure encryption in existing simulation-based security frameworks. In our opinion, this is a problem of expressiveness: we cannot formulate our weaker notion of dynamic key-corruption in, e. g., UC.

Existing work circumvents the problem in two ways. The first option is to use a game-based definition instead simulation-based security, see for example [KSW11]. There, the attacker tries to distinguish real encryptions from fake encryption and is constraint by a number of rules, to avoid what are called "trivial attacks". In this particular case, there are five kinds of request the adversary is not allowed to make. It is very difficult to say whether any of those constraints forbids more than just "trivial attacks". The attacker has to choose which key to attack before the experiment. It is not clear whether this is a restriction. Since Security APIs are supposed to be used in other protocols, composability is a big issue. It is not clear how Security APIs behave when used in several protocols at once, so a proof by reduction to the game-based definition is necessary. The second option is conditional simulatability, i. e., an implementation is proven to UC-realize F toy or F KW for a restricted set of environments E, most often for all E that do not corrupt keys that have been used to encrypt before corruption. Theorem 16 shows a similar property. Although this approach benefits from some advantages of simulation-based security, it turns out to be insufficient for Security APIs. The restriction on the environment may hold for most protocols, still, when a party that uses a Security API becomes corrupted, it is impossible to guarantee that it corrupts the key before it uses it to encrypt. We aim at using Security APIs as building blocks in arbitrary protocols to allow for secure execution of the protocol despite corrupted parties, so conditional simulatability does not solve the problem, either.

We conclude that a new framework is needed that allows to use non-forward secure encryption in a composable setting with dynamic corruption by allowing to express that encrypted messages must remain secure until a key is corrupted, but not necessarily longer. A framework that could conserve the nice properties of simulation-based security(intuitiveness, composability) would be of great benefit. Furthermore, we suspect that this kind of "weak" dynamic corruption might turn out to be equal to static corruption.

In the full version of the paper [KKS12] we prove that a deterministic authenticated symmetric key-wrapping scheme KW = (KG, Wrap, UnWrap), as defined by Kremer et al. [KSW11] can be transformed into a protocol version πKW that UC-emulates F KW under the condition corrupt-before-wrap.

B The Full Proof of Theorem 12

Theorem 12. ST is secure with respect to any parameters (Φ, Φ ext , Room, F, Π), where Π describes a static-key hierarchy.

Proof. In the following, we will abbreviate F KM -Net (Φ,Φ ext ,Room,F ,Π) by F KM -Net and STN ST,Φ,Φ ext ,Room,F ,Π by STN. We have to show that there is a simulator Sim, such that for all environments E, Pr[EXEC STN,D,E = 1] -Pr[EXEC F KM -Net,Sim,E = 1] is negligible. Since the environment can access the Secure Tokens through the dummy users Φ, it does not need to corrupt them. The Security APIs themselves are assumed to be tamper-resistant. Technically, if D corrupts a dummy user ϕ i (which is stateless), E can instruct it to send messages to other parties than ST i , but other ST j , j = i will respond with ⊥. Therefore, when Sim is instructed by the environment to send something on behalf of the corrupted user U i in the ideal world, it will return ⊥ if it is addressed to ST j for j = i. If the message is addressed to ST i , Sim will append the string by(U i ) to the message. By definition of F KM , this is will be treated as if the message were coming from the dummy party for U i , therefore we conclude that, without loss of generality, we can assume that E never corrupts any U ∈ U. Aside from the behaviour we specified, Sim behaves like D, e. g., it might forward messages to the KU-functionalities.

Before proving the claim formally, we introduce some notation: When we talk about internal variables of functionalities or protocols, we subscript the variable with the entity it belongs to whenever we need to disambiguate them. For example, credentials(i) F KM denotes the credentials for index i in the key-management functionality, and not the credentials inside a secure token.

Invariant As soon as to(m k ) has finished processing m k , the following holds for all sequences of messages (m 0 ,. . . ,m k ) the environment sends or receives via the dummy users or the adversary:

state consistency: For all users U j and handles h: If i = I(U j , h) is defined on F KM , then (a) credentials(i) F KM and credentials(h) ST j are equally distributed and (b) attr(U j , h) F KM = attr(h) ST j . If I(U j , h) is undefined, then no entry with h as first element exists in List KM F . A corruption request for (U j , h) is recorded on ST j iff and only iff a corruption request for (U j , h) is recorded on F KM .

phase consistency: F KM and all ST i ∈ Room are in the same phase.

secrecy of uncorrupted wrapping credentials: If, attr(U j , h) F KM = 0, c = credentials(I(U j , h)) and there is [(ptr , k) ∈ List s.t. k ∈ K uncorrupted ] F KW , then, the output of ST j and F KM is independent of c. output consistency: The distribution of all messages received by the environment is the same in the real execution and the ideal execution consistency of functionalities: F 1 . . . F l and F KW have equally distributed states in both the real execution and the ideal execution Initial step: For the empty sequence, i. e., prior to all messages sent by the environment, the state of all ST i is empty, as well as the state of F KM , and they are in the init phase. Furthermore, no message is output to the environment, and the functionalities did not receive any messages yet, therefore we conclude that the invariant is preserved.

Induction step Now assume that the invariant holds after messages (m 0 , . . . , m k-1 ).

The environment sends a message m k . Case distinction:

Case: to(m k ) ∈ {F 1 • • • F l }: (Only A
• • • F l } and a = 0)
The same sequence of commands is sent to F in both executions. By consistency of functionalities in the previous proof step, and the fact that F runs the same code in both worlds, we can assure consistency of functionalities. The credentials output by F are saved in credentials(i) F KM and credentials(h) ST i , respectively. By state consistency in the previous step, and since F receives the same commands in both instances, the distribution of the credentials is equal. Thus, state consistency holds. Attributes are stored correctly. Output and phase consistency, as well as secrecy of uncorrupted wrapping credentials, hold trivially. -m=(Share,sid ,(U i , h 1 ),(U j , h 2 )) and U i =recipient(m) For this case we have to look into the details of the scheduling of messages in the UC-model. When a message is sent on a direct channel, the next program called is the code that processes the message. This is why the message sent via F SIMT to ST j is processed before the environment can send any further messages. By inspection of the messages sent and the fact that F SIMT guarantees authenticity, we see that credentials, attributes and types are correctly transferred between ST i and ST j , thus state consistency holds.

If I(U j , h 2 ) KM F is undefined or there is no List entry for h in ST j , {0, 1} is output, otherwise (Share,sid ). By state consistency, those two events coincide, i. e., in both networks the same is output, thus output consistency holds. The phase is not changed, so the invariant holds in this case.

Case: to(m k ) = ST i and phase "run" Once in phase "run", no phase change takes place anymore in every F KM and ST i , therefore phase consistency holds for any m.

-m=(New,sid ,F,h,a) The handling of this message is defined just as in the set-up phase, and since the invariant is independent of the phase we are in (except for phase consistency, of course, but we just dealt with this) , the argument is literally the same as for the same message in the set-up phase. -m=(AttributeChange,sid ,h,a new) The condition in ST i implements the policy relation, therefore the invariant transfers easily.

-m=(Wrap,sid ,h 1 , h 2 ,id) State consistency holds trivially by the fact that neither credentials, nor attributes are touched. Therefore, the wrapping functionality F KW receives the same messages in both worlds and is, by consistency of functionalities in the previous proof step, in the same state in both worlds at the end of its processing of the message. Thus consistency of functionalities holds, and by the fact that the response is forwarded in the same manner, output consistency holds as well. Since F KW only outputs the message to be wrapped iff the wrapping keys is corrupted, we can assure secrecy of uncorrupted wrapping credentials. If the handles h 1 or h 2 are not defined, by state consistency, both F KM and ST i output ⊥. -m=(Unwrap,sid ,h,c, a, F, id)

• I(U j , h) F KM not defined, or policy(F KW ,Unwrap, [attr(I(U, h))] F KM , a)

= false Due to state consistency, in both worlds ⊥ is output and nothing else, thus the invariant is preserved. • F KW returns ⊥ to the query (Unwrap,sid , credentials(I(U, h), <a , type, id>,w). by state consistency, the query equals the query (Unwrap,sid , credentials(h), <a,type,id>,w) emitted by ST i , hence, by consistency of functionalities, ST i receives ⊥, too. Therefore, both respond with ⊥. • otherwise: In F KM a new handle is created, and I(U, h) updated to either point to a newly generated key-index, or to one already in place with the same credentials and attributes. In both cases, ST i creates a new handle and stores it along credential, type and attribute in the list. Hence, state consistency holds. Secrecy of uncorrupted wrapping credentials and output consistency follow from the fact that no output is produced except on the secret channel to F KW . Consistency of functionalities follows from the fact that the same unwrap command is sent to F KW in both cases, and that the credentials are equal by state consistency from the previous proof step.

-m=(Cmd,sid ,h,m) No internal state is changed, the message is directly forwarded, so phase consistency and state consistency hold. Because F KW ∈ {F 1 , . . . , F l }, the output is independent of each wrapping credential, so secrecy of uncorrupted wrapping credentials is preserved. State consistency guarantees that the same message to F is computed. Since consistency of functionalities in the previous proof step can be assumed, and key-manageable functionalities are caller-independent (see Definition 4) , we conclude consistency of functionalities for this step. Output consistency follows, because both ST j and F KM only forward the output of F. -m=(Corrupt,sid ,(U j , h)) By state consistency, the response is distributed equally in real and ideal execution, hence output consistency holds, and because the output is either ⊥ or depends only on the value of a corrupted credential, secrecy of corrupted credentials is guaranteed as well. Neither changes its internal state, except for the register of corruption request: the corruption request for (U j , h) is recorded on ST j as well as on F KM if I(U j , h) and (h, credentials(h)) are defined, which coincides by state consistency of the previous step. Therefore, state consistency holds for the next step.

The message is addressed to the adversary only, so we have consistency of functionalities. -m=(CorruptionStatus,sid ,(U,h)) By state consistency, the response is the same in the real and the ideal execution. No internal state is changed, therefore, the invariant holds for this step. m is none of the above F KM and ST i output ⊥.

C F KW Can Be Implemented Using Deterministic Authenticated Encryption with Key-Dependant Security

In the following we describe a Key-wrapping functionality and show that it can be implemented using a deterministic authenticated encryption scheme as defined in We repeat the definition of from [KSW11] here. It is based on the notion of deterministic, authenticated encryption from [RS06], but it additionally supports key-dependant messages. We changed the definition, so it allows to wrap the same key with the same wrapping key but under different attributes, just like in the DAE definition from [RS06].

Definition 18 (Multi-user setting for key wrapping). We define experiments Exp wrap,real A,KW (η) and Exp wrap,fake A,KW (η). In both experiments the adversary can access a number of keys k 1 , k 2 , . . . , k n . . . (which he can ask to be created via a query NEW). In his other queries, the adversary refers to these keys via symbols K 1 , K 2 , . . . , K n (where the implicit mapping should be obvious). By abusing notation we often use K i as a placeholder for k i so, for example, Wrap a Ki (K j ) means Wrap a ki (k j ). We now explain the queries that the adversary is allowed to make, and how they are answered in the two experiments.

-NEW(K i ): a new key k i is generated via k i ← KG(η) -ENC(K i , a, m) where m ∈ K ∪ {K i | i ∈ N} and h ∈ H. The experiment returns Wrap a ki (m).
-TENC(K i , a, m) where m ∈ K ∪ {K i | i ∈ N} and a ∈ H. The real experiment returns Wrap a ki (m), whereas the fake experiment returns

$ |Wrap a k i (m)|
-DEC(K i , a, c): the real experiment returns UnWrap a ki (c), the fake experiment returns ⊥.

-CORR(K i ): the experiment returns k i Correctness of the wrapping scheme requires that for any k 1 , k 2 ∈ K and any a ∈ H, if c ← Wrap a k1 (k 2 ) then Unwrap a k1 (c) = k 1 . Consider the directed graph whose nodes are the symbolic keys K i and in which there is an edge from K i to K j if the adversary issues a query ENC(K i , a, K j ). We say that a key K i is corrupt if either the adversary corrupted the key from the start, or if the key is reachable in the above graph from a corrupt key. If a handle, respectively pointer, points to a corrupted key, we call the pointer corrupted as well.

We make the following assumptions on the behaviour of the adversary.

-For all i the query NEW(K i ) is issued at most once.

-All the queries issued by the adversary contain keys that have already been generated by the experiment. -The adversary never makes a test query TENC(K i , a, K j ) if K i is corrupted at the end of the experiment. -If A issues test query TENC(K i , a, m) then A does not issue TENC(K j , a , m ) or ENC(K j , a , m ) with (K i , m) = (K j , m ) -The adversary never queries DEC(K i , a, c) if c was the result of a query TENC(K i , a, m) or of a query ENC(K i , a, m) or K i is corrupted.

At the end of the execution the adversary has to output a bit b which is also the result of the experiment. The advantage of adversary A in breaking the key-wrapping scheme KW is defined by: Adv

¥

We now generate an adversary B against Definition 18. Internally, it simulates E, acting for the dummy-adversary, respectively the adversary-simulator, as well as for πKW , respectively F KW .

-If E sends (Generate, sid ) to F KW , B echoes the same message to E, pretending to be Sim. It waits for the environment's response of form (Generate,sid ,k ) and ignores it. As we are not yet sure whether this key will become corrupted, we do not emit a NEW query yet. Instead, B draws a pointer ptr ← P and saves it in the list of uninitialized pointers P new . B sends (Generate • ,sid ,ptr ) to E. If any of the following commands takes a key-pointer ptr , output (⊥) in case ptr was not generated in this step.

-If E sends (CorruptionStatus,sid ,ptr ) to F KW for a pointer for which it sent a (Corrupt,sid ,ptr ) query before, the output is (CorruptionStatus • , sid ,Corrupted), otherwise, the output is ⊥.

-If E sends (Corrupt,sid ,ptr ) to F KW for an uninitialized pointer ptr , B emits a query NEW(K ptr , 1). Save the response in k ptr . Record ptr as initialized and corrupted. Record the corruption query for this pointer, to answer later (CorruptionStatus) queries correctly. If any of the following commands is called for a key-pointer ptr that is uninitialized, then emit a query NEW(K ptr , 0) and record ptr as initialized and uncorrupted before further processing it.

-If E sends (Wrap,sid ,ptr ,a,m) to F KW for an uncorrupted pointer ptr , B checks if the query TENC (K ptr ,a, m) was emitted before. If this is true, return the response r to this query saved previously to E, in form of the message (Wrap • ,r). If not, the query is emitted, and the response r sent to E in the same form, whilst being saved as a response to the query TENC (K ptr ,a, m). If ptr is corrupted, compute c := Wrap a k (m) for the k associated to ptr . Return (Wrap • , r) to E, where r is the response again. In case m ∈ P, if m is uninitialized, B emits a query NEW(K m , 1), saves the response in k m and records m as initialized and corrupted.

-If E sends (Unwrap,sid ,ptr ,a,c) to F KW for a ptr that is marked uncorrupted, then B responds by sending (Unwrap • , sid , m) for a message m previously recorded in a query TENC (ptr ,a,m) with response c. If no such query exists, call DEC (K ptr ,a,c), and use the response in place of m. In case ptr is corrupted, send (Unwrap • , sid , Unwrap a kptr (c)) to E.

First we show that the adversary B is valid, in the sense that it does not violate any of the five assumptions on his behaviour from Definition 18, then we show that we provide E with suitable views for the case of the fake, as well as the real game. First, the probability that (⊥, Collision) is output is negligible. If this is never output, we can guarantee that all NEW(K i ) queries have distinct i. Second, before issuing a query, it is checked if the key-pointer has previously been initialized using a NEW query. Third, TENC(K ptr , a, m) is only queried if K ptr is uncorrupted. Fourth, ENC is never queried, and B remembers the response to a previous TENC query, so it does not issue it twice. Fifth, assume ptr to be uncorrupted. Then, a ciphertext is only part of in a DEC query, if it did not result from a TENC query to the same functionality before. If ptr is corrupted, no DEC query is sent. Note that we never emit a ENC-query. Since, by the fourth condition, it cannot be used on a key that is later used for a test query, it does not provide for more than an oracle Wrap • k (•) for a randomly drawn k ← KG(1 η ) We now show that, for the real experiment, the view of E is the same as in the real execution. (Generate,sid ) generates a random handle ptr ∈ P and no further output. A key k ptr is drawn using KG as soon as ptr is used in another query for the first time. In the real experiment, (Wrap,sid ,ptr ,a,m) outputs Wrap a kptr (m), performing the same substitution of ptr by k ptr that the experiment performs by "abuse of notation". Similarly, (Unwrap, sid , ptr , a, c) outputs Unwrap a kptr (c), except in case ptr points to an uncorrupted key k and c resulted from a previous query TENC(K ptr , a, m). B responds with the message m that was queried. In this case, by the correctness property we have that m = Unwrap a k (c). If (Corrupt,sid ,ptr ) is called, E receives the key k ptr that will be used for all further wrappings and unwrappings for the pointer ptr . If (CorruptionStatus,sid ,ptr ) is called, B outputs, independent of the experiment, and like both F KW and πKW , whether the pointer is initialized and a corruption query for this pointer was emitted before. Therefore, E receives the same output that πKW is defined to produce. Now we show that, in the fake experiment, the view of E is the same as in the ideal execution. (Generate,sid ) behaves just as before and outputs a randomly drawn pointer. With the same argument as before, (CorruptionStatus) is simulated correctly. (Wrap,sid ,ptr ,a,m) outputs W rap a kptr (L a (k ptr , m)) (m might be a key or a message) if ptr is uncorrupted, otherwise B computes W rap a kptr (m) without emitting a query, providing the same outputs as F KW for corrupted, as well as uncorrupted keys. Again, pointers are substituted by keys in this step. (Unwrap, sid , ptr , a, c) is a more complicated case: If k ptr is an uncorrupted key and r was the result of a previous (Wrap,ptr ,a,m) query, just as F KW , the simulation outputs m. If c is uncorrupted, but such a query has not been made before, DEC(K ptr , a, c) outputs ⊥, and (Unwrap • ,sid ,⊥) is output, exactly as F KW is specified to do. If c is corrupted, the simulation, as well as F KW compute (Unwrap • , sid , Unwrap a kptr (c)). Since we have established that B is a valid adversary and, as argued before, E is provided with correct views, we have that Pr

F≈Fig. 1 .

 1 Fig. 1. Distributed security tokens in the network (left-hand side) and idealized functionality F KM in the same network (right-hand side), simplified.

  sid = (S, R, sid ) rcv (Send,sid ,m) from S snd (Sent,sid ,m) to R and halt forever ¥ Listing 1.2. A Secure Instantenous Message Transmission Funct. F SIMT

  phase init: #receive algorithms enc, dec and kmaster, k slave from A phase run: rcv (Enc, key∈ {master, slave}, m) from U: if corrupt(key), snd (Encryption,c=enc(kkey,m)) to U else snd (Encryption,c=enc(kkey,0 |m| )) to U save (m,c) rcv (Dec, key∈ {master, slave}, c) from U: if corrupt(key), snd (Decryption,dec(kkey,c)) to U else if (m,c) saved snd (Decryption,m) to U rcv (Corrupt, key∈ {master) if key=master, set corrupt(master) and corrupt(slave) else set corrupt(slave ) [...]

  wrap KW,A (η) = Pr b ← Exp wrap,real KW,A (η) : b = 1 -Pr b ← Exp wrap,fake KW,A (η) : b = 1 and KW is secure if the advantage of any probabilistic polynomial time algorithm is negligible. Theorem 16. If a symmetric encryption scheme KW = (KG, Wrap, UnWrap) is secure with respect to Definition 18, then for the protocol version πKW (see Definition 17), πKW UC-emulates F KW under the condition corrupt-before-wrap.Proof. Assume for contradiction an environment E such that Pr[EXEC E,D,π KW = 1| corrupt-before-wrap] -Pr[IDEAL E,Sim,F KW = 1| corrupt-before-wrap] is nonnegligible for all simulators. We fix the following simulator:

  phase init: snd (Algorithms, sid, Wrap, Unwrap) to FKW and enter phase run phase run:rcv (Generate,sid ) from F KW snd (Generate,sid ,k ← KG(1 η )) to F KW rcv (Wrap,sid ,ptr ,k,a,m) from F KW snd (Wrap,sid ,Wrap a k (m)) to F KW otherwise: act like D

  [b ← Exp wrap,real KW,B (η) : b = 1] equals Pr[EXEC E,D,π KW = 1| corrupt-before-wrap], as well as Pr[b ← Exp wrap,fake KW,B (η) : b = 1] equals Pr[IDEAL E,Sim,F KW = 1| corrupt-before-wrap]. Thus, we can conclude that Adv wrap KW,A (η) is non-negligible, contradicting the assumption.

  type,a,cred) to List snd (Send,(Ui, Uj, sid ),OK) else snd (Send,(Ui, Uj, sid ),⊥) to F SIMT rcv (FinishSetup) from any U for any U ∈ Room snd (Send,(Ui, U, sid ), FinishSetup) to F SIMT rcv (Sent,(U, Ui, sid ), FinishSetup • ) to F SIMT snd (FinishSetup • ,sid ) to U enter phase run rcv (Sent, (U, Ui, sid ),FinishSetup) from F SIMT snd (Send,(Ui, U, sid ), FinishSetup • ) to F SIMT enter phase run phase run: rcv(New,sid, F, a) from Ui:

	. . .	#behave as in setup phase

rcv (AttributeChange,sid ,h,a new) from Ui: if attr (h)=a new: snd (AttributeChange,sid ) to Ui else snd ⊥ to Ui rcv (Wrap,sid,h1, h2,id) from Ui: if attr (h1)=0 or attr(h1)≤attr(h2): snd ⊥ else # attrh(h1)≥1 and attr(h1)>attr(h2) snd (Wrap, sid ,sid(h1),credentials(h1), <attr(h2),type(h2),id>,credentials(h2)) to F KW rcv (Wrap • ,wrap) from F KW ; snd (Wrap • ,sid ,(wrap,<attr(h2),type(h2),id>)) to Ui rcv (Unwrap,sid,h,c, a, F, id )) from Ui: if attr (h) ≥ 1 and attr(h) > a snd (Unwrap,sid ,credentials(h),<a,F,id>,c) to F KW ; rcv (Unwrap,sid ,k) from F KW generate fresh h '; save (h', F, a, k) rcv (Command,sid,h,m) from Ui, Command ∈ Cj if attr (h) =0 or h does not exist: snd ⊥ to Ui else # attr(h)=0 snd (Command, sid , credentials(h),m) to Fj rcv (Command • , sid , m) from Fj; snd (Command • , sid , m) to Ui rcv (Corrupt,sid ,(U,h)) from A if U=Ui snd (Corrupt • , sid , credentials(h)) to A; save corruption request for h rcv (CorruptionStatus,sid ,h) from Ui if corruption request for h was saved snd (CorruptionStatus • ,sid ,Corrupted) to U ¥ Listing 1.3. A security token ST i using F KW and F SIMT

  L, M, Y #Leakage function domain of plaintexts,signatures structure: K #set of generated keys K corrupted ⊂ K, K uncorrupted := K \ K corrupted to K corrupted and save corruption request for ptr rcv (CorruptionStatus,sid ,ptr ) from Ui if corruption request for ptr was saved snd (CorruptionStatus • ,sid ,Corrupted) to U else snd ⊥ to U

	add k ¥
	Listing 1.4. A signature functionality F SIG
	Signatures: K → 2 M×Y
	List : P × K
	Algorithms Sig, Ver
	phase init:
	rcv (Algorithms, sid , sig, ver) from A
	Sig:=sig; Ver:=ver; enter phase run
	phase run:
	or b ∈ {0, 1}
	b ← ⊥
	snd (Verify • ,sid ,b) to P
	rcv(VerifyPublic,sid ,vk,m,σ)
	search (ptr , k = (sk , vk )) ∈List
	if such ptr does not exist, or k ∈ K corrupted
	b ←Ver(vk , m, σ)
	else
	b ←Ver(vk , m, σ)
	if b=1 and ∃σ : (m, σ ) ∈Signatures(vk)
	or b ∈ {0, 1}
	b ← ⊥
	snd (VerifyPublic • ,sid ,b) to P
	rcv(Corrupt,sid ,ptr ) from A
	if (ptr , k) ∈List

params: rcv (Generate, sid ) from P snd (Generate, sid ) to A rcv (KeyGenKey, sid , k := (sk , vk )) from A ptr ← {0, 1} |k| add (ptr , k) to List snd (Generate • , sid , ptr ) to P rcv (VerificationKey,sid ,ptr) search (ptr , (sk , vk )) ∈List snd (VerificationKey • ,sid ,vk) to P rcv (Sign,sid , ptr ∈ P, m ∈ M) from P search (ptr , (sk , vk )) ∈List σ ← Sig(sk , m) if Ver(vk , m, σ) save (m, σ) in Signatures(vk) else σ ← ⊥ snd (Sign • ,sid ,σ) to P rcv(Verify, sid , ptr ∈ P, m, σ) from P search (ptr , k = (sk , vk )) ∈List b ←Ver(vk , m, σ) if k / ∈ K corrupted and b=1 and ∃σ : (m, σ ) ∈Signatures(vk)

  save corruption request for h rcv(GenerateNonceGuess, sid ) from A h ← {0, 1} η add h to Pcor save corruption request for h snd (GenerateNonceGuess • , sid , h) to A rcv (CorruptionStatus,sid ,h) from Ui if corruption request for h was saved snd (CorruptionStatus • ,sid ,Corrupted) to U else snd ⊥ to U

	(Cmd,h,m)
	¥
	Listing 1.5. A nonce-generaration functionality F Nonce

structure: List: P, Pcor ⊂ P rcv(Generate, sid ) from any P: h ← {0, 1} η snd (Generate • , sid , h) to P rcv(Equal, sid , h1, h2) for any P if h1 = h2 or h1 ∈ Pcor or h2 ∈ Pcor then snd (Equal • ,sid ,YES) to P else snd (Equal • ,sid ,NO) to P rcv(Corrupt, sid ,h) from A snd (Corrupt • , sid , h) to A

  and the external dummy users in Φ ext can address the KU-functionalities.) Neither state, nor phase of F KM and any ST are affected, thus state consistency and phase hold. Both F KM and the ST i ignore messages coming from the functionalities, except while processing a Command ∈ C. Consistency of functionalities and output consistency is preserved, because the functionalities are equal in both worlds and receive the same input. Hence, consistency of functionalities follows from the induction hypothesis. Case: to(m k ) = ST i and phase set-up -m=(New,sid ,F,a) while (F=F KW and a>0 ) or (F∈ {F 1

A F KW and the commitment problem

In F KM , as well as in the proposed implementation of a Security API, ST , we rely on the key-wrapping functionality F KW . Due to the commitment problem, it is not possible to realize this functionality under dynamic corruption of keys, therefore F KM is not realizable in this form. This following section will explain the commitment problem and explain out the difference of dynamic corruption in the context of Security APIs to the traditional understanding. It will furthermore show how to realize F KW using an existing definition of wrapping schemes from [KSW11] for all runs where the commitment problem does not occur.

We build on a definition for deterministic, authenticated wrapping-schemes, going back to the original work by Rogaway and Shrimpton [RS06] which has been adapted to a multi-user setting and to allow key-dependant messages in [KSW11]. We further generalised it to allow the same key to be encrypted several times with different attributes. This is necessary in our work, because we support attribute changes, therefore a key can have different attributes on different machines. A leakage function serves as a parameter in F KW . It determines the amount of information about the message that is ideally given to the wrapping algorithm.

Typically, it outputs a random string with a length that depends on the length of the message, the key, and the bound attribute. F KW is detailed in Listing 1.8.

We chose deterministic encryption because it is used in most hardware tokens, and because we can show that it is possible to implement F KW using a keywrapping scheme as described in Definition 17 in [KSW11]. The security F KM provides depends on the authenticity and secrecy provided by F KW , however, F KW can easily be modified to define probabilistic encryption, by not performing the test ''If there is c*" after reception of a message (Wrap,sid ,. . . ), but jumping directly into the else branch. It would be interesting to investigate how asymmetric encryption schemes could be used here, but this is out of the scope of this work.

params: X ,K ⊂ X ,H, Y #message-,key-,attribute-and ciphertext space P #distribution of pointers, with support disjoint from X #requirement: ∀p ∈ support(P) : Pr