Design and formal verification of a CEM protocol with transparent TTP

doi:10.1007/s11704-013-1268-6

Front Comput Sci

2013, Vol. 7

Issue (2) : 279-297 https://doi.org/10.1007/s11704-013-1268-6

RESEARCH ARTICLE

Design and formal verification of a CEM protocol with transparent TTP

Zhiyuan LIU¹, Jun PANG²(

), Chenyi ZHANG³

1. School of Management Science and Engineering, Shandong Normal University, Jinan 250000, China; 2. Faculty of Science, Technology and Communication, University of Luxembourg, Luxembourg 1359, Luxembourg; 3. School of Information Technology and Electrical Engineering, University of Queensland, Brisbane QLD4072, Australia

Download: PDF(500 KB) HTML
Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks

Abstract

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. Cederquist et al. proposed an optimistic certified email protocol, which employs key chains to reduce the storage requirement of the TTP. We extend their protocol to satisfy the property of TTP transparency, using existing verifiably encrypted signature schemes. An implementation with the scheme based on bilinear pairing makes our extension one of the most efficient CEM protocols satisfying strong fairness, timeliness, and TTP transparency. We formally verify the security requirements of the extended protocol. The properties of fairness, timeliness and effectiveness are checked in the model checker Mocha, and TTP transparency is formalised and analysed using the toolsets μCRL and CADP.

Keywords fair exchange CEM protocols fairness TTP transparency formal verification

Corresponding Author(s): PANG Jun,Email:jun.pang@uni.lu

Issue Date: 01 April 2013

Cite this article:

Zhiyuan LIU,Jun PANG,Chenyi ZHANG. Design and formal verification of a CEM protocol with transparent TTP[J]. Front Comput Sci, 2013, 7(2): 279-297.

URL:

https://academic.hep.com.cn/fcs/EN/10.1007/s11704-013-1268-6
https://academic.hep.com.cn/fcs/EN/Y2013/V7/I2/279

