• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

On Verifying Anonymity of Security Protocols with Formal Methods

Research Project

Project/Area Number 19700018
Research Category

Grant-in-Aid for Young Scientists (B)

Allocation TypeSingle-year Grants
Research Field Fundamental theory of informatics
Research InstitutionAichi Institute of Technology (2008-2009)
NTT Communication Science Laboratories (2007)

Principal Investigator

KAWABE Yoshinobu  Aichi Institute of Technology, 情報科学部, 准教授 (80396184)

Project Period (FY) 2007 – 2009
Project Status Completed (Fiscal Year 2009)
Budget Amount *help
¥3,380,000 (Direct Cost: ¥2,900,000、Indirect Cost: ¥480,000)
Fiscal Year 2009: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2008: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2007: ¥1,300,000 (Direct Cost: ¥1,300,000)
Keywords暗号系 / セキュリティ検証 / 匿名性 / フォーマルメソッド / 定理証明 / 形式検証 / I / O-オートマトン / 0-オートマトン
Research Abstract

This study proposed a new method to prove the anonymity of security protocols. We employ a formal method ; specifically, we extended our "anonymous simulation method"to deal with probabilistic protocols and stronger adversaries. In this study, we demonstrated the anonymity verification for Crowds. Also, we proved the receipt-freeness property of an e-voting protocol.

Report

(4 results)
  • 2009 Annual Research Report   Final Research Report ( PDF )
  • 2008 Annual Research Report
  • 2007 Annual Research Report
  • Research Products

    (21 results)

All 2010 2009 2008 2007 Other

