ISO IEC 29128-2011 Information technology - Security techniques - Verification of cryptographic protocols《信息技术 安全技术 加密协议的验证》.pdf

1、 Reference number ISO/IEC 29128:2011(E) ISO/IEC 2011INTERNATIONAL STANDARD ISO/IEC 29128 First edition 2011-12-15 Information technology Security techniques Verification of cryptographic protocols Technologies de linformation Techniques de scurit Vrification des protocoles cryptographiques ISO/IEC 2

2、9128:2011(E) COPYRIGHT PROTECTED DOCUMENT ISO/IEC 2011 All rights reserved. Unless otherwise specified, no part of this publication may be reproduced or utilized in any form or by any means, electronic or mechanical, including photocopying and microfilm, without permission in writing from either ISO

3、 at the address below or ISOs member body in the country of the requester. ISO copyright office Case postale 56 CH-1211 Geneva 20 Tel. + 41 22 749 01 11 Fax + 41 22 749 09 47 E-mail copyrightiso.org Web www.iso.org Published in Switzerland ii ISO/IEC 2011 All rights reservedISO/IEC 29128:2011(E) ISO

4、/IEC 2011 All rights reserved iiiContents Page Foreword . v Introduction vi 1 Scope 1 2 Terms and definitions . 1 3 Symbols and notation. 2 4 General . 3 5 Specifying cryptographic protocols 5 5.1 Objectives 5 5.2 The abstraction levels . 5 5.3 The specification of security protocols 5 5.3.1 General

5、 . 5 5.3.2 The symbolic messages . 5 5.3.3 Observing messages 6 5.3.4 Algebraic properties 7 5.3.5 Protocol roles 7 5.4 The specification of adversarial model . 8 5.4.1 Network specification . 8 5.4.2 The attacker . 8 5.4.3 The scenario 9 5.5 The specification of security properties . 10 5.5.1 Gener

6、al . 10 5.5.2 Trace properties 11 6 Cryptographic protocol assurance levels 12 6.1 General . 12 6.2 Protocol Assurance Level 1 . 13 6.3 Protocol Assurance Level 2 13 6.4 Protocol Assurance Level 3 . 14 6.5 Protocol Assurance Level 4 . 14 6.6 Difference among Protocol Assurance Levels . 14 6.7 Corres

7、ponding assurance levels in ISO/IEC 15408 . 15 7 Security Assessment and Verification 16 7.1 Protocol specification . 16 7.1.1 PPS_SEMIFORMAL . 16 7.1.2 PPS_FORMAL 17 7.1.3 PPS_MECHANIZED . 17 7.2 Adversarial model . 18 7.2.1 PAM INFORMAL . 18 7.2.2 PAM_FORMAL . 18 7.2.3 PAM_MECHANIZED . 19 7.3 Secu

8、rity properties 20 7.3.1 General . 20 7.3.2 PSP_INFORMAL 21 7.3.3 PSP_FORMAL 21 7.3.4 PSP_MECHANIZED . 22 7.4 Self-assessment evidence for verification 23 7.4.1 General . 23 7.4.2 PEV_ARGUMENT . 23 7.4.3 PEV_HANDPROVEN 23 7.4.4 PEV_BOUNDED . 24 7.4.5 PEV_UNBOUNDED 24iv ISO/IEC 2011 All rights reserv

9、ed 8 Common Methodology for Cryptographic Protocols Security Evaluation . 25 8.1 Introduction . 25 8.2 Protocol specification evaluation . 26 8.2.1 Evaluation of sub-activity (PPS_SEMIFORMAL) . 26 8.2.2 Evaluation of sub-activity (PPS_FORMAL) 26 8.2.3 Evaluation of sub-activity (PPS_MECHANIZED) . 26