1	Onieva J, Zhou J, Lopez J. Multiparty nonrepudiation: a survey. ACM Computing Surveys (CSUR) , 2008, 41(1): 5 doi: 10.1145/1456650.1456655
2	Asokan N, Schunter M, Waidner M. Optimistic protocols for fair exchange. In: Proceedings of the 4th ACM conference on Computer and Communications Security . 1997, 7-17
3	Dolev D, Yao A. On the security of public key protocols. IEEE Transactions on Information Theory , 1983, 29(2): 198-208 doi: 10.1109/TIT.1983.1056650
4	Kremer S, Raskin J. A game-based verification of non-repudiation and fair exchange protocols. In: Proceedings of the 12th International Conference on Concurrency Theory . 2001, 551-565
5	Anderson B, Hansen J, Lowry P, Summers S. Standards and verification for fair-exchange and atomicity in e-commerce transactions. Information Sciences , 2006, 176(8): 1045-1066 doi: 10.1016/j.ins.2005.01.016
6	Chadha R, Kremer S, Scedrov A. Formal analysis of multiparty contract signing. Journal of Automated Reasoning , 2006, 36(1): 39-83 doi: 10.1007/s10817-005-9019-5
7	Zhang Y, Zhang C, Pang J, Mauw S. Game-based verification of multiparty contract signing protocols. In: Proceedings of the 6th International Conference on Formal Aspects in Security and Trust . 2009, 186-200
8	Chen M, Wu K, Xu J, He P. A new method for formalizing optimistic fair exchange protocols. In: Proceedings of the 12th International Conference on Information and Communications Security . 2010, 251-265 doi: 10.1007/978-3-642-17650-0_18
9	Gaber T, Zhang N. Fair and abuse-free contract signing protocol supporting fair license reselling. In: Proceedings of the 4th IFIP International Conference on New Technologies, Mobility and Security (NTMS) . 2011, 1-7
10	Chatterjee K, Raman V. Synthesizing protocols for digital contract signing. In: Proceedings of the 13th International Conference on Verification, Model Checking, and Abstract Interpretation . 2012, 152-168 doi: 10.1007/978-3-642-27940-9_11
11	Williams D, Ruiter d J, Fokkink W. Model checking under fairness in prob and its application to fair exchange protocols. Theoretical Aspects of Computing-ICTAC 2012 , 2012, 168-182
12	Zhang Y, Zhang C, Pang J, Mauw S. Game-based verification of contract signing protocols with minimal messages. Innovations in Systems and Software Engineering , 2012, 8(2): 111-124 doi: 10.1007/s11334-012-0180-9
13	Micali S. Certified email with invisible post offices. In: Proceedings of the RSA Security Conference . 1997
14	Markowitch O, Kremer S. An optimistic non-repudiation protocol with transparent trusted third party. In: Proceedings of the 4th International Conference on Information Security . 2001, 363-378
15	Imamoto K, Sakurai K. A certified e-mail system with receiver’s selective usage of delivery authority. In: Proceedings of the 3rd International Conference on Cryptology: Progress in Cryptology . 2002, 326-338
16	Ateniese G, Nita-Rotaru C. Stateless-recipient certified e-mail system based on verifiable encryption. In: Proceedings of the Cryptographer’s Track at the RSA Conference on Topics in Cryptology . 2002, 182-199
17	Micali S. Simple and fast optimistic protocols for fair electronic exchange. In: Proceedings of the 22nd Annual ACM Symposium on Principles of Distributed Computing . 2003, 12-19
18	Nenadi? A, Zhang N, Barton S. Fair certified e-mail delivery. In: Proceedings of the 2004 ACM Symposium on Applied Computing . 2004, 391-396 doi: 10.1145/967900.967985
19	Wang G. Generic non-repudiation protocols supporting transparent offline TTP. Journal of Computer Security , 2006, 14(5): 441-467
20	Ma C, Li S, Chen K, Liu S. Analysis and improvement of fair certified e-mail delivery protocol. Computer Standards & Interfaces , 2006, 28(4): 467-474 doi: 10.1016/j.csi.2005.03.002
21	Liang X, Cao Z, Lu R, Qin L. Efficient and secure protocol in fair document exchange. Computer Standards & Interfaces , 2008, 30(3): 167-176 doi: 10.1016/j.csi.2007.08.003
22	Hwang R, Lai C. Efficient and secure protocol in fair e-mail delivery. WSEAS Transactions on Information Science and Applications , 2008, 5: 1385-1394
23	Cederquist J, Dashti M, Mauw S. A certified email protocol using key chains. In: Proceedings of the 21st International Conference on Advanced Information Networking and Applications Workshops . 2007, 525-530
24	Zhang F, Safavi-Naini R, Susilo W. Efficient verifiably encrypted signature and partially blind signature from bilinear pairings. In: Proceedings of the 5th Conference on Cryptology in India . 2003, 71-84
25	Alur R, Henzinger T, Mang F, Qadeer S, Rajamani S, Tasiran S. MOCHA: Modularity in model checking. Computer Aided Verification , 1998, 521-525
26	Alur R, Henzinger T, Kupferman O. Alternating-time temporal logic. Journal of the ACM , 2002, 49(5): 672-713 doi: 10.1145/585265.585270
27	Blom S, Fokkink W, Groote J, Langevelde I, Lisser B, Pol J. μCRL: a toolset for analysing algebraic specifications. In: Proceedings of the 13th International Conference on Computer Aided Verification . 2001, 250-254 doi: 10.1007/3-540-44585-4_23
28	Blom S, Calamé J, Lisser B, Orzan S, Pang J, Van De Pol J, Dashti M, Wijs A. Distributed analysis with μ CRL: a compendium of case studies. Tools and Algorithms for the Construction and Analysis of Systems , 2007, 4424: 683-689 doi: 10.1007/978-3-540-71209-1_53
29	Fernandez J, Garavel H, Kerbrat A, Mounier L, Mateescu R, Sighireanu M. CADP a protocol validation and verification toolbox. Computer Aided Verification , 1996, 437-440
30	Liu Z, Pang J, Zhang C. Extending a key-chain based certified email protocol with transparent TTP. In: Proceedings of the 8th IEEE/IFIP International Conference on Embedded and Ubiquitous Computing (EUC) . 2010, 630-636
31	Liu Z, Pang J, Zhang C. Verification of a key-chain based TTP transparent CEMprotocol. In: Proceedings of the 3rdWorkshop on Harnessing Theories for Tool Support in Software . 2011, 51-65
32	Gürgens S, Rudolph C, Vogt H. On the security of fair non-repudiation protocols. Information Security , 2003, 4(4): 253-262 doi: 10.1007/s10207-004-0063-7
33	Asokan N, Shoup V, Waidner M. Optimistic fair exchange of digital signatures. IEEE Journal an Selected Areas in Communications , 1998, 18: 591-606
34	Bao F, Deng R, Mao W. Efficient and practical fair exchange protocols with off-line ttp. In: Proceedings the 1998 IEEE Symposium on Security and Privacy . 1998, 77-85
35	Boyd C, Foo E. Off-line fair payment protocols using convertible signatures. In: Proceedings of the International Conference on the Theory and Applications of Cryptology and Information Security: Advances in Cryptology . 1998, 271-285
36	Camenisch J, Damg?rd I. Verifiable encryption, group encryption, and their applications to separable group signatures and signature sharing schemes. In: Proceedings of the 6th International Conference on the Theory and Application of Cryptology and Information Security: Advances in Cryptology . 2000, 331-345
37	Cathalo J, Libert B, Quisquater J. Cryptanalysis of a verifiably committed signature scheme based on GPS and RSA. In: Proceedings of the 4th Conference on Information Security . 2004, 52-60 doi: 10.1007/978-3-540-30144-8_5
38	Bao F. Colluding attacks to a payment protocol and two signature exchange schemes. In: ASIACRYPT 2004 , LNCS 3329: 417-429
39	Ateniese G. Efficient verifiable encryption (and fair exchange) of digital signatures. In: Proceedings of the 6th ACM conference on Computer and communications security . 1999, 138-146
40	Boneh D, Gentry C, Lynn B, Shacham H. Aggregate and verifiably encrypted signatures from bilinear maps. Advances in Cryptology _EUROCRYPT 2003, 416-432
41	Grabher P, Gro?sch?dl J, Page D. On software parallel implementation of cryptographic pairings. In: Proceedings of the 13th Workshop on Selected Areas in Cryptography . 2009, 35-50 doi: 10.1007/978-3-642-04159-4_3
42	Gro?sch?dl J. Personal communications. World Scientific , 2010
43	Gürgens S, Rudolph C. Security analysis of (un-) fair non-repudiation protocols. Formal Aspects of Security , 2003, 229-232
44	Boneh D. Twenty years of attacks on the RSA cryptosystem. Notices of the AMS , 1999, 46(2): 203-213
45	Cederquist J, Corin R, Dashti M. On the quest for impartiality: design and analysis of a fair non-repudiation protocol. In: Proceedings of the 7th international conference on Information and Communications Security . 2005, 27-39 doi: 10.1007/11602897_3
46	Abadi M, Blanchet B. Computer-assisted verification of a protocol for certified email. In: Proceedings of the 10th international conference on Static analysis . 2003, 316-335
47	Groote J, Pang J, Wouters A. Analysis of a distributed system for lifting trucks. Journal of Logic and Algebraic Programming , 2003, 55(1): 21-56 doi: 10.1016/S1567-8326(02)00038-3
48	Fokkink W,Pang J, Pol v. d J. Cones and foci: a mechanical framework for protocol verification. Formal Methods in System Design , 2006, 29(1): 1-31 doi: 10.1007/s10703-006-0004-3
49	Pang J, Fokkink W, Hofman R, Veldema R. Model checking a cache coherence protocol for a Java DSM implementation. In: Proceedings of the 17th International Symposium on Parallel and Distributed Processing . 2003, 238-249
50	Pang J. Analysis of a security protocol in μCRL. In: Proceedings of the 4th Conference on Formal Engineering Methods . 2002, 396-400 doi: 10.1007/3-540-36103-0_40
51	Blom S, Groote J, Mauw S, Serebrenik A. Analysing the BKE-security protocol with μCRL. Electronic Notes in Theoretical Computer Science , 2005, 139(1): 49-90 doi: 10.1016/j.entcs.2005.09.005
52	Chothia T, Orzan S, Pang J, Dashti M. A framework for automatically checking anonymity with μCRL. In: Proceedings of the 2nd international conference on Trustworthy global computing . 2006, 301-318
53	Liu Z. Extending a certified email protocol with ttp transparency and its formal verification. Master’s thesis, University of Luxembourg , 2010
54	Milner R. A calculus of communicating systems. Springer-Verlag New York, Inc. , 1982
55	Henzinger T, Majumdar R, Mang F, Raskin J. Abstract interpretation of game properties. In: Proceedings of the 7th International Symposium on Static Analysis . 2000, 220-239 doi: 10.1007/978-3-540-45099-3_12
56	Emerson E, Namjoshi K. On reasoning about rings. International Journal of Foundations of Computer Science , 2003, 14(4): 527-549 doi: 10.1142/S0129054103001881
57	Paulson L. The inductive approach to verifying cryptographic protocols. Journal of computer security , 1998, 6(1-2): 85-128
58	Abadi M, Fournet C. Mobile values, new names, and secure communication. ACM SIGPLAN Notices , 2001, 36(3): 104-115 doi: 10.1145/373243.360213

