Design and formal verification of a CEM protocol with transparent TTP
Design and formal verification of a CEM protocol with transparent TTP
Zhiyuan LIU1, Jun PANG2(), Chenyi ZHANG3
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
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.
Corresponding Author(s):
PANG Jun,Email:jun.pang@uni.lu
引用本文:
. Design and formal verification of a CEM protocol with transparent TTP[J]. Frontiers of Computer Science, 2013, 7(2): 279-297.
Zhiyuan LIU, Jun PANG, Chenyi ZHANG. Design and formal verification of a CEM protocol with transparent TTP. Front Comput Sci, 2013, 7(2): 279-297.
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
