論文の概要: Cryptographic Choreographies

• arxiv url: http://arxiv.org/abs/2602.12967v1
• Date: Fri, 13 Feb 2026 14:35:19 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-02-16 23:37:53.983694
• Title: Cryptographic Choreographies
• Title（参考訳）: 暗号振付
• Authors: Sebastian Mödersheim, Simon Lund, Alessandro Bruni, Marco Carbone, Rosario Giustolisi,
• Abstract要約: 本稿では,暗号プロトコル仕様のための振付言語であるCryptoChoreoを紹介する。 プロセス計算への変換によってCryptoChoreoのセマンティクスを定義する。
• 参考スコア（独自算出の注目度）: 37.66265825228905
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: We present CryptoChoreo, a choreography language for the specification of cryptographic protocols. Choreographies can be regarded as an extension of Alice-and-Bob notation, providing an intuitive high-level view of the protocol as a whole (rather than specifying each protocol role in isolation). The extensions over standard Alice-and-Bob notation that we consider are non-deterministic choice, conditional branching, and mutable long-term memory. We define the semantics of CryptoChoreo by translation to a process calculus. This semantics entails an understanding of the protocol: it determines how agents parse and check incoming messages and how they construct outgoing messages, in the presence of an arbitrary algebraic theory and non-deterministic choices made by other agents. While this semantics entails algebraic problems that are in general undecidable, we give an implementation for a representative theory. We connect this translation to ProVerif and show on a number of case studies that the approach is practically feasible.
• Abstract（参考訳）: 本稿では,暗号プロトコル仕様のための振付言語であるCryptoChoreoを紹介する。 ChoreographiesはAlice-and-Bob表記の拡張と見なすことができ、プロトコル全体の直感的な高レベルなビューを提供する。 標準的なAlice-and-Bob表記に対する拡張は、非決定論的選択、条件分岐、変更可能な長期記憶である。 プロセス計算への変換によってCryptoChoreoのセマンティクスを定義する。 このセマンティクスにはプロトコルの理解が含まれており、任意の代数理論と他のエージェントによる非決定論的選択の存在下で、エージェントが受信メッセージのパースとチェックの仕方や、送信メッセージの構築方法を決定する。 この意味論は一般に決定不可能な代数的問題を含むが、代表論の実装を与える。 我々は、この翻訳をProVerifに接続し、このアプローチが事実上実現可能であることを示す多くのケーススタディを示す。

関連論文リスト

• Molly: A Verified Compiler for Cryptoprotocol Roles [0.0]
  Mollyは暗号プロトコルロールを直線プログラムにコンパイルする。 我々は,ランタイムの公理化に基づいて,プロトコルの役割を意味論的に定義する。
  論文  参考訳（メタデータ） (2023-11-22T21:04:07Z)
• LpiCT: A logic security analysis framework for protocols [1.4852249222037588]
  本稿では,論理規則と証明,バイナリツリー,KMPアルゴリズムを導入し,論理セキュリティ解析フレームワークとアルゴリズムを新たに拡張する。 実験結果から,新たな拡張理論,論理セキュリティ分析フレームワーク,アルゴリズムが,暗号プロトコルの設計と実装に論理的欠陥があるかどうかを効果的に解析できることが示唆された。
  論文  参考訳（メタデータ） (2023-11-01T12:06:47Z)
• CryptoVerif: a Computationally-Sound Security Protocol Verifier (Initial Version with Communications on Channels) [2.06682776181122]
  この文書はセキュリティプロトコル検証器CryptoVerifを示す。 これはシンボリックなドレフ・ヤオモデルではなく、計算モデルに依存している。 自動で動作させることもできるし、手動による証明表示でガイドすることもできる。
  論文  参考訳（メタデータ） (2023-10-23T07:53:38Z)
• Lexinvariant Language Models [84.2829117441298]
  離散語彙記号から連続ベクトルへの写像であるトークン埋め込みは、任意の言語モデル(LM)の中心にある 我々は、語彙記号に不変であり、したがって実際に固定トークン埋め込みを必要としないテクスチトレキシン変種モデルについて研究する。 十分長い文脈を条件として,レキシン変項LMは標準言語モデルに匹敵する難易度が得られることを示す。
  論文  参考訳（メタデータ） (2023-05-24T19:10:46Z)
• Rigidity of superdense coding [3.4113536110736766]
  量子ビットを1つだけ送信し、共有EPRペアを使用することで、2ビットの古典情報を通信することができる。 送信機と受信機は、古典的ランダム性の源として追加の絡み合いのみを使用することを示す。 $d=2$の場合(つまり1つのqubitを送信)とは異なり、より高額な$d$に対して、等価なスーパーセンスコーディングプロトコルが存在する。
  論文  参考訳（メタデータ） (2020-12-03T03:04:27Z)
• Hierarchical Poset Decoding for Compositional Generalization in Language [52.13611501363484]
  出力が部分的に順序付けられた集合(命題)である構造化予測タスクとして人間の言語理解を形式化する。 現在のエンコーダ・デコーダアーキテクチャは意味論のポーズ構造を適切に考慮していない。 本稿では,言語における合成一般化のための新しい階層型ポーズデコーディングパラダイムを提案する。
  論文  参考訳（メタデータ） (2020-10-15T14:34:26Z)
• A Transformer-based Approach for Source Code Summarization [86.08359401867577]
  コードトークン間のペア関係をモデル化することにより,要約のためのコード表現を学習する。 アプローチは単純であるにもかかわらず、最先端技術よりもかなりの差があることが示される。
  論文  参考訳（メタデータ） (2020-05-01T23:29:36Z)
• Emergence of Pragmatics from Referential Game between Theory of Mind Agents [64.25696237463397]
  エージェントが手書きのルールを指定せずに「行間を読む」能力を自発的に学習するアルゴリズムを提案する。 協調型マルチエージェント教育状況における心の理論(ToM)を統合し,適応型強化学習(RL)アルゴリズムを提案する。
  論文  参考訳（メタデータ） (2020-01-21T19:37:33Z)
• Lexical Sememe Prediction using Dictionary Definitions by Capturing Local Semantic Correspondence [94.79912471702782]
  セメムは人間の言語の最小の意味単位として定義されており、多くのNLPタスクで有用であることが証明されている。 本稿では,このようなマッチングを捕捉し,セメムを予測できるセメム対応プールモデルを提案する。 我々は,有名なSememe KB HowNetのモデルとベースライン手法を評価し,そのモデルが最先端のパフォーマンスを実現することを発見した。
  論文  参考訳（メタデータ） (2020-01-16T17:30:36Z)

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

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