[1]	Kazuhiro OGATA. A divide & conquer approach to liveness model checking under fairness & anti-fairness assumptions[J]. Front. Comput. Sci., 2019, 13(1): 51-72.
[2]	Yongwang ZHAO, Zhibin YANG, Dianfu MA. A survey on formal specification and verification of separation kernels[J]. Front. Comput. Sci., 2017, 11(4): 585-607.
[3]	Yuyue DU,Yuhui NING. Property analysis of logic Petri nets by marking reachability graphs[J]. Front. Comput. Sci., 2014, 8(4): 684-692.
[4]	Jingyuan WANG,Jiangtao WEN,Yuxing HAN,Jun ZHANG,Chao LI,Zhang XIONG. Achieving high throughput and TCP Reno fairness in delay-based TCP over large networks[J]. Front. Comput. Sci., 2014, 8(3): 426-439.
[5]	Yuanjie SI, Jun SUN, Yang LIU, Jin Song DONG, Jun PANG, Shao Jie ZHANG, Xiaohu YANG. Model checking with fairness assumptions using PAT[J]. Front. Comput. Sci., 2014, 8(1): 1-16.
[6]	Van Chan NGO, Jean-Pierre TALPIN, Thierry GAUTIER, Paul Le GUERNIC, Lo?c BESNARD. Formal verification of synchronous data-flow program transformations toward certified compilers[J]. Front Comput Sci, 2013, 7(5): 598-616.
[7]	Yuehua DAI, Yi SHI, Yong QI, Jianbao REN, Peijian WANG. Design and verification of a lightweight reliable virtual machine monitor for a many-core architecture[J]. Front Comput Sci, 2013, 7(1): 34-43.

Viewed

Full text

Abstract

Cited

Shared

Discussed