セキュリティプロトコル表記

暗号学において、セキュリティ（エンジニアリング）プロトコル表記法は、プロトコルナレーション^[1]やアリス＆ボブ表記法とも呼ばれ、コンピュータネットワークなどの動的システムのエンティティ間の通信プロトコルを表現する方法です。形式モデルのコンテキストでは、このようなシステムの特性についての推論が可能になります。

標準表記は、通信を希望するプリンシパルのセット (通常はAlice、Bob、Charlie などの名前) で構成されます。プリンシパルは、サーバー S、共有キー K、タイムスタンプ T にアクセスでき、認証目的でnonce N を生成できます。

簡単な例としては次のようなものが考えられます。

${\displaystyle A\rightarrow B:\{X\}_{K_{A,B}}}$

これは、 A が共有キーK _A,Bで暗号化された平文Xで構成されるメッセージをB obに送信することを意図していることを示しています。

別の例としては次のようなものが考えられます。

${\displaystyle B\rightarrow A:\{N_{B}\}_{K_{A}}}$

これは、Bが Alice の公開鍵を使用して暗号化されたnビットN _Bからなる Alice 宛のメッセージを意図していることを示しています。

2 つの添え字K _A,Bを持つキーは、対応する 2 人の個人によって共有される対称キーです。1 つの添え字K _Aを持つキーは、対応する個人の公開キーです。秘密キーは、公開キーの 逆として表されます。

この表記法では操作のみが指定され、そのセマンティクスは指定されません。たとえば、秘密鍵の暗号化と署名は同じように表されます。

このような方法で、より複雑なプロトコルを表現することができます。例としてKerberosを参照してください。一部の情報源では、この表記法をKerberos表記法と呼んでいます。^[2]一部の著者は、Steiner、Neuman、Schiller ^[3]が使用した表記法を注目すべき参考文献と考えています。^[4]

このようにセキュリティ プロトコルについて推論するモデルはいくつか存在しますが、そのうちの 1 つがBAN ロジックです。

セキュリティ プロトコル表記法は、振り付けプログラミングで使用される多くのプログラミング言語に影響を与えました。