※一部、英文及び仏文を自動翻訳した日本語訳を使用しています。
序文
ISO (国際標準化機構) と IEC (国際電気標準会議) は、世界標準化のための専門システムを形成しています。 ISO または IEC のメンバーである国家機関は、技術活動の特定の分野を扱うために、それぞれの組織によって設立された技術委員会を通じて、国際規格の開発に参加しています。 ISO と IEC の技術委員会は、相互に関心のある分野で協力しています。 ISO および IEC と連携して、政府および非政府の他の国際機関もこの作業に参加しています。情報技術の分野では、ISO と IEC が合同技術委員会 ISO/IEC JTC 1 を設立しました。
国際規格は、ISO/IEC 指令で指定された規則に従って起草されます。 2.
合同技術委員会の主な任務は、国際規格を作成することです。合同技術委員会によって採択された国際規格草案は、投票のために各国の機関に回覧されます。国際規格として発行するには、投票を行う国の機関の少なくとも 75% による承認が必要です。
このドキュメントの要素の一部が特許権の対象となる可能性があることに注意してください。 ISO および IEC は、そのような特許権の一部またはすべてを特定する責任を負わないものとします。
ISO/IEC 29128 は、合同技術委員会 ISO/IEC JTC 1, 情報技術、小委員会 SC 27, IT セキュリティ技術によって作成されました。
序章
デジタル通信のセキュリティは、暗号化メカニズムがますます重要な役割を果たす多くの側面に依存しています。このようなメカニズムが使用されている場合、暗号化アルゴリズムの強度、実装の正確さと正確さ、暗号化システムの正しい操作と使用、展開された暗号化プロトコルのセキュリティなど、多くのセキュリティ上の懸念があります。
暗号化アルゴリズムの仕様、および暗号化デバイスとモジュールの実装とテストに関する標準は既に存在します。ただし、そのような通信で使用されるプロトコルの仕様を評価するための標準または一般的に受け入れられているプロセスはありません。この国際規格の目標は、暗号プロトコル仕様のセキュリティに関して定義されたレベルの信頼性を提供するために、暗号プロトコル仕様の検証手段を確立することです。
1 スコープ
この国際規格は、暗号プロトコルの仕様のセキュリティ証明のための技術基盤を確立します。この国際規格は、これらのプロトコルの設計評価基準と、そのようなプロトコルの検証プロセスに適用される方法を指定します。この国際規格は、ISO/IEC 15408 の評価保証コンポーネントと一致するさまざまなプロトコル保証レベルの定義も提供します。
2 用語と定義
このドキュメントでは、次の用語と定義が適用されます。
2.1
アリティ
引数の数
2.2
暗号プロトコル
暗号化を使用してセキュリティ関連の機能を実行するプロトコル
2.3
正式な方法
ハードウェアおよびソフトウェア システムの仕様、設計、分析、構築、および保証に使用されるモデリング、計算、および予測のための確立された数学的概念に基づく手法
2.4
正式な説明
十分に確立された数学的概念に基づいて構文と意味が定義されている記述
2.5
正式な言語
確立された数学的概念に基づいて構文とセマンティクスが定義されているハードウェアおよびソフトウェア システムの仕様、設計、分析、構築、および保証におけるモデリング、計算、および予測のための言語。
2.6
敵対的モデル
プロトコルを破ろうとする敵の力の説明
注記 1:利用可能なリソース、敵の能力などの制限が含まれます。
2.7
セキュリティ プロパティ
機密性、真正性、匿名性などを保証するために暗号プロトコルが設計されている、公式または非公式に定義されたプロパティ
2.8
自己評価の証拠
指定されたプロトコルが指定されたセキュリティ プロパティを満たしているかどうかを検証するために開発者が使用する証拠
注記 1:暗号プロトコルの仕様、敵対的モデル、および正式な検証ツールの出力 (写し) が含まれます。
2.9
プロトコル モデル
敵対モデルに関するプロトコルとその動作の仕様
2.10
プロトコル仕様
指定されたプロトコルのすべての正式および非公式の説明
注記 1:各プロトコル参加者によるすべてのプロセス、参加者間のすべての通信、およびその順序が含まれます。
2.11
秘密
メッセージまたはデータが許可されていないエンティティによって学習されるべきではないことを示す暗号プロトコルのセキュリティ プロパティ。
2.12
可変長
アリティが可変の関数の性質
参考文献
| [1] | Yannick Chevalier, Ralf K"usters, Micha"el Rusinowitch, Mathieu Turuan XOR を使用したプロトコルの安全性に対する NP 決定手順。理論上のコンピュータ科学、338(1-3):247-274, 200 |
| [2] | ヒューバート・コモン＝ルンドとラルフ・トレイネン。簡単な侵入者控除。検証: 理論と実践、コンピュータ サイエンスの講義ノートの第 2772 巻、225 ～ 242 ページ。スプリンガーズ、2003年。 |
| [3] | D ドレフと A ヤオ。公開鍵プロトコルのセキュリティについて。情報理論に関する IEEE トランザクション、29:198-208, 1983 年。 |
| [4] | F. ハビエル セイヤー ファブレガ、ジョナサン C. ヘルツォーク、ジョシュア D. グットマン。ストランド スペース: セキュリティ プロトコルが正しいことの証明。ジャーナル オブ コンピューター セキュリティ、7:191-230, 1999 年。 |
| [5] | マーティン・アバディとロジャー・ニーダム、暗号化プロトコルの慎重なエンジニアリング実践、セキュリティとプライバシーの研究に関する1994年IEEEコンピュータ協会シンポジウムの議事録、1994年。 |
| [6] | ロス・アンダーソンとロジャー・ニーダム、公開鍵プロトコルのロバストネス原則、暗号学の進歩に関する国際会議の議事録 (CRYPTO 95)、コンピュータ科学の講義ノートの第 963 巻、236 ～ 247 ページ。スプリンガー出版社、1995 年。 |
| [7] | David Basin, Sebastian Mödersheim, Luca Viganô、「OFMC: セキュリティ プロトコルのシンボリック モデル チェッカー」、International Journal of Information Security, Springer-Verlag, 2005 年。 |
| [8] | アレッサンドロ・アルマンド、デヴィッド・ベイシン、ヨハン・ボイシュット、ヤニック・シュヴァリエ、ルカ・コンパーニャ、ホルヘ・クエラー、ポール・ハンケス・ドリエルスマ、ピエール＝シリル・ヘアム、オルガ・クチナレンコ、ヤコポ・マントヴァーニ、セバスチャン・モーダースハイム、デヴィッド・フォン・オーハイム、マイケル・ルシノウィッチ、ジャドソン・サンティアゴ、マチュー・トゥルアニ、ルカViganô、Laurent Vigneron, 「インターネット セキュリティ プロトコルおよびアプリケーションの自動検証のための AVISPA ツール」、CAV'2005 議事録、LNCS 3576, Springer-Verlag, 2005 年。 |
| [9] | C. Cremer, Scyther - Semantics and Verification of Security Protocols, アイントホーフェン工科大学、博士論文、2006 年。 |
| [10] | B. ブランシェ、セキュリティ プロトコル対応の自動検証、CoRR abs/0802.3444, 2008 年。 |
| [11] | S. Delaune et al.、モノイド方程式理論のシンボリック プロトコル分析、情報と計算、第 206 巻、第 2 ～ 4 号、312 ～ 351 ページ、2008 年。 |
| [12] | 参照。 R Kusters および T Truderung, ホーン理論ベースのアプローチで XOR を使用したプロトコル分析を XOR のないケースに還元、Proc.コンピューターと通信のセキュリティに関する第 15 回 ACM 会議の 129 ～ 138 ページ、2008 年。 |
| [13] | ISO/IEC 15408-1:2009, 情報技術 — セキュリティ技術 — IT セキュリティの評価基準 — 1: 導入と一般的なモデル |
| [14] | ISO/IEC 15408-2:2008, 情報技術 — セキュリティ技術 — IT セキュリティの評価基準 — 2: セキュリティ機能要素 |
| [15] | ISO/IEC 15408-3:2008, 情報技術 — セキュリティ技術 — IT セキュリティの評価基準 — 3: セキュリティ保証コンポーネント |
Foreword
ISO (the International Organization for Standardization) and IEC (the International Electrotechnical Commission) form the specialized system for worldwide standardization. National bodies that are members of ISO or IEC participate in the development of International Standards through technical committees established by the respective organization to deal with particular fields of technical activity. ISO and IEC technical committees collaborate in fields of mutual interest. Other international organizations, governmental and non-governmental, in liaison with ISO and IEC, also take part in the work. In the field of information technology, ISO and IEC have established a joint technical committee, ISO/IEC JTC 1.
International Standards are drafted in accordance with the rules given in the ISO/IEC Directives, 2.
The main task of the joint technical committee is to prepare International Standards. Draft International Standards adopted by the joint technical committee are circulated to national bodies for voting. Publication as an International Standard requires approval by at least 75 % of the national bodies casting a vote.
Attention is drawn to the possibility that some of the elements of this document may be the subject of patent rights. ISO and IEC shall not be held responsible for identifying any or all such patent rights.
ISO/IEC 29128 was prepared by Joint Technical Committee ISO/IEC JTC 1, Information technology, Subcommittee SC 27, IT Security techniques.
Introduction
The security of digital communications is dependent on a number of aspects, where cryptographic mechanisms play an increasingly important role. When such mechanisms are being used, there are a number of security concerns such as the strength of the cryptographic algorithms, the accuracy and correctness of the implementation, the correct operation and use of cryptographic systems, and the security of the deployed cryptographic protocols.
Standards already exist for the specification of cryptographic algorithms, and for the implementation and test of cryptographic devices and modules. However, there are no standards or generally accepted processes for the assessment of the specification of protocols used in such communication. The goal of this International Standard is to establish means for verification of cryptographic protocol specifications to provide defined levels of confidence concerning the security of the specification of cryptographic protocols.
1 Scope
This International Standard establishes a technical base for the security proof of the specification of cryptographic protocols. This International Standard specifies design evaluation criteria for these protocols, as well as methods to be applied in a verification process for such protocols. This International Standard also provides definitions of different protocol assurance levels consistent with evaluation assurance components in ISO/IEC 15408.
2 Terms and definitions
For the purposes of this document, the following terms and definitions apply.
2.1
arity
number of arguments
2.2
cryptographic protocol
protocol which performs a security-related function using cryptography
2.3
formal methods
techniques based on well-established mathematical concepts for modelling, calculation, and predication used in the specification, design, analysis, construction, and assurance of hardware and software systems
2.4
formal description
description whose syntax and semantics are defined on the basis of well-established mathematical concepts
2.5
formal language
language for modelling, calculation, and predication in the specification, design, analysis, construction, and assurance of hardware and software systems whose syntax and semantics are defined on the basis of wellestablished mathematical concepts
2.6
adversarial model
description of the powers of adversaries who can try to defeat the protocol
Note 1 to entry: It includes restriction on available resources, ability of adversaries, etc.
2.7
security property
formally or informally defined property which a cryptographic protocol is designed to assure such as secrecy, authenticity, or anonymity
2.8
self-assessment evidence
evidence that the developer uses to verify whether a specified protocol fulfils its designated security properties
Note 1 to entry: It includes cryptographic protocol specification, adversarial model and output (transcripts) of formal verification tool.
2.9
protocol model
specification of a protocol and its behaviour with respect to an adversarial model
2.10
protocol specification
all formal and informal descriptions of a specified protocol
Note 1 to entry: It includes all processes by each protocol participant, all communications between them and their order
2.11
secrecy
security property for a cryptographic protocol stating that a message or data should not be learned by unauthorized entities
2.12
variadic
property of a function whose arity is variable
Bibliography
| [1] | Yannick Chevalier, Ralf K"usters, Micha"el Rusinowitch, and Mathieu Turuani. An NP decision procedure for protocol insecurity with XOR. Theor. Comput. Sci., 338(1-3):247–274, 2005. |
| [2] | Hubert Comon-Lundh and Ralf Treinen. Easy intruder deductions. In Verification: Theory and Practice, volume 2772 of Lecture Notes in Computer Science, pages 225–242. Springer, 2003. |
| [3] | D. Dolev and A. Yao. On the security of public key protocols. IEEE Transactions on Information Theory, 29:198–208, 1983. |
| [4] | F. Javier Thayer Fábrega, Jonathan C. Herzog, and Joshua D. Guttman. Strand spaces: Proving security protocols correct. Journal of Computer Security, 7:191–230, 1999. |
| [5] | Martin Abadi and Roger Needham, Prudent engineering practice for cryptographic protocols, the Proceedings of the 1994 IEEE Computer Society Symposium on Research in Security and Privacy, 1994. |
| [6] | Ross Anderson and Roger Needham, Robustness principles for public key protocols, the Proceedings of International Conference on Advances in Cryptology (CRYPTO 95), volume 963 of Lecture Notes in Computer Science, pages 236–247. Springer-Verlag, 1995. |
| [7] | David Basin, Sebastian Mödersheim, Luca Viganô,"OFMC: A symbolic model checker for security protocols", International Journal of Information Security, Springer-Verlag, 2005. |
| [8] | Alessandro Armando, David Basin, Yohan Boichut, Yannick Chevalier, Luca Compagna, Jorge Cuellar, Paul Hankes Drielsma, Pierre-Cyrille Héam, Olga Kouchnarenko, Jacopo Mantovani, Sebastian Mödersheim, David von Oheimb, Michael Rusinowitch, Judson Santiago, Mathieu Turuani, Luca Viganô, Laurent Vigneron,"The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications", in Proceedings of CAV'2005, LNCS 3576, Springer-Verlag, 2005. |
| [9] | С. Cremer, Scyther - Semantics and Verification of Security Protocols, Technische Universiteit Eindhoven, PhD Thesis, 2006. |
| [10] | B. Blanchet, Automatic Verification of Correspondences for Security Protocols, CoRR abs/0802.3444, 2008. |
| [11] | S. Delaune et al., Symbolic protocol analysis for monoidal equational theories, Information and Computation, Volume 206, Issues 2-4, pages 312-351, 2008. |
| [12] | Cf. R. Kusters and T. Truderung, Reducing protocol analysis with XOR to the XOR-free case in the horn theory based approach, In Proc. of the 15th ACM conference on Computer and communications security, pages 129-138, 2008. |
| [13] | ISO/IEC 15408-1:2009, Information technology — Security techniques — Evaluation criteria for IT security — 1: Introduction and general model |
| [14] | ISO/IEC 15408-2:2008, Information technology — Security techniques — Evaluation criteria for IT security — 2: Security functional components |
| [15] | ISO/IEC 15408-3:2008, Information technology — Security techniques — Evaluation criteria for IT security — 3: Security assurance components |