SAS

Abstract

In the formal analysis of security protocols, what the intruder infers from messages travelling on the network can be abstracted into checking whether a term is derivable in an inference system from a given finite set of terms. Thus verification amounts (essentially) to studying bounds on proof size. We use this technique in the context of distributive encryption to show that the verification problem is DEXPTIME-complete. The work reported is joint with A. Baskar (Darmstadt) and S.P.Suresh (Chennai).