第 6 章 ハッシュ関数からの情報漏洩を考慮した安全性の形式検証
6.4 結論
■案2のrEROモデル リネームを行う必要が無いよう，EOの出力値は一様ランダムに決定 されることを利用して，定義される処理をあらかじめ1つにまとめた書き換え規則である．
この規則の下では，12回のゲームの変形で証明できた．証明にかかる時間は，約30秒であ る．攻撃者が攻撃に成功する確率は，高々(qS +qR+qE +1)∗ϵ であるとの結果を得た．
第 7 章
結論
本論文では，証明可能安全なRFIDシステム，証明可能安全な追跡不可能電子現金システム を提案した．また，情報を漏えいするランダムオラクルモデルの形式検証についても検証事例 を与えた．
従来の暗号理論では，通信路を流れるデータに対してのみ攻撃が行われる状況を想定して安 全性の解析を行うものが中心であった．しかし，現実には，内部者の不正・不注意による情報 漏洩や，暗号デバイスの物理的解析など，従来の暗号理論のモデルでは捉えきれない攻撃によ り，深刻な被害が生じる例が後を絶たない．
近年の暗号理論では，そのような攻撃技術の発展に対応するため，暗号デバイスからの秘密 情報の漏えいを考慮した攻撃モデルの議論が盛んに行われている．そのような攻撃モデルは，
従来よりも複雑であるため，そのモデルの下での安全性証明も複雑化し，人為的なミスが混入 する可能性や証明のための負荷が増す傾向にある．
本論文では，物理的解析や内部者の不正による情報漏えいを考慮した新たな攻撃モデルを構 築し，それらのモデルの下で安全な暗号システムを提案した．さらに，以下に示すように，そ れらの安全性証明は，適切なモデルを介することにより，安全性証明中の議論を平易にして いる．
第4章では，3つの秘密鍵のみが用いられるよう単純化した攻撃モデルでの単純化方式の安 全性を介して，ハッシュ連鎖により依存関係を持つ複数の秘密鍵が用いられる攻撃モデルでの 提案方式の安全性を証明した．単純化したモデルでは，3つの秘密鍵のうち最新の鍵が攻撃者 に予め与えられるため，弱い意味でのForward-securityを表したモデルといえる．単純化方式 の単純化モデルにおける安全性は，CryptoVerifで検証を行うことで，人手による複雑な議論 を必要としない．つまり，第4章の安全性証明は，形式検証による検証結果を利用すること で，所望の安全性の議論を平易にした．
第5章では，1つの署名鍵のみが用いられるAbeのブラインド署名の攻撃モデルを介して，
複数の発行鍵が用いられる攻撃モデルでの提案方式の安全性を証明した．Abeのブラインド署 名の安全性は，文献[6]で証明されているため，人手によるさらなる議論を必要としない．つ まり，第5章の安全性証明は，既存の証明結果を利用することで，所望の安全性の議論を平易 にした．
第6章では，ランダムオラクルの出力で衝突が生じない限り，文献[74]で与えられた2つの モデルと等価な攻撃モデルを定式化した．文献[74]で定義された攻撃モデルは，CryptoVerif で記述することはできなかったが，第6章で定義した攻撃モデルは，衝突時の振る舞いを単純 化したことで，CryptoVerifで定式化できる．そして，CryptoVerifを用いて，定式化した攻撃 モデルの下でFDH署名の安全性を証明した．すなわち，文献[74]で証明されたFDH署名の 安全性を，衝突が生じた際の振る舞いを単純化した攻撃モデルを介して安全性証明を与えたと 言える．つまり，第６章の安全性証明は，第4章と同様に，形式検証による検証結果を利用す ることで，所望の安全性の議論を平易にした．
このように，本論文では安全性証明の議論がしやすいモデルを考え，その上で大半の議論を 行うという証明技法を用いている．一般に，安全性証明の議論がしやすいモデルには，下記の モデルが考えられる．
• 単純な攻撃モデル
• 証明手法が確立されている攻撃モデル
• 人手による議論が不要な攻撃モデル
本論文では，既存の証明結果や形式検証により，人手による議論が不要な攻撃モデルを見出し て活用することにより，安全性証明中の議論を平易にした．
つまり，既存の証明結果や形式検証可能な安全性より，所望の安全性を導くという安全性証 明の手法を与えたもので，この手法は本論文で議論した以外の方式・安全性に広く適用できる と考えている．そして，本論文で与えた証明技法をより洗練することにより，暗号システムの 高度化・複雑化や，攻撃モデルの発展により複雑化する安全性証明を平易に与えることができ ると期待される．
参考文献
[1] RFID security & privacy lounge. http://www.avoine.net/rfid/.
[2] 電子政府推奨暗号リスト. http://www.cryptrec.go.jp/list.html.
[3] 42nd Annual Symposium on Foundations of Computer Science, FOCS 2001, 14-17 October 2001, Las Vegas, Nevada, USA. IEEE Computer Society, 2001.
[4] Mart´ın Abadi and C´edric Fournet. Mobile values, new names, and secure communication.
InPOPL, pp. 104–115, 2001.
[5] Mart´ın Abadi and Phillip Rogaway. Reconciling two views of cryptography (the computa-tional soundness of formal encryption). J. Cryptology, Vol. 15, No. 2, pp. 103–127, 2002.
[6] Masayuki Abe. A secure three-move blind signature scheme for polynomially many signa-tures. In Birgit Pfitzmann, editor, EUROCRYPT, Vol. 2045 ofLecture Notes in Computer Science, pp. 136–151. Springer, 2001.
[7] Masayuki Abe and Eiichiro Fujisaki. How to date blind signatures. In Kim and Matsumoto [65], pp. 244–251.
[8] Masayuki Abe and Tatsuaki Okamoto. Provably secure partially blind signatures. In Mihir Bellare, editor, CRYPTO, Vol. 1880 of Lecture Notes in Computer Science, pp. 271–286.
Springer, 2000.
[9] Reynald Affeldt and Naoki Kobayashi. A coq library for verification of concurrent programs.
Electr. Notes Theor. Comput. Sci., Vol. 199, pp. 17–32, 2008.
[10] Reynald Affeldt, Miki Tanaka, and Nicolas Marti. Formal proof of provable security by game-playing in a proof assistant. In Willy Susilo, Joseph K. Liu, and Yi Mu, editors, ProvSec, Vol. 4784 ofLecture Notes in Computer Science, pp. 151–168. Springer, 2007.
[11] Jo¨el Alwen, Yevgeniy Dodis, and Daniel Wichs. Leakage-resilient public-key cryptography in the bounded-retrieval model. In Halevi [52], pp. 36–54.
[12] Myrto Arapinis, Tom Chothia, Eike Ritter, and Mark Ryan. Analysing unlinkability and
anonymity using the applied pi calculus. InCSF, pp. 107–121, 2010.
[13] Gilles Barthe, Benjamin Gr´egoire, Sylvain Heraud, and Santiago Zanella B´eguelin. Formal certification of elgamal encryption. In Pierpaolo Degano, Joshua D. Guttman, and Fabio Martinelli, editors, Formal Aspects in Security and Trust, Vol. 5491 of Lecture Notes in Computer Science, pp. 1–19. Springer, 2008.
[14] Gilles Barthe, Benjamin Gr´egoire, Sylvain Heraud, and Santiago Zanella B´eguelin.
Computer-aided security proofs for the working cryptographer. In Phillip Rogaway, edi-tor,CRYPTO, Vol. 6841 ofLecture Notes in Computer Science, pp. 71–90. Springer, 2011.
[15] David Basin and Cas Cremers. Evaluation of iso/iec 9798 protocols. http://www.
cryptrec.go.jp/estimation/techrep id2014 2.pdf, 2010.
[16] Mihir Bellare. Practice-oriented provable-security. InISW, pp. 221–231, 1997.
[17] Mihir Bellare, Chanathip Namprempre, David Pointcheval, and Michael Semanko. The one-more-RSA-inversion problems and the security of chaum’s blind signature scheme. J.
Cryptology, Vol. 16, No. 3, pp. 185–215, 2003.
[18] Mihir Bellare and Phillip Rogaway. Random oracles are practical: A paradigm for designing efficient protocols. In Dorothy E. Denning, Raymond Pyle, Ravi Ganesan, Ravi S. Sandhu, and Victoria Ashby, editors, ACM Conference on Computer and Communications Security, pp. 62–73. ACM, 1993.
[19] Mihir Bellare and Phillip Rogaway. Optimal asymmetric encryption. InEUROCRYPT, pp.
92–111, 1994.
[20] Mihir Bellare and Phillip Rogaway. Code-based game-playing proofs and the security of triple encryption. Cryptology ePrint Archive, Report 2004/331, 2004. http://eprint.
iacr.org/.
[21] Bruno Blanchet. A computationally sound mechanized prover for security protocols. Cryp-tology ePrint Archive, Report 2005/401, 2005. http://eprint.iacr.org/.
[22] Bruno Blanchet. A computationally sound mechanized prover for security protocols. In IEEE Symposium on Security and Privacy, pp. 140–154. IEEE Computer Society, 2006.
[23] Bruno Blanchet, Aaron D. Jaggard, Andre Scedrov, and Joe-Kai Tsay. Computationally sound mechanized proofs for basic and public-key kerberos. In Masayuki Abe and Virgil D.
Gligor, editors,ASIACCS, pp. 87–99. ACM, 2008.
[24] Bruno Blanchet and David Pointcheval. Automated security proofs with sequences of games.
In Cynthia Dwork, editor, CRYPTO, Vol. 4117 of Lecture Notes in Computer Science, pp.
537–554. Springer, 2006.
[25] Dan Boneh. The decision diffie-hellman problem. In Joe Buhler, editor,ANTS, Vol. 1423 of Lecture Notes in Computer Science, pp. 48–63. Springer, 1998.
[26] Stefan Brands. Untraceable off-line cash in wallets with observers (extended abstract). In Douglas R. Stinson, editor, CRYPTO, Vol. 773 of Lecture Notes in Computer Science, pp.
302–318. Springer, 1993.
[27] Gilles Brassard, editor. Advances in Cryptology - CRYPTO ’89, 9th Annual International Cryptology Conference, Santa Barbara, California, USA, August 20-24, 1989, Proceedings, Vol. 435 ofLecture Notes in Computer Science. Springer, 1990.
[28] Mayla Brus`o, Konstantinos Chatzikokolakis, and Jerry den Hartog. Formal verification of privacy for RFID systems. InCSF, pp. 75–88, 2010.
[29] Ran Canetti. Universally composable security: A new paradigm for cryptographic protocols.
InFOCS[3], pp. 136–145.
[30] Ran Canetti. Universally composable security: A new paradigm for cryptographic proto-cols. InFOCS 2001[3], pp. 136–145, An updated version is available at Cryptology ePrint Archive, http://eprint.iacr.prg/2000/067.
[31] Ran Canetti, Ling Cheung, Dilsun Kirli Kaynar, Moses Liskov, Nancy A. Lynch, Olivier Pereira, and Roberto Segala. Analyzing security protocols using probabilistic i/o automata.
InWODES, 2006.
[32] Ran Canetti, Ling Cheung, Dilsun Kirli Kaynar, Moses Liskov, Nancy A. Lynch, Olivier Pereira, and Roberto Segala. Time-bounded task-pioas: A framework for analyzing security protocols. In Shlomi Dolev, editor,DISC, Vol. 4167 ofLecture Notes in Computer Science, pp. 238–253. Springer, 2006.
[33] Ran Canetti and Jonathan Herzog. Universally composable symbolic analysis of mutual authentication and key-exchange protocols. In Shai Halevi and Tal Rabin, editors,TCC, Vol.
3876 ofLecture Notes in Computer Science, pp. 380–403, An updated version is available at Cryptology ePrint Archive, http://eprint.iacr.prg/2004/334. Springer, 2006.
[34] David Chaum. Untraceable electronic mail, return addresses, and digital pseudonyms. Com-mun. ACM, Vol. 24, No. 2, pp. 84–88, 1981.
[35] David Chaum. Blind signatures for untraceable payments. In David Chaum, Ronald L.
Rivest, and Alan T. Sherman, editors, CRYPTO, pp. 199–203. Plenum Press, New York, 1982.
[36] David Chaum, Amos Fiat, and Moni Naor. Untraceable electronic cash. In Shafi Goldwasser, editor, CRYPTO, Vol. 403 of Lecture Notes in Computer Science, pp. 319–327. Springer,
1988.
[37] Xiaofeng Chen, Fangguo Zhang, and Kwangjo Kim. Id-based multi-proxy signature and blind multisignature from bilinear pairings. InKIISC conference 2003, pp. 11–19, 2003.
[38] Jean-S´ebastien Coron. Optimal security proofs for PSS and other signature schemes. In Lars R. Knudsen, editor, EUROCRYPT, Vol. 2332 of Lecture Notes in Computer Science, pp. 272–287. Springer, 2002.
[39] V´eronique Cortier and Bogdan Warinschi. Computationally sound, automated proofs for security protocols. InESOP, pp. 157–171, 2005.
[40] Ronald Cramer and Victor Shoup. Design and analysis of practical public-key encryption schemes secure against adaptive chosen ciphertext attack. SIAM Journal of Computing, Vol. 33, pp. 167–226, 2003.
[41] Ivan Damgård. A design principle for hash functions. In Brassard [27], pp. 416–427.
[42] Jerry den Hartog and Erik P. de Vink. Verifying probabilistic programs using a hoare like logic. Int. J. Found. Comput. Sci., Vol. 13, No. 3, pp. 315–340, 2002.
[43] Yevgeniy Dodis, Thomas Ristenpart, and Thomas Shrimpton. Salvaging merkle-damgård for practical applications. In Antoine Joux, editor,EUROCRYPT, Vol. 5479 ofLecture Notes in Computer Science, pp. 371–388. Springer, 2009.
[44] Danny Dolev and Andrew Chi-Chih Yao. On the security of public key protocols. IEEE Transactions on Information Theory, Vol. 29, No. 2, pp. 198–207, 1983.
[45] Matthew K. Franklin and Moti Yung. Secure and efficient off-line digital money (extended abstract). In Andrzej Lingas, Rolf G. Karlsson, and Svante Carlsson, editors, ICALP, Vol.
700 ofLecture Notes in Computer Science, pp. 265–276. Springer, 1993.
[46] Oded Goldreich, 2007.
[47] Shafi Goldwasser and Silvio Micali. Probabilistic encryption and how to play mental poker keeping secret all partial information. InSTOC, pp. 365–377. ACM, 1982.
[48] Shafi Goldwasser and Silvio Micali. Probabilistic encryption. J. Comput. Syst. Sci., Vol. 28, No. 2, pp. 270–299, 1984.
[49] Shafi Goldwasser, Silvio Micali, and Charles Rackoff. The knowledge complexity of inter-active proof-systems (extended abstract). In Robert Sedgewick, editor,STOC, pp. 291–304.
ACM, 1985.
[50] Shafi Goldwasser, Silvio Micali, and Ronald L. Rivest. A digital signature scheme secure against adaptive chosen-message attacks. SIAM J. Comput., Vol. 17, No. 2, pp. 281–308, 1988.
[51] J. Alex Halderman, Seth D. Schoen, Nadia Heninger, William Clarkson, William Paul, Joseph A. Calandrino, Ariel J. Feldman, Jacob Appelbaum, and Edward W. Felten. Lest we remember: Cold boot attacks on encryption keys. In Paul C. van Oorschot, editor,USENIX Security Symposium, pp. 45–60. USENIX Association, 2008.
[52] Shai Halevi, editor. Advances in Cryptology - CRYPTO 2009, 29th Annual International Cryptology Conference, Santa Barbara, CA, USA, August 16-20, 2009. Proceedings, Vol.
5677 ofLecture Notes in Computer Science. Springer, 2009.
[53] Yoshikazu Hanatani, Yuichi Komano, Kazuo Ohta, and Noboru Kunihiro. Provably se-cure electronic cash based on blind multisignature schemes. In Giovanni Di Crescenzo and Aviel D. Rubin, editors, Financial Cryptography, Vol. 4107 of Lecture Notes in Computer Science, pp. 236–250. Springer, 2006.
[54] Gerhard Hancke and Markus Kuhn. An RFID Distance Bounding Protocol. In Conference on Security and Privacy for Emerging Areas in Communication Networks – SecureComm 2005, pp. 67–73, Athens, Greece, September 2005. IEEE, IEEE Computer Society.
[55] Ryotaro Hayashi and Keisuke Tanaka. The security with the randomness revealed for public-key encryption. InSCIS 2007, 2007.
[56] Patrick Horster, Markus Michels, and Holger Petersen. Blind multisignature scheme based on the discrete logarithm problem. InProc. of 11th Annual Computer Security Applications Conference, pp. 149–155, 1995.
[57] Kazuharu Itakura and Katsuhiro Nakamura. A public key cryptosystem suitable for digital multisignatures. InNEC Research&Development, 71, pp. 1–8, 1983.
[58] Romain Janvier, Yassine Lakhnech, and Laurent Mazar´e. Completing the picture: Soundness of formal encryption in the presence of active adversaries. InESOP, pp. 172–185, 2005.
[59] Ari Juels. Minimalist cryptography for low-cost rfid tags. In Carlo Blundo and Stelvio Cimato, editors, SCN, Vol. 3352 of Lecture Notes in Computer Science, pp. 149–164.
Springer, 2004.
[60] Ari Juels and Stephen Weis. Defining strong privacy for RFID. Cryptology ePrint Archive, Report 2006/137, 2006.
[61] Ari Juels and Stephen Weis. Defining Strong Privacy for RFID. InInternational Conference on Pervasive Computing and Communications – PerCom 2007, pp. 342–347, New York City, New York, USA, March 2007. IEEE, IEEE Computer Society Press.
[62] Ari Juels and Stephen A. Weis. Defining strong privacy for rfid.ACM Trans. Inf. Syst. Secur., Vol. 13, No. 1, 2009.
[63] Yusuke Kawamoto, Hideki Sakurada, and Masami Hagiya. Computationally sound symbolic anonymity of a ring signature. In Joint Workshop on Foundations of Computer Security, Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security (FCS-ARSPA-WITS’08), pp. 161–175, 2008.
[64] Yusuke Kawamoto, Hideki Sakurada, and Masami Hagiya. Computationally sound formal-ization of rerandomizable rcca secure encryption. In V´eronique Cortier, Claude Kirchner, Mitsuhiro Okada, and Hideki Sakurada, editors, Formal to Practical Security, Vol. 5458 of Lecture Notes in Computer Science, pp. 158–180. Springer, 2009.
[65] Kwangjo Kim and Tsutomu Matsumoto, editors. Advances in Cryptology - ASIACRYPT ’96, International Conference on the Theory and Applications of Cryptology and Information Security, Kyongju, Korea, November 3-7, 1996, Proceedings, Vol. 1163 ofLecture Notes in Computer Science. Springer, 1996.
[66] Steve Kremer and Laurent Mazar´e. Adaptive soundness of static equivalence. In Joachim Biskup and Javier Lopez, editors, ESORICS, Vol. 4734 of Lecture Notes in Computer Sci-ence, pp. 610–625. Springer, 2007.
[67] Chin-Laung Lei, Wen-Shenq Juang, and Pei-Ling Yu. Provably secure blind threshold sig-natures based on discrete logarithm. J. Inf. Sci. Eng., Vol. 18, No. 1, pp. 23–39, 2002.
[68] MasterCard and Visa. Set secure electronic transaction specification, book 1: Business de-scription. May 1997.
[69] MasterCard and Visa. Set secure electronic transaction specification book 2: Programmer’s guide. May 1997.
[70] Shin’ichiro Matsuo, Kunihiko Miyazaki, Akira Otsuka, and David A. Basin. How to eval-uate the security of real-life cryptographic protocols? - the cases of ISO/IEC 29128 and CRYPTREC. In Financial Cryptography and Data Security, FC 2010 Workshops, RLCPS, WECSR, and WLC 2010, Tenerife, Canary Islands, Spain,, Vol. 6054 ofLNCS, pp. 182–194.
Springer, January 2010.
[71] Ralph C. Merkle. One way hash functions and DES. In Brassard [27], pp. 428–446.
[72] Silvio Micali, Kazuo Ohta, and Leonid Reyzin. Accountable-subgroup multisignatures: ex-tended abstract. In Michael K. Reiter and Pierangela Samarati, editors,ACM Conference on Computer and Communications Security, pp. 245–254. ACM, 2001.
[73] Daniele Micciancio and Bogdan Warinschi. Soundness of formal encryption in the presence of active adversaries. In Moni Naor, editor, TCC, Vol. 2951 ofLecture Notes in Computer Science, pp. 133–151. Springer, 2004.