塚田 恭章

J-GLOBALへ         更新日: 18/09/22 19:15
 
アバター
研究者氏名
塚田 恭章
 
ツカダ ヤスユキ
eメール
tsukadakanto-gakuin.ac.jp
URL
http://home.kanto-gakuin.ac.jp/~tsukada/index-j.html
所属
関東学院大学
部署
理工学部 理工学科 情報学系
職名
教授
学位
博士(工学)(東京工業大学), 理学修士(東京工業大学)

プロフィール

1988年東京工業大学理学部情報科学科卒業. 1990年同大学院理工学研究科情報科学専攻修士課程修了. 同年日本電信電話株式会社入社. 同社基礎研究所,コミュニケーション科学基礎研究所勤務を経て, 2017年より関東学院大学理工学部理工学科情報学系教授. 数理的技法によるネットワークセキュリティの研究および教育に従事. 博士(工学)(東京工業大学). 日本ソフトウェア科学会,日本応用数理学会,情報処理学会, Association for Computing Machinery (ACM) 各会員.

研究分野

 
 

経歴

 
1990年4月
 - 
1999年1月
日本電信電話(株) 基礎研究所 情報科学研究部
 
1999年1月
 - 
2000年3月
日本電信電話(株) コミュニケーション科学基礎研究所 人間情報研究部
 
2000年4月
 - 
2009年3月
日本電信電話(株) コミュニケーション科学基礎研究所 人間情報研究部 主任研究員
 
2009年4月
 - 
2010年9月
日本電信電話(株) コミュニケーション科学基礎研究所 協創情報研究部 主任研究員
 
2009年9月
 - 
2016年2月
法政大学 理工学部 応用情報工学科 兼任講師
 
2010年10月
 - 
2014年6月
日本電信電話(株) コミュニケーション科学基礎研究所 協創情報研究部 主幹研究員
 
2014年7月
 - 
2017年3月
日本電信電話(株) コミュニケーション科学基礎研究所 メディア情報研究部 主幹研究員
 
2017年4月
 - 
現在
関東学院大学 理工学部 理工学科 情報学系 教授
 
2018年4月
 - 
現在
関東学院大学 大学院工学研究科 情報学専攻 博士前期課程指導教授
 
2018年4月
 - 
現在
関東学院大学 大学院工学研究科 総合工学専攻 博士後期課程指導教授
 
2018年4月
 - 
現在
関東学院大学 大学院工学研究科 情報学専攻 主任
 

学歴

 
1984年4月
 - 
1988年3月
東京工業大学 理学部 情報科学科
 
1988年4月
 - 
1990年3月
東京工業大学 大学院理工学研究科 情報科学専攻 修士課程
 

委員歴

 
1996年6月
 - 
2000年3月
情報処理学会  学会誌編集委員
 
2001年4月
 - 
2005年3月
情報処理学会  アルゴリズム研究運営委員
 
2001年4月
 - 
2009年3月
日本ソフトウェア科学会  編集委員
 
2006年5月
 - 
2012年3月
日本応用数理学会  「数理的技法による情報セキュリティ」研究部会 幹事
 
2008年5月
 - 
2008年5月
情報処理学会  会誌「フォーマルメソッドの新潮流」特集 ゲストエディタ
 
2008年5月
 - 
2009年5月
電子情報通信学会  論文誌和文D・英文D 「フォーマルアプローチ」特集号 編集委員
 
2008年5月
 - 
2012年3月
日本応用数理学会  JSIAM Letters 編集委員
 
2008年10月
 - 
2008年10月
電子情報通信学会  ハンドブック/知識ベース委員会 『知識ベース』執筆委員
 
2008年2月
 - 
2011年3月
JST  戦略的国際科学技術協力推進事業 日本-フランス(CNRS)研究交流「計算機によって検証された安全性証明」プロジェクト 研究者
 
2009年4月
 - 
2009年4月
暗号の計算論的・記号的安全性証明に関するスプリングスクール&国際ワークショップ(CoSyProofs 2009) 運営委員
 
2012年4月
 - 
2014年6月
日本応用数理学会  理事
 
2013年5月
 - 
2014年6月
日本応用数理学会  副会長
 
2013年4月
 - 
