University of Luxembourg
CADP (Construction and Analysis of Distributed Processes)
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.
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.
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,
Available on-line at: http://satoss.uni.lu/members/jun/papers/TTSS10.pdf
or from the CADP Web site in PDF or PostScript
University of Luxembourg
Computer Science and Communications
Office: Campus Kirchberg, E204
6, rue Richard Coudenhove-Kalergi
Tel: (+352) 46 66 44 5625
Fax: (+352) 46 66 44 5620 (with a cover page)
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|