# Advanced cryptography: Symbolic methods for security analysis

Instructor:Daniele Micciancio

# Homework 1

In their landmark paper "New directions in cryptography", Diffie and Hellman consider the following two constructions of one-way functions from a (family of) block ciphers E: {0,1}^n x {0,1}^m -> {0,1}^m:

1. Fix a message p (e.g., the all zero string p=0), and define f(x) = E(x,p), i.e., p encrypted under key x.
2. Assuming n=m, define f(x) = E(x,x)

Remember the definition of one-way function:

Definition:A function f is (t,epsilon)-one-way if there is an efficient algorithm that on input x, outputs f(x), but for any algorithm A running in time at most t, the probability that f(A(f(x))) = f(x) (when x is chosen uniformly at random from the domain of f) is less than epsilon)..

In the above definition and below in the homework, you can consider either the asymptotic setting (where t and epsilon are functions of the input length n=|x|, and for every polynomial t(n) there is a negligible function epsilon(n) such that for any n function f(x):{0,1}^n -> {0,1}* is (t(n),epsilon(n))-one-way) or concrete values of t and epsilon, whatever you find more convenient. In the asymptotic setting, of course, we are assuming the existence of a family of block ciphers (one for every value of n).

Block ciphers are typically modeled as super-pseudorandom permutations. Intuitively a function family is super-pseudo random if no polynomial time adversary can tell the difference between a function from the family and a real random function, given oracle access to the function and its inverse.

Definition: A family of permutations f_k(x) (where |k|=n and |x|=m) is super-pseudorandom if for every polynomial time oracle algorithm A, the difference between the probability that A outputs one in the following two experiments is negligible:

1. Choose k at random, and run A with oracle access to f_k and (f_k)^{-1}.
2. Choose f as a random permutation from {0,1}^m to {0,1}^m, and run A with oracle access to f and f^{-1}. (Technically, f is implemented as an algorithm that keeps track of all the queries asked by A, and answers new queries at random)

It is also assumed that f_k and its inverse can be efficiently computed, given knownedge of the key k.

The above permutations are called "super"-pseudorandom because A is given access to both f and its inverse, i.e., it can make both encryption and decryption queries to the block cipher. A similar definition where A has only access to f results in the standard definition of pseudorandom function. Superpseudorandom permutations can be efficiently obtained from pseudorandom functions, using a construction of Luby and Rackoff, but we are not concerned with this distinction here, and only consider the stronger notion of super-pseudorandom permutation.

Question 1: Show that construction 2 is not provably secure in the sense that (under minimal assumptions, see below) there exists a family of super-pseudorandom permutations E(k,*) such that the corresponding function f(x) = E(x,x) is not one-way.

