Title: Formalizing key properties for fair exchange protocols and
its applications

Contact person: Dr. Jun Pang

Short description:
In certified email (CEM) protocols, trusted third party (TTP)
transparency is an important security requirement which helps to avoid
bad publicity as well as protecting individual users' privacy. There
are a number of CEM protocols in the literature that supports the
transparency of TTP.

In this project, we will investigate ways to formalize TTP
transparency taking into account the underlying cryptographic
techniques to realize this property and the ability of the adversary
in terms of Dolev-Yao's symbolic model. One possible direction is to
interpret TTP transparency using the notion of static equivalence in
the applied pi calculus. After achieving a formal understanding of TTP
transparency, we will cover other desired properties such as stateless
TTP and accountability.

Prerequisites:
        - Security protocols
        - Formal methods

References:
Extending a key-chain based certified email protocol with transparent
TTP.  Zhiyuan Liu, Jun Pang, and Chenyi Zhang.  In Proc. 6th IEEE/IFIP
Symposium on Trusted Computing and Communications - TrustCom'10,
pp. 630-636. IEEE Computer Society, 2010.