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:

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:

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:

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:

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.