Impossibility Results for secret establishment

Security protocol design is a creative discipline where the solution space depends on the problem to be solved and the cryptographic operators available. In this paper, we examine the general question of when two agents can create a shared secret. Namely, given an equational theory describing the cryptographic operators available, is there a protocol that allows the agents to establish a shared secret?

We examine this question in several settings. First, we provide necessary and sufficient conditions for secret establishment using subterm convergent theories. This directly yields a decision procedure for this problem. As a consequence, we obtain impossibility results for symmetric encryption and signature schemes. Second, we use algebraic methods to prove impossibility results for two important theories that are not subterm convergent: XOR and abelian groups. Finally, we develop a general combination result that enables modular impossibility proofs. For example, the results for symmetric encryption and XOR can be combined to obtain impossibility for the joint theory.

Demo

Sig = {enc,dec,pair,p1,p2,sign,extr,check,sk,pk}
Eqs = {enc(dec(m,k),k) = m,
       p1(pair(x,y)) = x,
       p2(pair(x,y)) = y,
       check(sign(m,sk(k)),pk(k)) = m,		
       extr(sign(m,sk(k)))  = m}

Sig = {enc, dec,sk,pk}
Eqs = {enc(dec(m,pk(k)),sk(k)) = m}

Sig = {enc,dec}
Eqs = {dec(dec(enc(enc(m,k1),k2),k1),k2) = m,
       dec(enc(m,k),k) = m}