Verification of a Key Chain Based TTP Transparent CEM Protocol

Organisation:	University of Luxembourg
Method:	Mocha language muCRL
Tools used:	CADP (Construction and Analysis of Distributed Processes) Mocha muCRL
Domain:	Security Protocols.
Period:	2010-2011
Size:	n/a
Description:	Certified email (CEM) protocols, as an extension of regular email services, require that both senders and receivers be responsible for their roles in the email services, i.e., neither the sender can deny the dispatch of the email, nor can the receiver deny the receipt. This is usually implemented by a non-repudiable evidence of origin (EOO) that is to be acquired by the receiver, and a non-repudiable evidence of receipt (EOR) that is to be acquired by the sender. A CEM protocol is supposed to guarantee fairness with respect to non-repudiable evidences, meaning that, at the end of a fair protocol run, either both parties acquire all the evidences, or no party gets an evidence. A trusted third party (TTP) can be introduced to take charge of the whole procedure and to provide undeniable records of submission (of the sender) and delivery (of the receiver). TTP transparency states that if a TTP has been contacted to help in a protocol, the resulting evidences will be the same as those obtained in the case where the TTP has not participated. This work deals with the formal analysis of a recently proposed CEM protocol with a transparent TTP, that applies key chains to reduce TTP's storage requirement. TTP transparency is achieved by using a verifiably encrypted signature scheme. Two kinds of formal analysis were carried out. First, the CEM protocol was described in the guarded command language of the Mocha model checker. The properties of strong fairness, effectiveness, and timeliness were specified in ATL (Alternating-time Temporal Logic) and verified using the Mocha model checker. Second, the protocol was specified in muCRL and the corresponding state spaces were analyzed using CADP by comparing the execution traces for getting evidences in the system with only honest participants and in the system containing dishonest participants. The analysis revealed that traces leading to evidences in the system containing dishonest participants do not involve TTP participation, which indicates that the CEM protocol satisfies TTP transparency.
Conclusions:	The way to formalize TTP transparency in this case study is rather abstract w.r.t. the underlying cryptographic techniques and the ability of the adversary. Future work regards the investigation of other approaches for encoding TTP transparency, e.g., using an applied pi-calculus. The CEM protocol can also be extended to cover other design goals such as stateless TTP and accountability.
Publications:	[Liu-Pang-Zhang-11] Zhiyuan Liu, Jun Pang, and Chenyi Zhang. "Verification of A Key Chain Based TTP Transparent CEM Protocol". Proceedings of the 4th International Workshop on Harnessing Theories for Tool Support in Software TTSS'10, ENTCS vol. 274, pages 51-65, 2011. Available on-line at: http://satoss.uni.lu/members/jun/papers/TTSS10.pdf or from the CADP Web site in PDF or PostScript
Contact:	Jun Pang University of Luxembourg Computer Science and Communications Office: Campus Kirchberg, E204 6, rue Richard Coudenhove-Kalergi L-1359 LUXEMBOURG Tel: (+352) 46 66 44 5625 Fax: (+352) 46 66 44 5620 (with a cover page) Email: Jun.Pang@uni.lu Web: http://satoss.uni.lu/jun/
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page