米崎 直樹 Yonezaki Naoki

ID:1000000126286

東京工業大学大学院情報理工学研究科 Graduate School of Information Science and Engineering, Tokyo Institute of Technology (2015年 CiNii収録論文より)

同姓同名の著者を検索

論文一覧:  55件中 1-20 を表示

  • 1 / 3
  • 環境許容性のあるリアクティブシステム合成法 (ソフトウェアサイエンス)

    上野 篤史 , 冨田 尭 , 島川 昌也 [他] , 萩原 茂樹 , 米崎 直樹

    形式的に記述された仕様からリアクティブシステム(RS)を自動合成する手法では,仕様<ψ_<sys>を満たす振る舞いをするRSが制約ψ_<env>に従う環境からの入力を想定する場合,ψ_<env>→ψ_<sys>の形で仕様が記述される.この仕様からは,環境から_ψ<ψenv>を満たさない想定外の入力に対してどのような振る舞いをしても良 …

    電子情報通信学会技術研究報告 = IEICE technical report : 信学技報 114(510), 7-12, 2015-03-09

  • リアクティブシステム仕様の極小強充足不能部分計算に関する考察

    萩原 茂樹 , 江川 直毅 , 島川 昌也 , 米崎 直樹

    組み込みシステムなど,環境と相互にやりとりを行うリアクティブシステムは,社会インフラとしていたるところで用いられており,リアクティブシステムを誤りなく構成することが不可欠である.そのためには,リアクティブシステムの仕様に誤りがあってはならない.リアクティブシステム仕様には,実現可能性(プログラム化可能性)が強く求められる.もし,実現不可能である場合,仕様を修正する必要がある.仕様のどの部分に誤りが …

    情報処理学会論文誌プログラミング(PRO) 7(5), 11-11, 2014-12-05

    情報処理学会

  • D-3-2 実現可能性判定を高速化するための仕様の特徴量に基づいた仕様分割手法(D-3.ソフトウェアサイエンス,一般セッション)

    長利 健治 , 萩原 茂樹 , 米崎 直樹

    電子情報通信学会総合大会講演論文集 2014年_情報・システム(1), 17, 2014-03-04

  • 紛失通信プロトコルの解析のための可能世界意味論に基づく形式体系

    小黒博昭 , 萩原茂樹 , 米崎直樹

    著者らはこれまでに、暗号プロトコルの基本要素としてよく<br />利用される1-out-of-2型の紛失通信プロトコルに着目し、<br />同プロトコルの一実現形態であるEGL85プロトコルの性質を<br />記号論的に解析するための形式体系を提案している。<br />しかしながら、従来の形式体系には構文に対する直観的な<br />意味し …

    全国大会講演論文集 2011(1), 439-441, 2011-03-02

    情報処理学会

  • 記号論的暗号解析を用いた Oblivious Transfer プロトコルの解析

    小黒 博昭 , 萩原 茂樹 , 米崎 直樹

    BheryらはDolev-Yaoの記号論的な手法をもとに,暗号文から得られる部分情報を推論可能な演繹体系(Judgment-Deduction System, JD体系)を提案している.しかし,従来のJD体系は, Oblivious Transfer (OT,紛失通信)プロトコルに対し, OTが満足すべき性質を検証するための記述能力を保持していなかった.本論文では, OTの性質を検証可能な形式体系 …

    電子情報通信学会論文誌. D, 情報・システム = The IEICE transactions on information and systems (Japanese edition) 92(5), 596-607, 2009-05-01

    参考文献12件

  • 形式オントロジーに基づく遺伝子調節のための数値モデル

    秋山 卓見 , 泉 直子 , 萩原 茂樹 [他] , 米崎 直樹

    近年の分子生物学の進展の中において,遺伝子ノックダウン実験による遺伝子調節ネットワークの解明が進んでいる.本研究では,それらを計算論的モデルを用いて捉えなおし,形式手法を反映したかたちで解析したすなわち,化学反応の活性/抑制関係を表現した,資源の取り合いを基本概念とする意味論を持つ形式オントロジーの公理を満たす,遺伝子調節量を表す数値間の演算の代数的制約と,そのインスタンスとなる関数を提案した.ま …

    情報処理学会研究報告バイオ情報学(BIO) 2007(21(2007-BIO-008)), 71-78, 2007-03-05

    情報処理学会 参考文献6件

  • 記号論及び計算論によるセキュリティ解析の相互関係(<特集>数理的技法による情報セキュリティ)

    萩原 茂樹 , 米崎 直樹

    暗号プロトコルの解析は,確率的多項式時間チューリング機械を用いる計算論的手法と,Dolev-Yaoモデルに基づく記号論的手法がそれぞれ独立に研究されてきた.記号論による解析は,抽象レベルの解析とみなせ簡潔で分かりやすい一方,記号論による解析結果と計算論による解析結果の対応が明らかでなかった.この問題に対してAbadiとRogawayは,完全な対称鍵暗号方式を前提としてメッセージの見た目の等価性を記 …

    応用数理 17(4), 291-301, 2007

    CiNii 外部リンク J-STAGE 参考文献10件

  • 安全性を保証する構造要件に基づくセキュリティプロトコルの自動生成法

    佐藤 直人 , 萩原 茂樹 , 米崎 直樹

    近年のインターネット上での重要な取引の増加に伴い、安全なプロトコルが必要不可欠となっているが、検証による安全性保証の限界を考えると、安全なプロトコルを自動生成することが望ましい。本稿では二者間データ通信のためのセキュリティプロトコル自動生成法を提案する。これは、プロトコルの構造から安全性を導出する推論規則を利用し、安全なプロトコルのみを生成する手法である。また、プロトコルに対するコスト評価を行うこ …

    情報処理学会研究報告マルチメディア通信と分散処理(DPS) 2005(33(2004-DPS-122)), 157-162, 2005-03-22

    情報処理学会 参考文献5件

  • 安全性を保証する構造要件に基づくセキュリティプロトコルの自動生成法

    佐藤 直人 , 萩原 茂樹 , 米崎 直樹

    近年のインターネット上での重要な取引の増加に伴い、安全なプロトコルが必要不可欠となっているが、検証による安全性保証の限界を考えると、安全なプロトコルを自動生成することが望ましい。本稿では二者間データ通信のためのセキュリティプロトコル自動生成法を提案する。これは、プロトコルの構造から安全性を導出する推論規則を利用し、安全なプロトコルのみを生成する手法である。また、プロトコルに対するコスト評価を行うこ …

    情報処理学会研究報告コンピュータセキュリティ(CSEC) 2005(33(2004-CSEC-028)), 157-162, 2005-03-22

    情報処理学会

  • 20周年記念特集号の編集にあたって(<特集>20周年記念特集)

    米崎 直樹

    コンピュータソフトウェア = Computer software 20(6), 533, 2003-11-26

    CiNii 外部リンク 機関リポジトリ

  • 演繹体系による暗号方式の形式化と体系の性質としての暗号方式の安全性

    AshrafMoustafaBHERY , 萩原 茂樹 , 米崎 直樹

    非対称暗号方式など、暗号方式の特徴やその安全性は、確率理論や計算量理論を用いてこれまで盛んに研究されてきた。本稿では、理想化された非対称暗号方式を形式化可能なJDE体系と呼ぶ演繹体系を提案する。この演繹体系を用いることにより、様々な非対称暗号方式の類似した安全性を統一的に取り扱うことが可能となる。本稿では、安全性を表現するためにいくつか新しいアイデアを導入した。まず、content-of等いくつか …

    情報処理学会研究報告コンピュータセキュリティ(CSEC) 2003(74(2003-CSEC-022)), 31-37, 2003-07-17

    情報処理学会 参考文献17件

  • 演繹体系による暗号方式の形式化と体系の性質としての暗号方式の安全性

    Bhery Ashraf Moustafa , 萩原 茂樹 , 米崎 直樹

    非対称暗号方式等、暗号方式の特徴やその安全性は、確率理論や計算量理論を用いてこれまで盛んに研究されてきた。本稿では、理想化された非対称暗号方式を形式化可能なJDE体系と呼ぶ演繹体系を提案する。この演繹体系を用いることにより、様々な非対称暗号方式の類似した安全性を統一的に取り扱うことが可能となる。本稿では、安全性を表現するためにいくつか新しいアイデアを導入した。まず、content-of等いくつか関 …

    電子情報通信学会技術研究報告. ISEC, 情報セキュリティ 103(195), 31-37, 2003-07-10

    参考文献17件

  • SSLとリレーサーバを用いたPOP before SMTPのセキュアな実現法

    増井 健司 , 友石 正彦 , 米崎 直樹

    電子メールの送信時にユーザ認証を行うために,SMTP接続の前にPOPによるユーザ認証を要求する,POP before SMTPと呼ばれる方式がRFC2476において提案され,これを採用するサイトが増えている.しかし,POPサーバを非武装地帯で運用することは,外部からの攻撃を受けやすく危険性が高い.そこで,POPサーバをファイアウォールで保護するために,ゲートウェイヘのPOP接続をサイト内側のPOP …

    電子情報通信学会論文誌. D-I, 情報・システム, I-情報処理 = The transactions of the Institute of Electronics, Information and Communication Engineers. D-I 86(4), 260-268, 2003-04-01

    参考文献13件

  • Spi計算の型付けによる公開鍵暗号方式を用いたプロトコルのメッセージ認証の検証

    畑山 研 , 萩原 茂樹 , 米崎 直樹

    これまでに、Gordonらにより、Spi計算に型付けを行うことにより、対称鍵暗号を用いるセキュリティプロトコルのメッセージ認証を検証する手法が提案されている。しかし、公開鍵暗号系を用いるプロトコルについては明らかではなかった。本稿ではそのようなプロトコルのメッセージ認証を検証する手法について報告する。公開鍵を用いるプロトコルでは、認証者が、相手を認証するために、最初に意図した相手のみに読めるように …

    情報処理学会研究報告コンピュータセキュリティ(CSEC) 2002(43(2002-CSEC-017)), 25-30, 2002-05-23

    情報処理学会 参考文献5件

  • リアクティブシステムの段階的充足可能性と Safety Property の関係

    吉浦 紀晃 , 米崎 直樹

    時相論理で記述されたリアクティブシステムの仕様から、その仕様を満たすリアクティブシステムが存在するかどうかを判定することができる。また、その実現可能性に関しては様々な性質が提案されている。ここで提案されている実現可能性は、実際のリアクティブシステムにとっては、強すぎる性質である。一方、段階的充足可能性は、実際のリアクティブシステムが満たすべき性質に最も近いものであると考えられる。Safety Pr …

    電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス 100(570), 9-15, 2001-01-16

    参考文献20件

  • ソフトウェア発展と検証技術の未来 (特集 ソフトウェア発展)

    萩谷 昌己 , 米崎 直樹

    Bit 32(12), 3-8, 2000-12

    被引用文献3件

  • セキュリティプロトコルにおける暗号化メッセージの送信者による認知に関する検証法

    根岸 和義 , 米崎 直樹

    メッセージの認証の検証において,受信者が受信メッセージを全体として認証していても,その中の公開キーあるいは受信者の秘密キーにより暗号化された部分メッセージを送信者自身が暗号化して送信したかどうかを知ることは出来ない.我々はこの問題を解決するために以下のアイデアを提案する.(1)同一のメッセージの複数の出現の間に優先順序のあるプロトコルのみを対象とする.(2)セキュリティプロトコルの解析において,送 …

    情報処理学会研究報告コンピュータセキュリティ(CSEC) 2000(80(2000-CSEC-011)), 25-30, 2000-09-08

    情報処理学会 参考文献9件

  • セキュリティプロトコルの一貫性および正常終了一致の同一参加者による複数セッションを考慮した検証法

    根岸 和義 , 米崎 直樹

    従来のセキュリティプロトコルの検証では,(1)すり替えられることなくメッセージを伝達する,(2)秘密を保持する,ことの2点を検証することが一般的である.ただし,この中で考慮される攻撃のパターンでは,同一参加者の複数セッション間におけるプロトコルの,同一部分メッセージどうしのすり替えが考慮されていなかった.本論文ではこのような攻撃を考慮した一貫性の検証方法を与え,さらに,そこで用いられる推論規則の健 …

    情報処理学会論文誌 41(8), 2281-2290, 2000-08-15

    情報処理学会 参考文献10件 被引用文献1件

  • オブジェクトの項表現を意味論の基礎とする論理体系としてのOntologyとその表現力

    泉 直子 , 米崎 直樹

    人工知能学会全国大会論文集 = Proceedings of the Annual Conference of JSAI 14, 514-517, 2000-07-03

    参考文献7件

  • セキュリティプロトコルの一貫性および正常終了一致の検証法

    根岸 和義 , 米崎 直樹

    従来のセキュリティプロトコルの検証では,(1)すり替えられることなくメッセージを伝達する,(2)秘密を保持する,ことの2点を検証することが一般的である.ただし,この中で考慮される攻撃のパターンでは,同一参加者の複数セッション間におけるプロトコルの,同一部分メッセージ同士のすり替えが考慮されていなかった.本論文ではこのような攻撃を考慮した一貫性の検証方法を与え,さらに,そこで用いられる推論規則の健全 …

    情報処理学会研究報告コンピュータセキュリティ(CSEC) 2000(30(1999-CSEC-008)), 37-42, 2000-03-21

    情報処理学会

  • 1 / 3

ページトップへ