10、 8.3 Adversarial model evaluation 27 8.3.1 Evaluation of sub-activity (PAM INFORMAL) . 27 8.3.2 Evaluation of sub-activity (PAM_FORMAL) . 27 8.3.3 Evaluation of sub-activity (PAM_MECHANIZED) . 28 8.4 Security properties evaluation 28 8.4.1 Evaluation of sub-activity (PSP_INFORMAL) 28 8.4.2 Evaluatio

11、n of sub-activity (PSP_FORMAL) 28 8.4.3 Evaluation of sub-activity (PSP_MECHANIZED) . 29 8.5 Self-assessment evidence evaluation 29 8.5.1 Evaluation of sub-activity (PEV_ARGUMENT) . 29 8.5.2 Evaluation of sub-activity (PEV_HANDPROVEN) 30 8.5.3 Evaluation of sub-activity (PEV_BOUNDED) . 30 8.5.4 Eval

12、uation of sub-activity (PEV_UNBOUNDED) 30 Annex A (informative) Guidelines for Cryptographic Protocol Design . 32 Annex B (informative) Example of formal specification . 34 B.1 Symbolic specification of security protocols 34 B.1.1 Abstraction level . 34 B.1.2 Protocol specifications 35 B.2 State tra

13、nsitions 37 B.2.1 Attacker model 37 B.2.2 Configuration state . 37 B.2.3 Traces 38 B.3 Trace properties 38 B.3.1 Secrecy 38 B.3.2 Authentication . 39 Annex C (informative) Verification examples . 41 C.1 Sample protocol 41 C.2 Design artifacts . 41 C.2.1 Input to protocol verification tool . 42 C.2.2

14、 Protocol Specification 43 C.2.3 Operating Environment 44 C.2.4 Security Properties . 44 C.2.5 Evidence 44 C.3 Additional inputs for verification 47 Bibliography . 49 ISO/IEC 29128:2011(E) v Foreword ISO (the International Organization for Standardization) and IEC (the International Electrotechnical

15、 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 activit

16、y. 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 committe

17、e, ISO/IEC JTC 1. International Standards are drafted in accordance with the rules given in the ISO/IEC Directives, Part 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 n

18、ational 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 responsibl

19、e for identifying any or all such patent rights. ISO/IEC 29128 was prepared by Technical Committee ISO/IEC JTC 1, Information echnology, Subcommittee SC 27, Security echniques . ISO/IEC 2011 All rights reserved ISO/IEC 29128:2011(E) vi Introduction The security of digital communications is depend nt

20、 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 an

21、d 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 process

22、es 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 cryptogr

23、aphic protocols. ISO/IEC 2011 All rights reserved ISO/IEC 29128:2011(E) 1 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

24、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 fo

25、llowing 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 s

26、pecification, 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 t

27、he specification, design, analysis, construction, and assurance of hardware and software systems whose syntax and semantics are defined on the basis of well- established mathematical concepts ISO/IEC 2011 All rights reserved INTERNATIONAL STANDARD Information technology Security techniques Verificat

28、ion of cryptographic protocols ISO/IEC 29128:2011(E)2 2. 6 adversarial model description of the powers of adversaries who can try to defeat the protocol NOTE It includes restriction on available resources, ability of adversaries, etc. 2.7 security property formally or informally defined property whi

29、ch 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 It includes cryptographic protocol specification, adver

30、sarial 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 It includes all processes by each pr

31、otocol 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 3 Symbols and For the purpose

32、s of this document, the following symbols and notation apply. security property of a protocol model ISO/IEC 2011 All rights reserved ISO/IEC 29128:2011(E) 3 A,B role names m message r random nonce k key c communication channel enc encryption function dec decryption function paring operator Send send

33、ing process Receive receiving process 4 General Verification of a cryptographic protocol involves checking the following artifacts: a) specification of the cryptographic protocol; b) specification of the adversarial model; c) specification of the security objectives and properties; d) self-assessmen

34、t evidence that the specification of the cryptographic protocol in its adversarial model achieves and satisfies its objectives and properties. The artifacts shall clearly state parameters or properties relevant for the verification. Examples include the bound used in bounded verification as later de

