イベント順序証明システムの正当性の形式的証明
スポンサーリンク
概要
- 論文の詳細を見る
本稿では,NTTで開発した単一攻撃点のないイベント順序証明システムのモデルの基本的な性質の証明についてのべる.このモデルはインクリメンタルなMerkle木の構成に基づくものであり,その(1)完全化および(2)インクリメンタルなサニティチェックの正当性を示す.証明は主として定理証明系MONAを用いて構成しており,特に(2)インクリメンタルなサニティチェックの正当性については本稿で初めて証明を与えた.
- 社団法人電子情報通信学会の論文
- 2004-12-10
著者
-
小野 諭
Ntt情報流通プラットフォーム研究所
-
小野 諭
Nttソフトウェア研究所
-
小野 諭
日本電信電話株式会社
-
小川 瑞史
北陸先端科学技術大学院大学
-
小川 瑞史
Ntt
-
堀田 英一
NTT情報流通プラットフォーム研究所
-
堀田 英一
日本電信電話株式会社NTT情報流通プラットフォーム研究所
-
小川 瑞史
Ntt ソフトウェア研究所
関連論文
- QoS 制御技術の統合化方式とその効果
- モデル検査技術を利用したプログラム解析器の生成ツール
- イベント順序証明システムの正当性の形式的証明
- 抽象実行 そのフレームワークと実例(その3)
- 抽象実行 そのフレームワークと実例(その2)
- 抽象解釈におけるLazyな抽象領域の生成
- 抽象実行 そのフレームワークと実例(その1)
- 最小不動点計算に基づくプログラムの帰納的性質の導出 (並列処理)
- 広域データフロー解析に基づく関数型プログラムの変則性検出
- さきがけ「機能と構成」研究1 : 効率的で正しいプログラムの自動生成
- ASIA-PEPM 2002/FLOPS 2002参加報告
- 利得の最適連想規則を求める線形時間アルゴリズムの導出
- 最大重み和問題の線形時間アルゴリズムの導出
- ACM PLI 2000会議報告
- ナップサック問題およびその発展問題の統一的解法
- 周波数同期保証型放送品質映像伝送システム
- 周波数同期保証型放送品質映像伝送システム
- 周波数同期保証型放送品質映像伝送システム
- 周波数同期保証型放送品質映像伝送システム
- 周波数同期保証型放送品質映像伝送システム(画像符号化・通信・ストリーム技術,及び一般)
- 周波数同期保証型放送品質映像伝送システム(画像符号化・通信・ストリーム技術,及び一般)
- 周波数同期保証型放送品質映像伝送システム(画像符号化・通信・ストリーム技術,及び一般)
- B-7-56 非同期・適応型ネットワーク環境における連続メディア通信形態の一検討
- B-7-55 インタネット受信時刻・受信者指定型情報配送システムの一検討
- ディジタル携帯電話回線におけるARQのTCP/IP伝送特性に対する影響と伝送特性の改善方法について
- 携帯電話回線における再送機能のTCP/IP伝送特性に対する影響
- 携帯電話回線におけるTCP/IPプロトコルの伝送特性について
- ダイナミック・スライス型リンク方式による時刻証明の長期有効性保証方法(オフィスインフォメーションシステム及び一般)
- タイムスタンプ長期有効性保証フレームワーク(オフィスインフォメーションシステム及び一般)
- タイムスタンプ長期有効性保証フレームワーク
- イベント順序証明システムの脅威分析
- イベント順序証明システムの実現機構
- イベント順序証明技術を用いた長期有効性保証タイムスタンプシステム
- スケーラブルで単一攻撃点のないイベント順序証明システム実現機構
- イベント順序証明技術を用いた長期有効性保証タイムスタンプシステム
- スケーラブルで単一攻撃点のないイベント順序証明システム実現機構
- NTPを用いた追跡可能な時刻配送システムの設計(セッション2 : ドキュメント管理・流通基盤技術)
- フロー周波数安定度解析を用いたQoSパッシブ測定法
- インタ-ネットQoSビジュアライザを用いた品質測定実験 (特集 リアルタイム並列分散処理技術)
- インタ-ネットQoSビジュアライザ (特集 リアルタイム並列分散処理技術)
- FEC方式に基づくオーディオアプリケーションにおけるネットワークQoSのLWを用いた品質測定
- インターネットQoSビジュアライザのための実時間データ処理システムの構成
- オーディオパケット品質の適応型再構築手法に関する考察
- インターネットQoSビジュアライザを用いた遅延とジッターの測定
- インターネットQoSビジュアライザの設計と実現
- インターネットQoSビジュアライザにおけるQoS測定方法
- インターネットQoSビジュアライザの構成
- 非線形TRSのE重なり性について
- 書換え系のPerpetual性と一様停止性
- 高階書換え系の単一正規形性
- 逐次性v.s.ストリクト性 : 非線形項書換え系の最適戦略にむけて
- 高階書き換え系の単一正規形性
- 項グラフ書換え系における単純ギャップ停止性
- 91-37 パラメトリシティの証明論の概略
- 理論計算機科学に関する豊橋シンポジウムに参加して
- 公開鍵ベースケルベロス認証サービスにおけるサービスチケット失効リストの分散管理法の提案
- 統計的手法による弱一貫性データの複製制御方法
- ISDNを用いた高精度時計同期方法
- ISDNを用いた広域時計同期システム (特集 リアルタイム並列分散処理技術)
- ISDN時計同期システムのための統計的手法を用いた時計同期方法
- ISDNを用いた分散高精度時刻同期プロトコルとNTPの統合
- 高速ディジタル網を用いたクロック周波数同期
- うるう秒処理を含めた分散高精度時刻同期のための計算機時計システムの構成
- 高速デジタル網を用いた分散高精度時刻/周波数同期
- ISDN網を用いた分散高精度時刻/周波数同期
- 可変帯域リンクをもつネットワークの経路制御
- 分散トランザクション処理に適したダイアログ制御の記述法
- グラフマイナー定理に基づく線形時間アルゴリズムの自動生成
- π-計算の名前制限の名前生成による実装の正しさ
- インターネットにおけるQoSビジュアライザ
- 89-29 ストリクトネス解析に基づく関数型プログラムの計算量解析
- 87-21 関数型プログラムの静的解析
- 広域時計を用いた等時性保証通信の実現法
- グリッドコンピューティングにおける代理証明書信任リスト(ディペンダブルソフトウェア)
- インターネットにおける障害管理の総合的な総合的な支援システムについて
- スケーラビリティと耐故障性を備えたインターネットのインテリジェントサービスの構築法
- 移動体通信と品質 : TCP通信の性能の視点から
- 帯域予約されたTCPトラフィックの特性評価
- 並列分散型連続メディア処理モデルHEARTSにおける同時性保証機構
- 超高速ネットワークのためのルーチング技術
- 「情報処理学会論文誌 : プログラミング」の編集について
- TCP/IPプロトコルによるフレームリレーネットワークの特性評価
- 「情報処理学会論文誌 : プログラミング」の編集について
- Proxy Certificate Trust List for Grid Computing