Since super-pseudorandom permutations are not known to exist, in order to answer the question you need to make some assuption: at very least, you need to assume that super-pseudorandom permutations exist (which turns out to be equivalent to the existence of one-way functions, but that's a long, long proof. If you want to know more ... ask Russell.) It turns out that this is all you need. You should interpret the "Under minimal assumption" as "Prove that if super-pseudorandom permutations exist at all, then there exists a super-pseudorandom permutation family with the properties claimed in question 1". This also gives you a hint about how to approach the problem: start from an arbitrary super-pseudorandom permutation family, and show how to modify it in such a way that it is still provably super-pseudorandom, but the corresponding function f(x) = E(x,x) can be easily inverted.

Question 2: Prove that when m>n construction (1) is secure, i.e., for any family of super-pseudorandom permutations E(*,*) and fixed message p (e.g., p=0), the function f(x) = E(x,p) is one-way.

Notice that the assumption m>n is relatively common. E.g., DES uses keys of size n=56 and messages of size m=64 > n.

Extra Question: Can you answer question 2 for the case when m=n?

# Homework 2

In this assignment you are asked to use the Murphi model checker to model and analyze a simple security protocol. We describe the security protocol first.

Consider a set of clients Client[1],..., Client[n] that want to securely communicate with a Server using symmetric encryption. Each Client[i] has a long term symmetric key CK[i], known only to Client[i] and the Server. In order to protect the long term key, we want to minimize its usage, and use it only to securely communicate a session key SK[i] to be used by Client[i] and Server to encrypt regular communications. In summary, the server holds two tables of keys:

• ClientKeyTable[i=1..n] holding the long term keys CK[i] of the users
• SessionKeyTable[i=1..n] holding the current session key SK[i] of every user.

Each client Client[i] holds the long term key CK[i], and receives the session key SK[i] from the server encrypted under CK[i]. (The session key can be used to encrypt/decrypt subsequent communications, but in this assignment we are not concerned with that.)

For additional protection (e.g., to guard against insider attacks, or server break-in's) the key tables of the server are stored in encrypted form. Each entry in the ClientKeyTable or SessionKeyTable contains CK[i] or SK[i] encrypted under a master key (MasterKeyCKT and MasterKeySKT respectively). Of course, storing the master keys on the server as well would not offer any additional protection. So, the master keys are stored on a special tamper proof device, e.g., a smartcard, that does not offer direct access to the master keys. Rather the smartcard offers only the essential services required by the server to operate correctly. Namely, the smartcard allows to perform the following operations:

• Encrypt a message for a client: given as input a message m and an entry from the SessionKeyTable, outputs the encryption of m under the corresponding session key. Formally, this operation takes as input a message m and a ciphertext c, and performs the following steps:
1. Decrypt c using the MasterKeySKT to obtain a key k
2. Encrypt m under k and output the result
• Decrypt a message from a client: given a ciphertext and an entry from the SessionKeyTable, output the decryption of the ciphertext under the given session key. Formally, this operation takes two ciphertexts c1 and c2 and performs the following steps:
1. Decrypt c2 using the MasterKeySKT to obtain a key k
2. Decrypt c1 using k and output the result
• Re-encrypt a key: Given an entry from the ClientKeyTable and the corresponding entry from the SessionKeyTable, encrypt the session key from the second entry under the long term key from the first entry. Formally, this operation takes two ciphertexts c1 and c2 and performs the following operations:
1. Decrypt c1 using MasterKeyCKT to obtain a key k1
2. Decrypt c2 using MasterKeySKT to obtain a key k2
3. Encrypt k2 under k1 and output the result.

We consider a scenario where the adversary breaks into the server and gets access to the encrypted key tables as well as the smartcard. Specifically, the adversary can learn all the encrypted entries in the key tables, and get the smartcard to compute any of the three functions on adversarially chosen inputs. The question is: can the adversary learn any of the clients' long term or session keys? (Remember, all these keys are encrypted, and the adversary does not have direct access to the master keys used for encryption.)

Define a model in Murphi corresponding to the above scenario, state the relevant security properties, and run the analysis of the system under the following two setting:

• The ClientKeyTable and SessionKeyTable are encrypted under different master keys
• The same master key is used to encrypt both the ClientKeyTable and SessionKeyTable

In order to help you get started with the assignment, here is the definition of relevant constants, types, global variables and some auxiliary functions. See explainations below.

```-- Murphi model for the analysis of client server application
const
NumClients: 100;
MaxKeys: 1000;
MaxMem: 10000;
SAME_KEY: false;

type
ClientT: scalarset(NumClients);
KeyT: 0..MaxKeys;

TextT: record
-- Enc_key[data] or just data if key is undefined
data, key: KeyT;
end;

var
LastKey: KeyT;

ClientKeyTable, SessionKeyTable: array [ClientT] of TextT;
MasterKeyCKT, MasterKeySKT: KeyT;

SmartcardIN: array[1..2] of TextT;
SmartcardOUT: TextT;

AdvKnow: multiset[MaxMem] of TextT;

-- Functions and Procedures

function isCiphertext(text: TextT): boolean;
-- Check if text is a ciphertext
begin
return !isundefined(text.key);
end;

function isPlaintext(text: TextT): boolean;
-- Check if text is a plaintext
begin
return (isundefined(text.key) & !isundefined(text.data));
end;

function NewKey(): KeyT;
-- Generate a new key
begin
if LastKey < MaxKeys
then LastKey := LastKey+1; return LastKey;
else error "Too many keys"
end;
end;```

The model is parametric with respect to the number of clients (NumClients). The function NewKey can be used to generate new keys, and should be used to initialize the master keys and the tables. The parameter MaxKeys is a bound on the number of times the function NewKey can be called. The data type TextT can be used to represent some data optionally encrypted under a key, with the convention that if the field key is undefined than the data is unencrypted. Functions isCiphertext and isPlaintext take a value of type TextT as input, and will return true if and only if text is a ciphertext or unencrypted piece of data. The client server application described earlier requires the encryption function to be applied both to keys (e.g., in the table entries) and plain data (e.g., in client encryption/decryption). For simplicity, we assume that the messages encrypted/decrypted by the clients are also keys.

The global state of the system is defined by the following variables:

• LastKey: internal variable used by NewKey to generate fresh keys. This variable should not be used anywhere else in the model, except possibly for checking that we can generate new keys.
• MasterKeyCKT, MasterKeySKT: master keys used to encrypt the two tables stored on the server. These should be initialized to different or the same value depending on the constant parameter SAME_KEY.
• ClientKeyTable, SessionKeyTable: Tables holding the encryption of the long term and session keys of the clients. These tables should be initialized once and for all at the beginning. In a real application SessionKeyTable would be dynamic, and its entries would change over time when a client want to change its session key. For simplicity, in this assignment, you can consider the simplest case where the content of SessionKeyTable does not change during the attack.
• AdvKnow: collection of TextT values, representing the knowledge of the adversary. Remember that each TextT value can represent either a ciphertext, or a plain message (e.g., a key). Adversary should be able to perform all kinds of actions like encrypting a known key under a known key, decrypting a known ciphertext under a known key, learn values from ClientKeyTable and SessionKeyTable, reading/writing the input/output of the smartcard, invoke any of the three smartcard operations on the given inputs, etc. The parameter MaxMem represents the maximum number of values that the adversary can hold in its memory and it is necessary to bound the size of the system. The adversary may also generate new keys (with the function NewKey) or clear some of the entries in AdvKnow in order to reuse memory.
• SmartcardIN, SmartcardOUT: input and output values of the smartcard. The adversary has access to the master keys only through these variables and the operations performed by the smartcard.

Your assignment: In brief, your solution should be both informative and easy to read. You can use your common sense to determine what constitutes an adequate solution. In case you are still not sure about what I expect from you, here are more details. You should complete the above model introducing appropriate startstate, rules and invariants. Test the security of the system both when SAME_KEY is true or false, and using appropriate values of the constants. (The values 100, 1000, 10000 given above are probably too big, and you need to down scale the system in order to run it.) As you model the system you might be faced with modeling choices. Your solution should include a detailed description of your modeling choices, as well as a well documented Murphi source program. You should also report the details of the system you used to run the experiments, running times and comment on your findings. E.g., if you find an attack, you should give the trace of the attack, as output by the Murphi model checker, and also written in informal protocol notation. You should probably first analyze the system, by writing and running a Murphi program, and also after you are done with the analysis, starts writing your report. Please, mail your solutions (both the report in ps or pdf format, the Murphi source and output of the experiment) to Daniele by the due date. The report should be self contained, i.e., readable without the need to referencing the source program all the times.