35、scibed in Clause 7.4.4.1 or assumed algebraic properties of cryptographic operators used in the protocol as described in Clause 7.1.2.3 and Clause 5.3.4. The different Protocol Assurance Levels will lead to different requirements for these four artifacts. The stated requirements are only for design

36、verification not implementation verification. NOTE 1 For verifying an implementation, additional assurance requirements should be supplied and satisfied. This International Standard does not specify precisely what proof methods or tools shall be used, but instead only specifes their properties. This

37、 encourages protocol designers to use the state-of-the-art for protocol verification in terms of models, methods, and tools. ISO/IEC 2011 All rights reserved ISO/IEC 29128:2011(E) 4 Verification tools shall fulfil the following conditions. a) The verification tools are sound. The protocol designer o

38、r possibly an independent third party shall provide evidence of the correctness of the verification tool used. This may, for example, be in terms of a pencil-and-paper proof of the soundness of the calculus used or, in some cases, in terms of code inspection to see that the tool properly implements

39、the calculus. NOTE 2 This step is nontrivial, yet it is essential if machine checked proofs are to provide greater confidence than hand proofs. In theory, this can be done once and for all for a verification tool, although in practice, tools evolve over time. b) The results of verification tools are

40、 documented in such a way that they are repeatable. The protocol designer shall provide adequate documentation, including all inputs needed for the tool to construct a proof or (in the case of decision procedures) determine provability. c) The verification tools are available for outside evaluation

41、and use. The protocol designer shall indicate all necessary tools to independently check the proofs. NOTE 3 At least in theory, protocol verification canbe carried out by hand proofs, using paper and pencil. However, given the substantial amount of detail typically involved in security protocol veri

42、fication, especially for the high Protocol Assurance Levels, confidence in the results is substantially increased by using mechanized tools such as model checkers and theorem provers. Thus, proofs only with paper-and-pencil are treated as lower assurance level (i.e. PAL2) than mechanized proof in th

43、is International Standard. ISO/IEC 2011 All rights reserved ISO/IEC 29128:2011(E) 5 5 Specifying cryptographic protocols 5.1 Objectives The goal of this part is to provide guidelines and minimal requirements for specifying cryptographic protocols. 5.2 The abstraction levels The protocols can be spec

44、ified at several levels of abstraction, each corresponding to a computation model. At the most abstract level, messages are terms constructed from symbols and the attacker is also modelled as a formal process. We will call this abstraction the symbolic level. In such a model, the resources (both tim

45、e and space resources) are not considered. Any other model can be defined as a refinement of a symbolic model. For instance we can interpret the symbols used in the symbolic model as functions on bitstrings, that can be computed in polynomial time. Therefore, any cryptographic protocol consists in a

46、 symbolic specification and an interpretation in a given domain (e.g. bitstrings or structured data, or even material-dependent formats) of all the symbols, together with assumptions on their interpretation. Such hypotheses can ensure some correspondence between the properties at various abstraction

47、 levels. NOTE In this International Standard, we only consider the symbolic specification of security protocols. Further documents are required for the specification of other (lower) abstraction levels. Typically, it will be necessary to explain how to specify the interpretation domain and how to ca

48、rry security guarantees across levels of abstraction. 5.3 The specification of security protocols 5.3.1 General As explained, a symbolic specification is the necessary first part towards the full specification of a protocol. We list below the minimal mandatory parts in a symbolic protocol specificat

49、ion. 5.3.2 The symbolic messages The first part consists in specifying what are the possible (valid) messages. In this clause, the cryptographic primitives used in the protocol must be listed. Since we are talking about a symbolic specification, this part consists of providing with 1. a set of function symbols Each function symbol has either a fixed arity, that has to be specified, or it is variadic (in which case it has also to be specified). ISO/IEC 2011 All rights res