2019年6月
日本応用数理学会  代表会員
 
 
   
 
PASSAT (IEEE/ASE International Conference on Privacy, Security, Risk, and Trust) 2010, 2011, 2012, 2013  プログラム委員
 
 
   
 
DPM (International Workshop on Data Privacy Management) 2011, 2012, 2013, 2014, 2015, 2016, 2017, 2018  プログラム委員
 
 
   
 
ICISSP (International Conference on Information Systems Security and Privacy) 2015, 2016, 2017, 2018, 2019  プログラム委員
 

論文

 
Yasuyuki Tsukada, Hideki Sakurada, Ken Mano, and Yoshifumi Manabe
Annals of Mathematics and Artificial Intelligence   78(2) 101-129   2016年10月   [査読有り]
In this paper, we exploit epistemic logic (or the modal logic of knowledge) for multiagent systems to discuss the compositionality of several privacy-related information-hiding/disclosure properties. The properties considered here are anonymity, p...
藤田邦彦, 塚田恭章
情報処理学会論文誌   55(9) 2081-2091   2014年9月   [査読有り]
近年の情報システムの複雑化やネットワーク接続の常態化に伴い,アクセス制御の必要性と複雑性も増大している.アクセス制御は,情報やコンテンツなどのオブジェクトの利用を許諾あるいは拒否する仕組みであり,諾否の基準がアクセス制御ポリシとして設定される.アクセス制御ポリシの記法は,個々のシステムや言語に特化しており,管理者はそれぞれの記法に習熟していないと,設定ミスによる情報漏洩や不正行為を引き起こす可能性がある.また,アクセス制御の結果は,従来は許諾/拒否の二値を返すものとして定義されてきたが,ア...
Kunihiko Fujita and Yasuyuki Tsukada
Computers and Electrical Engineering   38(6) 1670-1686   2012年11月   [査読有り]
With recent advances in information and telecommunications technologies, a large range of digital content is distributed over the Internet. Whereas diverse licenses are provided to protect the content legally and have the advantage of offering aut...
河辺義信, 真野健, 櫻田英樹, 塚田恭章
情報処理学会論文誌   52(9) 2549-2561   2011年9月   [査読有り]
電子投票システムの満たすべき性質に,無証拠性が挙げられる.これは匿名性の拡張で,「プロトコルを観測して得られる情報に加えて,別の付加的な情報を投票者が外部に与えたとしても,ある投票パターンと別の(結果が同じとなる)投票パターンが区別できない」という性質である.本稿では,Leeらの電子投票プロトコルを題材とし,その無証拠性を定理証明器で形式的に検証する.
Yasuyuki Tsukada, Ken Mano, Hideki Sakurada, and Yoshinobu Kawabe
Transactions on Data Privacy   3(3) 177-198   2010年12月   [査読有り]
In this paper, we propose a taxonomy of privacy-related information-hiding/disclosure properties in terms of the modal logic of knowledge for multiagent systems. The properties considered here are anonymity, privacy, onymity, and identity. Intuiti...
Ken Mano, Yoshinobu Kawabe, Hideki Sakurada, and Yasuyuki Tsukada
Journal of Logic and Computation   20(6) 1251-1288   2010年12月   [査読有り]
We propose a new information-hiding property called role interchangeability for the verification of the anonymity and privacy of security protocols. First we formally specify the new property in multiagent systems, and describe its relationship wi...
藤田邦彦, 塚田恭章
情報処理学会論文誌   49(9) 3165-3179   2008年9月   [査読有り]
近年のコンテンツ流通環境においては,コンテンツの鑑賞だけでなく,その二次利用や再配信等への要求が高まっている.このような要求を支援するために,ライセンスの付与を容易に行える法的な枠組みを提供するプロジェクトがクリエイティブ・コモンズである.クリエイティブ・コモンズでは,ライセンス付与の条件を利用許諾という文書にまとめているが,自然言語で記述されているため,ライセンス付与に関連する処理の自動化等は困難であった.そこで我々は,利用許諾を多種論理を用いて定式化し,厳密な形式意味論を与えた.これに...
Yoshinobu Kawabe, Ken Mano, Hideki Sakurada, and Yasuyuki Tsukada
IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences   E91-A(9) 2597-2606   2008年9月   [査読有り]
Many Internet services and protocols should guarantee anonymity; for example, an electronic voting system should guarantee to prevent the disclosure of who voted for which candidate. To prove trace anonymity, which is an extension of the formulati...
Yoshinobu Kawabe, Ken Mano, Hideki Sakurada, and Yasuyuki Tsukada
Information Processing Letters   101(1) 46-51   2007年1月   [査読有り]
This paper presents an inductive method for verifying the anonymity of distributed systems with a theorem prover. We employ an I/O-automaton to describe a distributed, possibly infinite-state, system. We first extend the formulation of anonymity b...
塚田恭章
情報処理学会論文誌   46(1) 236-246   2005年1月   [査読有り]
悪性プログラムから計算機を守るためプログラム本体とそれが正しく安全に動作することの数学的証明を同時に流通させる方式(Proof-Carrying Code)が近年提案され,電子署名に基づく現行方式より高い安全性を保証する新技術として期待が集まっている.この方式の課題であった証明サイズの爆発の問題も,対話的・確率的手法に基づく効率的な証明検証技法を応用した対話型安全性証明つきプログラム配信方式の適用により対処できる.しかし,証明をそのまま流通させることは証明の盗用や悪用(たとえば証明を利用し...
Yasuyuki Tsukada
Automated Software Engineering   12(2) 237-257   2005年4月   [査読有り]
This paper proposes a new proof-based approach to safe evolution of distributed software systems. Specifically, it extends the simple certification mechanism of proof-carrying code (PCC) to make it interactive and probabilistic, thereby devising i...
Yasuyuki Tsukada
International Journal of Foundations of Computer Science   12(1) 31-67   2001年2月   [査読有り]
This paper treats Martin-Löf's type theory as an open-ended framework composed of (i) flexibly extensible languages into which various forms of objects and types can be incorporated, (ii) their uniform, effectively given semantics, and (iii) persi...
International Journal of Foundations of Computer Science   12(5) 695   2001年10月
The paper, Martin-Löf's type theory as an open-ended framework, by Yasuyuki Tsukada, published in Vol. 12, No. 1 (2001) 31-67, had several incorrect "=3D" characters scattered throughout the text. A corrected version of this paper will appear on t...
Ken Mano, Hideki Sakurada, and Yasuyuki Tsukada
Trust Management XI: Proceedings of the 11th IFIP WG 11.11 International Conference on Trust Management (IFIPTM 2017), IFIP Advances in Information and Communication Technology (IFIP AICT) Book Series (Springer)   505 135-151   2017年6月   [査読有り]
We present a mathematical formulation of a trust metric using a quality and quantity pair. Under a certain assumption, we regard trust as an additive value and define the soundness of a trust computation as not to exceed the total sum. Moreover, w...
Yasuyuki Tsukada, Hideki Sakurada, Ken Mano, and Yoshifumi Manabe
Proceedings of the Fourteenth Conference on Theoretical Aspects of Rationality and Knowledge (TARK 2013)   239-248   2013年1月   [査読有り]
In this paper, we present an epistemic logic approach to the compositionality of several privacy-related information-hiding/disclosure properties. The properties considered here are anonymity, privacy, onymity, and identity. Our initial observatio...
Kunihiko Fujita and Yasuyuki Tsukada
Proceedings of the Tenth Annual ACM Workshop on Digital Rights Management (ACM-DRM 2010)   61-72   2010年10月   [査読有り]
The emergence of different licenses has led to problems with the smooth flow of digital content across them. To activate digital content distribution, license interoperability must be revealed. In this paper, we present a framework for formally ex...
Kunihiko Fujita and Yasuyuki Tsukada
Proceedings of the Fifth International Workshop on Data Privacy Management (DPM 2010), Lecture Notes in Computer Science (Springer)   6514 140-154   2011年2月   [査読有り]
New security and privacy enhancing technologies are demanded in the new information and communication environments where a huge number of computers interact with each other in a distributed and ad hoc manner to access various resources. In this pa...
A formal approach to interoperability between licenses for content protection
Kunihiko Fujita, Hiroki Endo, and Yasuyuki Tsukada
Short Papers Proceedings of the Fourth International Workshop on Security (IWSEC 2009) [ISBN 978-4-915256-76-9]   81-98   2009年10月   [査読有り]
The emergence of different licenses has led to problems with the smooth flow of digital content across different licenses. To activate digital content distribution, license interoperability must be revealed. In this paper, we present a framework f...
Yasuyuki Tsukada, Ken Mano, Hideki Sakurada, and Yoshinobu Kawabe
Proceedings of the 2009 IEEE International Conference on Privacy, Security, Risk and Trust (PASSAT-09) (IEEE Computer Society Press)   42-51   2009年8月   [査読有り]
In this paper, we propose a taxonomy of privacy-related information-hiding/disclosure properties in terms of the modal logic of knowledge for multiagent systems. The properties considered here are anonymity, privacy, onymity, and identity. Intuiti...
Backward simulations for anonymity
Yoshinobu Kawabe, Ken Mano, Hideki Sakurada, and Yasuyuki Tsukada
Sixth IFIP WG 1.7, GI FoMSESS Workshop on Issues in the Theory of Security (WITS '06)   206-220   2006年3月   [査読有り]
There are many services and protocols on the Internet where anonymity should be provided. For example, an electronic voting system should guarantee to prevent the disclosure of who voted for which candidate. To prove trace anonymity, which is an e...
A role-based specification of the SET payment transaction protocol
Hideki Sakurada and Yasuyuki Tsukada
Advances in Network and Distributed Systems Security, IFIP TC11 WG11.4 First Annual Working Conference on Network Security (Kluwer Academic Publishers)   1-13   2001年11月   [査読有り]
In this paper, we define a language for specifying security protocols concisely and unambiguously. We use this language to formally specify the protocol for payment transactions in Secure Electronic Transaction (SET), which has been developed by V...
Yasuyuki Tsukada
2000 International Symposium on Principles of Software Evolution (IEEE Computer Society Press)   23-27   2001年2月   [査読有り]
This paper proposes a new proof-based approach to safe evolution of distributed software systems. Specifically, it extends the simple certification mechanism of proof-carrying code (PCC) to make it interactive and probabilistic, thereby devising c...
Type-free equational reasoning in the theory of inductively defined types
Yasuyuki Tsukada
Third Fuji International Symposium on Functional and Logic Programming (World Scientific)   227-246   1998年4月   [査読有り]
In this paper the semantics of inductively defined types in terms of partial equivalence relations is shown to be complete with respect to a coinductively defined, bisimulation-like program equivalence. Using this result in reasoning about objects...

書籍等出版物

 
数理的技法による安全性証明 [太田和夫, 盛合志帆 (編), 電子情報通信学会知識ベース, 1群 3編 (暗号理論)]
塚田恭章 (担当:分担執筆, 範囲:10章)
電子情報通信学会   2010年8月   
数理的技法による情報セキュリティ, 日本応用数理学会監修, シリーズ応用数理, 第1巻
萩谷昌己, 塚田恭章 (担当:共編者)
共立出版   2010年7月   ISBN:978-4-320-01950-8
ゲーム列による安全性証明の形式化と自動化-確率Hoare論理と確率プロセス計算によるアプローチ [萩谷昌己, 塚田恭章 (編), 数理的技法による情報セキュリティ, 日本応用数理学会監修, シリーズ応用数理, 第1巻]
真野健, 櫻田英樹, 河辺義信, 塚田恭章 (担当:分担執筆, 範囲:第4章 (pp. 65-86))
共立出版   2010年7月   

Misc

 
藤田邦彦, 塚田恭章
文京学院大学 総合研究所 経営論集   26(1) 13-21   2016年12月
医療従事者に対して患者が医療情報の利用を許諾するというアクセス制御モデルを提案する.本モデルでは,利用許諾は多種一階述語論理の枠組みで記述され,アクセス権の設定の妥当性を,対応する利用許諾の互換性の有無により厳密に判定できる.
塚田恭章, 真野健, 櫻田英樹
NTT技術ジャーナル   23(9) 22-25   2011年9月
電子商取引・電子政府・電子医療などのサービスを提供するICTシステムから,重要な個人情報やプライバシ情報が漏洩しないことを,フォーマルメソッド(形式手法,数理的技法)を用いて厳密に証明する手法について解説します.
真野健, 櫻田英樹, 河辺義信, 塚田恭章
応用数理   17(4) 38-46   2007年12月
Recently extensive research has been undertaken on the computational foundations of symbolic proof methods for security protocols. There are two approaches to providing such foundations. One is to give a probabilistic re-interpretation to existing...
塚田恭章, 真野健, 河辺義信, 櫻田英樹
NTT技術ジャーナル   19(6) 38-40   2007年6月
電子投票や電子オークションなどで用いられるセキュリティプロトコルが,匿名性(「誰が」の情報が漏洩しないこと)やプライバシ(「何をした」の情報が漏洩しないこと)に関する要件を正しく実現できているかどうかを,数理論理学・計算機科学の手法を駆使して厳密に検証する技術を紹介します.
安全なモバイルプログラム方式の理論
塚田恭章
NTT R&D   51(10) 765-771   2002年10月
ネットワークの発展に伴い大量のプログラムが流通する時代を迎え,破壊的な外部プログラムから計算機を守る新しい技術が必要になっている.近年,プログラム本体とそれが安全に動作することの数学的証明を同時に流通させる方式が提案され,電子署名に基づく現行技術の問題点を解決した革新的技術として期待が集まっている.しかし,一般に安全性証明はプログラムに比べて巨大になるため,安全性が効率的に検証可能となるプログラムには理論的限界が存在する.この限界を打破するため,証明それ自体を流通させる代わりに簡単な通信に...
塚田恭章
応用数理   24(2) 1   2014年6月
Akiko Orita, Ken Mano, and Yasuyuki Tsukada
A terminology for talking about privacy by data minimization: Anonymity, Unlinkability, Undetectability, Unobservability, Pseudonymity, and Identity Management, Version v0.34   74-78   2010年8月
塚田恭章
情報処理   49(5) 491-492   2008年5月
塚田恭章
応用数理   17(1) 85-86   2007年3月

講演・口頭発表等

 
質と量の組を用いたトラストの多値拡張
真野健, 櫻田英樹, 塚田恭章
コンピュータセキュリティシンポジウム2016 論文集 (情報処理学会), Vol. 2016, No. 2, pp. 1153-1160   2016年10月   
CSS2015において我々は,質と量の組を用いたトラストとその合成演算を定式化し,基本性質を証明した.また,トラスト計算プロトコルを提案し,その基本性質を用いてその正しさを示した.本稿では,同様な議論が適用可能な定式化のバリエーションのひとつとして,質の多値化を考える.多値論理を援用することで,2値の場合の同様に多値化されたトラスト計算の正しさを証明できる.
質と量の組を用いたトラストの定式化
真野健, 櫻田英樹, 塚田恭章
コンピュータセキュリティシンポジウム2015 論文集 (情報処理学会), Vol. 2015, No. 3, pp. 755-762   2015年10月   
質と量の組を用いてトラストを定量的に定式化する.ある仮定のもと,トラストを加法性を持つ値として捉え,その総和を超えないことをトラスト計算の健全性と定める.また,個々のトラスト計算の結果が健全であることだけでなく,計算手続きがトラストの付値の変化に対して安定であることの重要性も指摘する.そのような問題設定のもと,さまざまなトラスト合成演算を定義し,それを用いたトラスト計算プロトコルの健全性と安定性を証明する.さらに,プロトコルのプライバシ強化についても考察する.

特許

 
特開2017-59975 : トラスト計算装置, トラスト計算方法, およびプログラム
真野健, 櫻田英樹, 塚田恭章
特開2007-157021 : 耐タンパ証明携帯プログラム配信システム及びその方法
塚田恭章
特開2007-148624 : トレース等価性を基準とした役割交換可能性を用いた匿名性検査方法, その装置, そのプログラム
真野健, 河辺義信, 櫻田英樹, 塚田恭章
特開2007-66184 : 秘匿性検査装置及び秘匿性検査方法
櫻田英樹, 河辺義信, 真野健, 塚田恭章
特開2006-293633 : 匿名性検査装置, 方法, プログラム及び記録媒体
河辺義信, 真野健, 櫻田英樹, 塚田恭章
特開2006-197323 : 証明携帯プログラム配信方法および証明携帯プログラム配信システム
塚田恭章
特開2000-78126 : 対話型証明つき移動コード送受信システムおよび方法と対話型証明つき移動コード送受信プログラムを記録した記録媒体
塚田恭章

受賞

 
2005年10月
情報処理学会 CSS 2005 (Computer Security Symposium 2005) 優秀論文賞 シミュレーション技法によるセキュリティプロトコルの匿名性検証法
受賞者: 河辺義信,真野健,櫻田英樹,塚田恭章