All Journal Article (6 results) (of which Peer Reviewed: 6 results) Presentation (11 results) Remarks (4 results)

  • [Journal Article] Probabilistic anomymity via coalgebraic simulations2010

    • Author(s)
      Ichiro Hasuo, Yoshinobu Kawabe, Hideki Sakurada
    • Journal Title

      Theoretical Computer Science volume411,No.22-24

      Pages: 2239-2259

    • Related Report
      2009 Final Research Report
    • Peer Reviewed
  • [Journal Article] Probabilistic Anonymity via Coalgebraic Simulations2010

    • Author(s)
      I.Hasuo, Y.Kawabe, H.Sakurada
    • Journal Title

      Theoretical Computer Science 411

      Pages: 2239-2259

    • NAID

      120002511338

    • Related Report
      2009 Annual Research Report
    • Peer Reviewed
  • [Journal Article] On backward-style anonymity verification2008

    • Author(s)
      Yoshinobu Kawabe, Ken Mano, Hideki Sakurada, Yasuyuki Tsukada
    • Journal Title

      IEICE Transactions volumeE91-A,No.9

      Pages: 2597-2606

    • NAID

      10026851999

    • Related Report
      2009 Final Research Report
    • Peer Reviewed
  • [Journal Article] An adversary model for simulation-based anonymity proof2008

    • Author(s)
      Yoshinobu Kawabe, Hideki Sakurada
    • Journal Title

      IEICE Transactions volumeE91-A,No.4

      Pages: 1112-1120

    • NAID

      10026848731

    • Related Report
      2009 Final Research Report
    • Peer Reviewed
  • [Journal Article] On backward-style anonymity verification2008

    • Author(s)
      Y. Kawabe, K. Mano, H. Sakurada, Y. Tsukada
    • Journal Title

      IEICE Trans. Vol.E91A, No.9

      Pages: 2597-2606

    • NAID

      10026851999

    • Related Report
      2008 Annual Research Report
    • Peer Reviewed
  • [Journal Article] An adversary model for simulation-based anonymity proof2008

    • Author(s)
      Y.Kawabe, H.Sakurada
    • Journal Title

      IEICE Trans. Vol.E91A,No.4

      Pages: 1112-1120

    • NAID

      10026848731

    • Related Report
      2007 Annual Research Report
    • Peer Reviewed
  • [Presentation] 無証拠的プロトコルのフォーマルな記述について2009

    • Author(s)
      河辺義信
    • Organizer
      第21回電気関係学会東海支部連合大会
    • Place of Presentation
      愛知県豊田市
    • Year and Date
      2009-09-11
    • Related Report
      2009 Final Research Report
  • [Presentation] 無証拠的プロトコルのフォーマルな扱いについて2009

    • Author(s)
      河辺義信
    • Organizer
      第21回 電気関係学会東海支部連合大会
    • Place of Presentation
      愛知工業大学
    • Year and Date
      2009-09-10
    • Related Report
      2009 Annual Research Report
  • [Presentation] Anonymity, privacy, onymity and identity: a modal logic approach2009

    • Author(s)
      Yasuyuki Tsukada, Ken Mano, Hideki Sakurada, Yoshinobu Kawabe
    • Organizer
      IEEE International Conference on Privacy, Security, Risk and Trust (PASSAT-09)
    • Place of Presentation
      カナダ・バンクーバー市
    • Year and Date
      2009-08-29
    • Related Report
      2009 Final Research Report
  • [Presentation] I/O-オートマトンによる無証拠性の形式化について2009

    • Author(s)
      河辺義信, 真野健, 櫻田英樹, 塚田恭章
    • Organizer
      電子情報通信学会2009年暗号と情報セキュリティシンポジウム
    • Place of Presentation
      滋賀県大津市
    • Year and Date
      2009-01-23
    • Related Report
      2009 Final Research Report
  • [Presentation] 1/0-オートマトンによる無証拠性の形式化について2009

    • Author(s)
      河辺, 真野, 櫻田, 塚田
    • Organizer
      電子情報通信学会2009年暗号と情報セキュリティシンポジウム
    • Place of Presentation
      大津プリンスホテル(滋賀県大津市)
    • Year and Date
      2009-01-23
    • Related Report
      2008 Annual Research Report
  • [Presentation] 匿名性・プライバシ・顕名性・アイデンティティへの知識論理的アプローチ2008

    • Author(s)
      塚田恭章, 真野健, 櫻田英樹, 河辺義信
    • Organizer
      情報処理学会第11回コンピュータセキュリティシンポジウム
    • Place of Presentation
      沖縄県宜野湾市
    • Year and Date
      2008-10-08
    • Related Report
      2009 Final Research Report
  • [Presentation] 能動的な攻撃者が存在するシステムに対する匿名性の検証について2008

    • Author(s)
      河辺義信, 真野健, 櫻田英樹, 塚田恭章
    • Organizer
      電子情報通信学会2008年暗号と情報セキュリティシンポジウム
    • Place of Presentation
      宮崎県宮崎市
    • Year and Date
      2008-01-23
    • Related Report
      2009 Final Research Report
  • [Presentation] 能動的な攻撃者が存在するシステムに対する匿名性の検証について2008

    • Author(s)
      河辺, 真野, 櫻田, 塚田
    • Organizer
      電子情報通信学会2008年暗号と情報セキュリティシンポジウム
    • Place of Presentation
      宮崎シーガイアコンベンションセンター・サミット
    • Year and Date
      2008-01-23
    • Related Report
      2007 Annual Research Report
  • [Presentation] A formal approach to designing anonymous software2007

    • Author(s)
      Yoshinobu Kawabe, Hideki Sakurada
    • Organizer
      5th International Conference on Software Engineering Research, Management and Applications (SERA '07)
    • Place of Presentation
      韓国釜山市
    • Year and Date
      2007-08-21
    • Related Report
      2009 Final Research Report
  • [Presentation] A formal approach to designing anonymous software2007

    • Author(s)
      Y.Kawabe, H.Sakurada
    • Organizer
      5th International Conference on Software Engineering Research, Management and Applications (SERA'07)
    • Place of Presentation
      ヘウンデ・グランドホテル(韓国釜山市)
    • Year and Date
      2007-08-21
    • Related Report
      2007 Annual Research Report
  • [Presentation] 攻撃者を考慮した匿名性検証法2007

    • Author(s)
      河辺義信, 櫻田英樹
    • Organizer
      電子情報通信学会第20回回路とシステム軽井沢ワークショップ
    • Place of Presentation
      長野県軽井沢町
    • Year and Date
      2007-04-23
    • Related Report
      2009 Final Research Report
  • [Remarks] 研究代表者のウェブページ. ここでは, Lee電子投票の無証拠性の証明スクリプト(バッチファイルのようなもの)を公開している. 用いた定理証明器は, LP(Larch Prover)である

    • URL

      http://aitech.ac.jp/~kawabe/

    • Related Report
      2009 Final Research Report
  • [Remarks]

    • URL

      http://aitech.ac.jp/~kawabe/

    • Related Report
      2009 Annual Research Report
  • [Remarks]

    • URL

      http://aitech.ac.jp/~kawabe/

    • Related Report
      2008 Annual Research Report
  • [Remarks]

    • URL

      http://www.brl.ntt.co.jp/cs/ninri-g/security/index-j.html

    • Related Report
      2007 Annual Research Report

URL: 

Published: 2007-04-01   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi