Design and formal verification of a CEM protocol with transparent TTP

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

References

[1] Onieva J, Zhou J, Lopez J. Multiparty nonrepudiation: a survey. ACM Computing Surveys (CSUR), 2008, 41(1): 5

[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

[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

[6] Chadha R, Kremer S, Scedrov A. Formal analysis of multiparty contract signing. Journal of Automated Reasoning, 2006, 36(1): 39-83

[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

[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

[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

[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

[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

[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

[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

[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

[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

[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

[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

[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

[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

[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

[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

[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

[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

[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

[56] Emerson E, Namjoshi K. On reasoning about rings. International Journal of Foundations of Computer Science, 2003, 14(4): 527-549

[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

RIGHTS & PERMISSIONS

2014 Higher Education Press and Springer-Verlag Berlin Heidelberg