論文の概要: Tamgram: A Frontend for Large-scale Protocol Modeling in Tamarin

• arxiv url: http://arxiv.org/abs/2408.13138v1
• Date: Fri, 23 Aug 2024 15:00:44 GMT
• ステータス: 処理完了
• システム内更新日: 2024-08-26 14:41:09.652515
• Title: Tamgram: A Frontend for Large-scale Protocol Modeling in Tamarin
• Title（参考訳）: Tamgram: 玉林における大規模プロトコルモデリングのフロントエンド
• Authors: Di Long Li, Jim de Groot, Alwen Tiu,
• Abstract要約: この研究は、Tamgramと呼ばれる高レベルなプロトコルモデリング言語を導入し、Tamrinのマルチセット書き換えセマンティクスに変換できる形式的セマンティクスを導入している。 TamgramはネイティブなTamarinコードを直接記述できるだけでなく、さまざまな高レベルな構成で大きな仕様を簡単に構築できる。 本研究では,タマリンのトレースセマンティクスに関するタマグラムの健全性と完全性を証明し,異なる翻訳戦略について議論し,手作業によるタマリン仕様に匹敵する性能をもたらす最適戦略を特定する。
• 参考スコア（独自算出の注目度）: 3.7541073979828723
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Automated security protocol verifiers such as ProVerif and Tamarin have been increasingly applied to verify large scale complex real-world protocols. While their ability to automate difficult reasoning processes required to handle protocols at that scale is impressive, there remains a gap in the modeling languages used. In particular, providing support for writing and maintaining large protocol specifications. This work attempts to fill this gap by introducing a high-level protocol modeling language, called Tamgram, with a formal semantics that can be translated to the multiset rewriting semantics of Tamarin. Tamgram supports writing native Tamarin code directly, but also allows for easier structuring of large specifications through various high-level constructs, in particular those needed to manipulate states in protocols. We prove the soundness and the completeness of Tamgram with respect to the trace semantics of Tamarin, discuss different translation strategies, and identify an optimal strategy that yields performance comparable to manually coded Tamarin specifications. Finally we show the practicality of Tamgram with a set of small case studies and one large scale case study.
• Abstract（参考訳）: ProVerifやTamarinのような自動セキュリティプロトコル検証器は、大規模で複雑な実世界のプロトコルを検証するためにますます応用されている。 その規模でプロトコルを扱うのに必要な、難しい推論プロセスを自動化する能力は印象的だが、使われているモデリング言語にはまだギャップがある。 特に、大規模なプロトコル仕様を記述および保守するためのサポートを提供する。 この研究は、タマリンのマルチセット書き換えセマンティクスに変換可能な形式的セマンティクスで、Tamgramと呼ばれる高レベルのプロトコルモデリング言語を導入することで、このギャップを埋めようとしている。 TamgramはネイティブなTamarinコードを直接書くことをサポートしているが、様々な高レベルな構造体、特にプロトコルで状態を操作するために必要なものを通じて、大きな仕様を簡単に構成できる。 本研究では,タマリンのトレースセマンティクスに関するタマグラムの健全性と完全性を証明し,異なる翻訳戦略について議論し,手作業によるタマリン仕様に匹敵する性能をもたらす最適戦略を特定する。 最後に,小型ケーススタディと大規模ケーススタディのセットを用いて,Tamgramの実用性を示す。

関連論文リスト

• Advancing Interpretability in Text Classification through Prototype Learning [1.9526476410335776]
  ProtoLensはプロトタイプベースのモデルで、テキスト分類のための詳細なサブ文レベルの解釈機能を提供する。 ProtoLensは、Prototype-aware Span extractモジュールを使用して、関連するテキストスパンを識別する。 ProtoLensは、競争精度を維持しながら解釈可能な予測を提供する。
  論文  参考訳（メタデータ） (2024-10-23T03:53:46Z)
• TAMS: Translation-Assisted Morphological Segmentation [3.666125285899499]
  正準形態素セグメンテーションのためのシーケンス・ツー・シーケンスモデルを提案する。 我々のモデルは、超低リソース設定においてベースラインよりも優れるが、トレーニング分割とより多くのデータとの混合結果が得られる。 高いリソース設定で翻訳を便利にするためには、さらなる作業が必要であるが、我々のモデルは、リソース制約の厳しい設定で、約束を示す。
  論文  参考訳（メタデータ） (2024-03-21T21:23:35Z)
