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

1、raising standards worldwide NO COPYING WITHOUT BSI PERMISSION EXCEPT AS PERMITTED BY COPYRIGHT LAW BSI Standards Publication BS ISO/IEC 29128:2011 Information technology Security techniques Verification of cryptographic protocolsBS ISO/IEC 29128:2011 BRITISH STANDARD National foreword This British S

2、tandard is the UK implementation of ISO/IEC 29128:2011. The UK participation in its preparation was entrusted to Technical Committee IST/33, IT - Security techniques. A list of organizations represented on this committee can be obtained on request to its secretary. This publication does not purport

3、to include all the necessary provisions of a contract. Users are responsible for its correct application. The British Standards Institution 2012 ISBN 978 0 580 65107 6 ICS 35.040 Compliance with a British Standard cannot confer immunity from legal obligations. This British Standard was published und

4、er the authority of the Standards Policy and Strategy Committee on 31 January 2012. Amendments issued since publication Date Text affectedBS ISO/IEC 29128:2011Reference number ISO/IEC 29128:2011(E) ISO/IEC 2011INTERNATIONAL STANDARD ISO/IEC 29128 First edition 2011-12-15 Information technology Secur

5、ity techniques Verification of cryptographic protocols Technologies de linformation Techniques de scurit Vrification des protocoles cryptographiques BS ISO/IEC 29128:2011 ISO/IEC 29128:2011(E) COPYRIGHT PROTECTED DOCUMENT ISO/IEC 2011 All rights reserved. Unless otherwise specified, no part of this

6、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 at the address below or ISOs member body in the country of the requester. ISO copyright office Case postale 56 CH-1211

7、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 reservedBS ISO/IEC 29128:2011 ISO/IEC 29128:2011(E) ISO/IEC 2011 All rights reserved iiiContents Page Foreword . v Introduction vi 1 Scope 1 2 Terms and

8、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.3.2 The symbolic messages . 5 5.3.3 Observing messages 6 5.3.4 Algebraic properties 7 5.3.5

9、 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 General . 10 5.5.2 Trace properties 11 6 Cryptographic protocol assurance levels 12 6.1 General . 12 6.

10、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 Corresponding assurance levels in ISO/IEC 15408 . 15 7 Security Assessment and Verification 16 7.1 Proto

11、col 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 Security properties 20 7.3.1 General . 20 7.3.2 PSP_INFORMAL 21 7.3.3 PSP_FORMAL 21 7.3.4 PSP_MECHANIZ

12、ED . 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 24BS ISO/IEC 29128:2011 iv ISO/IEC 2011 All rights reserved 8 Common Methodology for Cryptographic Protocols Security Evaluation . 25

13、 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 8.3 Adversarial model evaluation 27 8.3.1 Evaluation of sub-activity (PAM I

14、NFORMAL) . 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 Evaluation of sub-activity (PSP_FORMAL) 28 8.4.3 Evaluation of sub-activity (PSP_MECH

15、ANIZED) . 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 Evaluation of sub-activity (PEV_UNBOUNDED) 30 Annex A (informative) Guidelines f

16、or 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 transitions 37 B.2.1 Attacker model 37 B.2.2 Configuration state . 37 B.2.3 Tra

17、ces 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 Protocol Specification 43 C.2.3 Operating Environment 44 C.2.4 Security Pro

18、perties . 44 C.2.5 Evidence 44 C.3 Additional inputs for verification 47 Bibliography . 49 ISO/IEC 29128:2011(E) BS ISO/IEC 29128:2011 v Foreword ISO (the International Organization for Standardization) and IEC (the International Electrotechnical Commission) form the specialized system for worldwide

19、 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 fie

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

21、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 national bodies for voting. Publication as an Internati

22、onal 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/I

23、EC 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) BS ISO/IEC 29128:2011 vi Introduction The security of digital communications is depend nt on a number of aspects, where cr

24、yptographic 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, a

25、nd 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 spec

26、ification 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. ISO/IEC 2011 All

27、 rights reserved ISO/IEC 29128:2011(E) BS ISO/IEC 29128:2011 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 well as met

28、hods 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 ter

29、ms 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 specificatio

30、n, 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 specific

31、ation, 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 Verification of cryp

32、tographic protocols ISO/IEC 29128:2011(E)BS ISO/IEC 29128:2011 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 p

33、roperty 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 It includes cryptographic protocol specifica

34、tion, 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 It includes all processes

35、 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 3 Symbols and For

36、the purposes 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) BS ISO/IEC 29128:2011 3 A,B role names m message r random nonce k key c communication channel enc encryption function dec decryption f

37、unction paring operator Send sending 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

38、and properties; d) self-assessment 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

39、 bounded verification as later descibed 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

40、requirements are only for design 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 onl

41、y specifes their properties. This 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) BS ISO/IEC 29128:2011 4 Verification tools shall fulfil the following conditions. a) Th

42、e verification tools are sound. The protocol designer or 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 co

43、de inspection to see that the tool properly implements 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 evo

44、lve over time. b) The results of verification tools are 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 v

45、erification tools are available for outside evaluation 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

46、 of detail typically involved in security protocol verification, 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

47、assurance level (i.e. PAL2) than mechanized proof in this International Standard. ISO/IEC 2011 All rights reserved ISO/IEC 29128:2011(E) BS ISO/IEC 29128:2011 5 5 Specifying cryptographic protocols 5.1 Objectives The goal of this part is to provide guidelines and minimal requirements for specifying

48、cryptographic protocols. 5.2 The abstraction levels The protocols can be specified 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

49、this abstraction the symbolic level. In such a model, the resources (both time 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 symbolic specification and an interpretation in a given domain (e.g. bitstrings or structured