• Code-Switched Language Identification is Harder Than You Think [69.63439391717691]
  コードスイッチングは、文字と音声の通信において一般的な現象である。 CSコーパスの構築の応用について検討する。 タスクをもっと多くの言語に拡張することで、タスクをより現実的にします。 文レベルのマルチラベルタグ付け問題としてタスクを再構築し、より難易度の高いものにする。
  論文  参考訳（メタデータ） (2024-02-02T15:38:47Z)
• ToPro: Token-Level Prompt Decomposition for Cross-Lingual Sequence Labeling Tasks [12.700783525558721]
  ToProメソッドは入力文を1つのトークンに分解し、各トークンに1つのプロンプトテンプレートを適用する。 マルチリンガルNERおよびPOSタグ付けデータセットの実験により,ToProをベースとしたファインチューニングは,ゼロショットのクロスリンガル転送において,VanillaファインチューニングとPrompt-Tuningに優れることが示された。
  論文  参考訳（メタデータ） (2024-01-29T21:44:27Z)
• Coding by Design: GPT-4 empowers Agile Model Driven Development [0.03683202928838613]
  この研究は、アジャイルモデル駆動開発(MDD)アプローチを提供し、OpenAIのGPT-4を使ってコードの自動生成を強化する。 私たちの研究は、現行のMDDメソッドへの重要な貢献として"アジリティ"を強調しています。 最終的に、GPT-4を利用して、最後のレイヤはJavaとPythonの両方でコードを自動生成します。
  論文  参考訳（メタデータ） (2023-10-06T15:05:05Z)
• LongCoder: A Long-Range Pre-trained Language Model for Code Completion [56.813974784131624]
  LongCoderは自己アテンションにスライディングウィンドウ機構を採用し、グローバルアクセス可能なトークンを2種類導入している。 ブリッジトークンは入力シーケンス全体を通して挿入され、ローカル情報を集約し、グローバルな相互作用を促進する。 メモリトークンは、後で呼び出され、記憶する必要がある重要なステートメントをハイライトするために含まれます。
  論文  参考訳（メタデータ） (2023-06-26T17:59:24Z)
• Online Gesture Recognition using Transformer and Natural Language Processing [0.0]
  トランスフォーマーアーキテクチャは、自然言語文のグリフストロークに対応するオンラインジェスチャーのための強力なマシンフレームワークを提供する。 トランスフォーマーアーキテクチャは、自然言語文のグリフストロークに対応するオンラインジェスチャーのための強力なマシンフレームワークを提供する。
  論文  参考訳（メタデータ） (2023-05-05T10:17:22Z)
• A Simple Multi-Modality Transfer Learning Baseline for Sign Language Translation [54.29679610921429]
  既存の手話データセットには、約10K-20Kの手話ビデオ、グロスアノテーション、テキストが含まれています。 したがって、データは効果的な手話翻訳モデルの訓練のボトルネックとなる。 この単純なベースラインは、2つの手話翻訳ベンチマークで過去の最先端の結果を上回っている。
  論文  参考訳（メタデータ） (2022-03-08T18:59:56Z)
• Improving Sign Language Translation with Monolingual Data by Sign Back-Translation [105.83166521438463]
  本稿では,手話テキストを手話訓練に組み込んだ手話逆翻訳(SignBT)手法を提案する。 テキストからグロスへの翻訳モデルを用いて、まずモノリンガルテキストをそのグロスシーケンスに逆変換する。 そして、推定グロス・トゥ・サインバンクから特徴レベルで部品をスプライシングしてペアサインシーケンスを生成する。
  論文  参考訳（メタデータ） (2021-05-26T08:49:30Z)
• Automatic Extraction of Rules Governing Morphological Agreement [103.78033184221373]
  原文から第一パス文法仕様を抽出する自動フレームワークを開発する。 我々は、世界の多くの言語の文法の中核にあるモルフォシンタクティックな現象である合意を記述する規則の抽出に焦点をあてる。 我々のフレームワークはUniversal Dependenciesプロジェクトに含まれるすべての言語に適用され、有望な結果が得られます。
  論文  参考訳（メタデータ） (2020-10-02T18:31:45Z)
• UniT: Unified Knowledge Transfer for Any-shot Object Detection and Segmentation [52.487469544343305]
  オブジェクト検出とセグメンテーションの方法は、トレーニングのための大規模インスタンスレベルのアノテーションに依存します。 本稿では,直感的かつ統一的な半教師付きモデルを提案する。
  論文  参考訳（メタデータ） (2020-06-12T22:45:47Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。