JP5368893B2 - Verification device, verification method, and verification program for verifying protocol safety - Google Patents

Description

  The present invention relates to a verification device, a verification method, and a verification program for verifying the security of an authentication or key exchange protocol having security functions such as authentication and key sharing.

  Conventionally, an empirically secure authentication or key exchange protocol has been proposed based on the insight of security and cryptographic techniques possessed by a protocol designer. However, security vulnerabilities have been pointed out after the proposed authentication or key exchange protocol specifications have been published. If vulnerabilities are discovered after the standardized authentication or key exchange protocol is widely spread through products, the cost associated with the modification of the products becomes a major problem.

  In particular, when a fatal vulnerability is discovered, it is necessary to take immediate measures such as applying software patches and replacing hardware chips and components in order to avoid economic damage. Therefore, as the proposed authentication or key exchange protocol and related products become more widespread, the social impact becomes very large, and in some cases, the entire system may fail.

  Therefore, an apparatus, a method, and a program for verifying the security of an authentication or key exchange protocol using a concept called “generally connectable security” have been proposed (for example, Patent Document 1 and Patent Document 2). reference). Here, “generic combinable security” means that an authentication or key exchange protocol is secure if an authentication or key exchange protocol safely realizes an ideal function related to the security function. ing. For example, if a key exchange protocol securely implements the key exchange ideal function, this key exchange protocol has been shown to be secure.

JP 2007-28447 A JP 2008-35117 A

  The above-mentioned “general-linkable safety” is said to be the strongest safety at present, and the ideal function covers all the safety required for the security function. Therefore, when a certain authentication or key exchange protocol securely realizes its ideal function, this authentication or key exchange protocol satisfies all the security required for the security function.

  However, because the security and efficiency of the protocol are in a trade-off relationship, the efficiency decreases as the security of the authentication or key exchange protocol increases. Therefore, when importance is attached to the efficiency of the authentication or key exchange protocol, the security may be lowered to an allowable limit. However, although the above prior art can verify the strict security of the authentication or key exchange protocol, it cannot perform the verification according to the level of security.

  Therefore, an object of the present invention is to provide a verification device, a verification method, and a verification program that can verify an authentication or key exchange protocol according to a level of security.

  The present invention provides the following solutions.

(1) A verification device for verifying the security of an authentication or key exchange protocol,
Verification items for satisfying the requirements for security against offline dictionary attacks in the authentication protocol, security against undetectable online dictionary attacks, and security against key leakage spoofing attacks, and detection failure in the key exchange protocol Security items for possible online dictionary attacks, security against unknown key agreement attacks, strong forward secrecy, weak backward secrecy, and verification items to satisfy the requirements of weak backward secrecy A storage unit
A type setting unit for setting the type of cryptographic primitive used in the protocol;
A role setting unit for setting the role of the cryptographic primitive whose type is set by the type setting unit;
A data setting unit for setting the type and state of flow data in the protocol or the type and state of arguments of cryptographic primitives;
A safety selection unit that selects the safety to be verified upon request;
The verification items relating to each of the safety selected by the safety selection unit are extracted from the storage unit, and the verification items are satisfied based on the type and role of the cryptographic primitive and the data set by the data setting unit A verification item determination unit for determining whether or not,
A verification apparatus comprising: a safety determination unit that determines that the protocol is safe when the verification item determination unit determines that all the selected verification items related to safety are satisfied.

(2) Security verification items against offline dictionary attacks in the authentication protocol are:
The cryptographic primitive that appears on the flow containing the long-term incomplete secret information that can be used repeatedly and secretly in another session is a symmetric key encryption or message authentication code scheme, or
A cryptographic primitive that appears on a flow containing long-term incomplete secret information that can be used repeatedly and secretly in another session is encryption using a password, public key cryptography, or hash function, and the cryptographic primitive The verification apparatus according to (1), wherein the argument includes temporary secret information that first appears in a secret state or temporary secret information that has appeared in a secret state before in the same session.

(3) Security verification items against undetectable online dictionary attacks in the authentication protocol are:
The cryptographic primitive that appears on a flow containing long-term incomplete secret information that can be used repeatedly and secretly in another session is a common key cipher, public key cipher or message authentication code scheme (1 ) Or the verification device according to (2).

(4) The security verification item against the key leakage spoofing attack in the authentication protocol is as follows:
The cryptographic primitive to be authenticated is a public key cryptography or digital signature scheme, and the temporary public information that the argument of the cryptographic primitive first appeared in the public state, the temporary that appeared in the public state before in the same session Public information, temporary secret information that first appeared in a secret state, or temporary secret information that appeared previously in a secret state in the same session, or
The cryptographic primitive to be authenticated is a Diffie-Hellman family or a hash function, and temporary secret information that the argument of the cryptographic primitive first appeared in a secret state, or a temporary that appeared in a secret state before in the same session The verification apparatus according to any one of (1) to (3), wherein the confidential information is included.

(5) Verification items for security against undetectable online dictionary attacks in the key exchange protocol are:
The cryptographic primitive that appears on a flow containing long-term incomplete secret information that can be used repeatedly and secretly in another session is a common key cipher, public key cipher or message authentication code scheme (1 The verification apparatus according to any one of (4) to (4).

(6) The security verification item against the unknown key sharing attack in the key exchange protocol is:
The cryptographic primitive that is the key generation target in the protocol is a common key cryptography, encryption using a password, a digital signature scheme or a message authentication code scheme, and an argument of the cryptographic primitive can be repeatedly used in another session and is in a public state Specific public information that appeared in, temporary public information that first appeared in the public state, temporary public information that appeared in the public state before in the same session, temporary secret information that first appeared in the secret state or the same session Contains temporary secret information that appeared in a secret state in the past, or
Cryptographic primitives that are key generation targets in the protocol are public key cryptography or hash functions, and the arguments of the cryptographic primitives can be used repeatedly in different sessions and appear in public state for the first time in secret state. Contain temporary secret information that has been created or has been previously secretly revealed in the same session, or
The cryptographic primitive included in the argument of the cryptographic primitive that is the key generation target in the protocol is the common key encryption, the encryption using the password, the digital signature scheme or the message authentication code scheme, and the cryptographic primitive argument included in the argument Specific public information that can be used repeatedly in another session and appeared in public status, temporary public information that first appeared in public status, temporary public information that appeared in public status in the same session, in secret status Contains temporary confidential information that first appeared or temporary confidential information that appeared in a secret state in the same session, or
The cryptographic primitive included in the argument of the cryptographic primitive that is the key generation target in the protocol is a public key cryptography or hash function, and the cryptographic primitive argument included in the argument can be repeatedly used in another session and appears in a public state Any one of (1) to (5) including the specified public information and the temporary secret information first appearing in the secret state or the temporary secret information previously appearing in the same session in the same session The verification device according to the above.

(7) The strong forward secrecy verification item in the key exchange protocol is:
The cryptographic primitive that is the key generation target in the protocol is public key cryptography, Diffie-Hellman family, hash function, or message authentication code scheme, and the temporary primitive information or the same that the argument of the cryptographic primitive first appears in a secret state or the same Contains temporary secret information that appeared in a secret state before in the session, or
The cryptographic primitive that is the key generation target in the protocol is a hash function or a message authentication code scheme, and the cryptographic primitive included in the argument of the cryptographic primitive that is the key generation target in the protocol is the Diffie-Hellman family, and the argument (1) to (6) that the argument of the cryptographic primitive included in includes the temporary secret information that first appeared in the secret state or the temporary secret information that appeared in the secret state before in the same session. The verification apparatus in any one of.

(8) The verification item of weak backward secrecy in the key exchange protocol is:
The cryptographic primitive that is the key generation target in the protocol is public key cryptography, Diffie-Hellman family, hash function, or message authentication code scheme, and the temporary primitive information or the same that the argument of the cryptographic primitive first appears in a secret state or the same Contains temporary secret information that appeared in a secret state before in the session, or
The cryptographic primitive that is the key generation target in the protocol is a common key encryption, encryption using a password, public key encryption, hash function, or message authentication code scheme, and the encryption primitive that is the key generation target in the protocol is an argument Temporary secret information that the cryptographic primitive included is the Diffie-Hellman family and the argument of the cryptographic primitive included in the argument first appeared in a secret state, or temporary secret information previously appeared in a secret state in the same session The verification apparatus according to any one of (1) to (7).

(9) A verification method in which a computer verifies the security of an authentication or key exchange protocol,
The computer includes verification items for satisfying the requirements of security against offline dictionary attacks in the authentication protocol, security against undetectable online dictionary attacks, and security against key leakage spoofing attacks, and the key exchange. Verification items to satisfy the requirements for security against undetectable online dictionary attacks in the protocol, security against unknown key sharing attacks, strong forward secrecy, and weak backward secrecy And a storage unit for storing
A type setting step for setting the type of cryptographic primitive used in the protocol;
A role setting step for setting the role of the cryptographic primitive whose type is set by the type setting step;
A data setting step for setting the type and state of flow data in the protocol or the type and state of arguments of cryptographic primitives;
A safety selection step for selecting the safety to be verified upon request;
The verification items related to the respective safety selected in the security selection step are extracted from the storage unit, and the verification items are satisfied based on the type and role of the cryptographic primitive and the data set in the data setting step. A verification item determination step for determining whether or not,
A verification method comprising: a safety determination step that determines that the protocol is safe when it is determined in the verification item determination step that all the selected safety verification items are satisfied.

(10) A verification program for causing a computer to verify the security of an authentication or key exchange protocol,
The computer includes verification items for satisfying the requirements of security against offline dictionary attacks in the authentication protocol, security against undetectable online dictionary attacks, and security against key leakage spoofing attacks, and the key exchange. Verification items to satisfy the requirements for security against undetectable online dictionary attacks in the protocol, security against unknown key sharing attacks, strong forward secrecy, and weak backward secrecy And a storage unit for storing
A type setting step for setting the type of cryptographic primitive used in the protocol;
A role setting step for setting the role of the cryptographic primitive whose type is set by the type setting step;
A data setting step for setting the type and state of flow data in the protocol or the type and state of arguments of cryptographic primitives;
A safety selection step for selecting the safety to be verified upon request;
The verification items related to the respective safety selected in the security selection step are extracted from the storage unit, and the verification items are satisfied based on the type and role of the cryptographic primitive and the data set in the data setting step. A verification item determination step for determining whether or not,
A verification program for executing a safety determination step for determining that the protocol is safe when it is determined in the verification item determination step that all the selected safety verification items are satisfied.

  According to the present invention, the authentication or key exchange protocol can be verified according to the level of security.

It is a figure which shows the structure of the verification apparatus which concerns on embodiment of this invention. It is a flowchart which shows the flow of the verification method which concerns on embodiment of this invention.

  Hereinafter, an example of an embodiment of the present invention will be described.

<Security model>
First, a security model related to the security level of an authentication or key exchange protocol is shown. In the present embodiment, a concept called “provable security” that proves the security of an authentication or key exchange protocol based on the computational complexity theory is used. “The authentication or key exchange protocol has provable security” means that the security of the authentication or key exchange protocol can be proved theoretically that the security of a certain cryptographic primitive results in security. Is shown. That is, an attacker who can break a certain authentication or key exchange protocol can prove that if this cryptographic primitive is not breached by proving that it can construct a machine that breaks a certain cryptographic primitive in polynomial time, Prove that the key exchange protocol is not broken.

  In the provable security described above, there is a security concept of matching conversion in the authentication protocol and semantic security in the key exchange protocol. For each concept, the following security requirements exist for authentication or key exchange protocols:

(1) matching conversion
This security indicates that in the authentication protocol, the attacker can do nothing but send the message received from one party as it is to the other party. That is, it indicates that the attacker cannot perform fraud such as tampering with a message, sending a new message, blocking a message, and changing the order of messages.

(1A) Security against offline dictionary attack This indicates that an attacker cannot search for a password of a party that matches the past history offline from a password guessing dictionary.

(1B) Security against undetectable online dictionary attack This means that it is possible to detect that an attacker is inquiring about a password to a party that has registered a password.

(1C) Security against key leakage / spoofing attacks Even if an attacker can obtain a long-term key of a party such as a common key of a common key cipher, a password, a secret key of a public key cipher, etc., Indicates that it cannot be impersonated.

(2) semantic security
This security indicates that in a key exchange protocol, an attacker cannot obtain any information about the session key. That is, the attacker cannot distinguish the session key and the random number in polynomial time.

(2A) Security against undetectable online dictionary attack This means that it is possible to detect that an attacker is inquiring about a password to a party that has registered a password.

(2B) Security against unknown key sharing attack This means that a session key cannot be shared with a party other than a party that a certain party thinks is correct.

(2C) strong forward secrecy
Even if an attacker can obtain the party's long-term key and internal state, such as a common key for common key cryptography, a secret key for public key cryptography, and a public key cryptography, it cannot obtain a session key shared before that Indicates.

(2D) weak backing secrecy
This indicates that even if an attacker can obtain a party long-term key such as a common key for common key cryptography, a password, and a secret key for public key cryptography, it cannot obtain a session key shared thereafter.

  However, in the case of an authentication or key exchange protocol that does not use a long-term key, (1C) security against key leakage spoofing attacks, (2C) strong forward secrecy, and (2D) weak backing secrecy are not required. In particular, in the case of an authentication or key exchange protocol that does not use a password, (1A) security against offline dictionary attacks, (1B) security against undetectable online dictionary attacks, (2A) against undetectable online dictionary attacks Safety is not required.

Here, the types of cryptographic primitives used in the authentication or key exchange protocol are as follows. Note that the parentheses are abbreviations indicating the respective encryption primitives.
[Common key cryptosystem]
・ Common key encryption (SKE)
・ Encryption using password (PWE)
[Public key cryptosystem]
・ Public key cryptography (PKE)
・ Diffie-Hellman family (DH)
・ Digital Signature Scheme (SIG)
[Hash function system]
・ Hash function (HF)
Message authentication code scheme (MAC)

The roles set for the above-mentioned cryptographic primitives are as follows. The parentheses are abbreviations indicating the roles.
-Cryptographic primitives (AGF) to be authenticated in the authentication protocol
-Cryptographic primitives (KGF) that are key generation targets in the key exchange protocol
-Cryptographic primitives (ACP) included in AGF and KGF arguments
-Cryptographic primitives (OCP) appearing on the flow

Further, the elements set for the flow data in the authentication or key exchange protocol or for the argument of the cryptographic primitive are as follows. The parentheses are abbreviations that indicate the type or state of each flow data or each argument.
[Types set for flow data and cryptographic primitive arguments]
・ Public information (PUB)
・ Specific public information (ID)
・ Temporary public information (TPK)
・ Long-term and complete confidential information (LLK)
・ Long-term and incomplete confidential information (PW)
・ Temporary confidential information (TSK)
[State set in flow data and cryptographic primitive arguments]
・ First appearance in public state (PFT)
-Previously published in the same session (PSS)
・ Repeatedly available in different sessions and publicly available (PRS)
・ First appearance in a secret state (SFT)
・ Appeared in secret before in the same session (SSS)
-Appears in a secret state that can be used repeatedly in different sessions (SRS)

<Verification items>
Next, verification items for the security of the authentication or key exchange protocol will be described. In the present embodiment, the authentication or key exchange protocol at two parties (between two users, between a server and a client, etc.) is targeted, and the following three points are assumed.

-If a secret key or password is used in an authentication or key exchange protocol, the two parties must share the same secret key or password in advance using some secure procedure, and the procedure is not vulnerable. To do.
・ If a public key is used in the authentication or key exchange protocol, each party can confirm the validity of the public key certificate with a third party such as a certificate authority. Is not vulnerable.
When the cryptographic primitive is compromised, the verification apparatus 1 can obtain and record the information in real time.

  The verification items for verifying the security of the authentication or key exchange protocol according to the level, that is, the type of security will be described below.

(1) Matching conversion for authentication protocol
(1A) Verification items in security against offline dictionary attack (Setting information related to attack) All flows (1A-a) OCP including PW-SRS is SKE or MAC.
(1A-b) OCP including PW-SRS is PWE, PKE, or HF, and the argument of OCP includes TSK-SFT or TSK-SSS.

(1B) Verification items in security against undetectable online dictionary attack (Setting information related to attack) All flows (1B-a) OCP including PW-SRS is SKE, PKE or MAC.

(1C) Verification item in security against key leakage spoofing attack (Setting information related to attack) Long-term key of one party (1C-a) AGF is PKE or SIG, and AGF argument is TPK-PFT or TPK- Includes PSS or TSK-SFT or TSK-SSS.
(1C-b) AGF is DH or HF, and the argument of AGF includes TSK-SFT or TSK-SSS.

(2) semantic security for key exchange protocol
(2A) Verification items in security against undetectable online dictionary attack (Setting information related to attack) All flows (2A-a) OCP including PW-SRS is SKE, PKE or MAC.

(2B) Verification items in security against unknown key sharing attack (Setting information related to attack) All flows (2B-a) KGF is SKE, PWE, SIG or MAC, and the argument of KGF is ID-PRS and ( TPK-PFT or TPK-PSS or TSK-SFT or TSK-SSS).
(2B-b) KGF is PKE or HF, and the argument of KGF includes ID-PRS and (TSK-SFT or TSK-SSS).
(2B-c) ACP is SKE or PWE or SIG or MAC, and the argument of ACP includes ID-PRS and (TPK-PFT or TPK-PSS or TSK-SFT or TSK-SSS).
(2B-d) ACP is PKE or HF, and the argument of ACP includes ID-PRS and (TSK-SFT or TSK-SSS).

(2C) Verification items in strong forward secrecy (Setting information related to attack) All long-term keys and internal state (2C-a) KGF is PKE, DH, HF or MAC, and KGF argument is TSK-SFT or TSK -Includes SSS.
(2C-b) KGF is HF or MAC, ACP is DH, and the argument of ACP includes TSK-SFT or TSK-SSS.

(2D) Verification items in weak backup secrecy (Setting information related to attack) All long-term keys (2D-a) KGF is PKE, DH, HF or MAC, and the argument of KGF is TSK-SFT or TSK-SSS Contains.
(2D-b) KGF is SKE or PWE or PKE or HF or MAC, ACP is DH, and the argument of ACP includes TSK-SFT or TSK-SSS.

<Configuration of verification device>
FIG. 1 is a diagram showing a configuration of a verification apparatus 1 that verifies the security of an authentication or key exchange protocol according to the present embodiment.
The verification device 1 includes a control unit 10, a storage unit 20, an input unit 30, and a display unit 40.

  The control unit 10 is a part that controls the entire verification apparatus 1, and appropriately reads and executes various programs stored in the storage unit 20, thereby cooperating with the above-described hardware and various functions according to the present invention. Is realized. The control unit 10 may be a CPU (Central Processing Unit).

  The storage unit 20 stores various programs for causing the hardware group to function as the verification device 1, programs for causing the control unit 10 to execute the functions of the present invention, a database, and the like. Specifically, the storage unit 20 stores the types and roles of the above-described cryptographic primitives, the types and states of the arguments of the flow data or the cryptographic primitives, and further, each of the above-described security and its verification items. . The storage unit 20 also stores information obtained by the control unit 10 via the input unit 30 or a predetermined network and indicating that each cryptographic primitive has been compromised. The storage unit 20 may be configured by any of various storage devices such as a hard disk, an optical disk drive, or a semiconductor memory.

  The input unit 30 is an interface device that receives an instruction input from a user (an administrator of the verification device 1) to the verification device 1. The input unit 30 is configured by, for example, a keyboard and a mouse.

  The display unit 40 displays a screen for accepting data input to the user (administrator of the verification device 1) or displays a screen of a processing result by the verification device 1. The display unit 40 may be a display device such as a cathode ray tube display device (CRT) or a liquid crystal display device (LCD).

  The computer referred to in the present invention is an information processing apparatus including a control device, a storage device, and the like. The verification apparatus 1 is an information processing apparatus including a control unit 10, a storage unit 20, and the like.

  In addition, the control unit 10 includes a protocol reception unit 101, a cryptographic primitive enumeration unit 102, a compromise information determination unit 103, a type setting unit 104, a role setting unit 105, a flow enumeration unit 106, and a data setting unit 107. A safety selection unit 108, a verification item determination unit 109, and a safety determination unit 110.

  Based on the instruction input from the input unit 30, the protocol receiving unit 101 receives input of specification data of an authentication or key exchange protocol that is a security verification target.

  The cryptographic primitive listing unit 102 lists all the cryptographic primitives used in this protocol from the protocol specification data received by the protocol receiving unit 101.

  The compromise information determination unit 103 determines whether there is compromise information for the cryptographic primitives enumerated by the cryptographic primitive enumeration unit 102. When there is even one piece of compromise information, the safety determination unit 110 determines that the protocol is not safe.

  The type setting unit 104 selects and sets the types of cryptographic primitives enumerated by the cryptographic primitive enumeration unit 102 from the above-described SKE, PWE, PKE, DH, SIG, HF, and MAC.

  The role setting unit 105 selects and sets the role of the cryptographic primitive whose type is selected by the type setting unit 104 from the above-described AGF, KGF, ACP, and OCP.

  The flow listing unit 106 lists all the flows in the verification target protocol received by the protocol receiving unit 101.

  The data setting unit 107 selects the type of flow data and cryptographic primitive arguments enumerated by the flow enumeration unit 106 from the above-mentioned PUB, ID, TPK, LLK, PW, and TSK according to the protocol specifications. In addition, the state is selected and set from the above-mentioned PFT, PSS, PRS, SFT, SSS, and SRS.

  Here, the types and states of the arguments of the flow data and the cryptographic primitive are set in the order of the enumerated protocol flows. The state is updated according to the previous flow in the session. In the public state and the secret state, the public state has priority.

  The safety selection unit 108 selects the safety requested for the verification target protocol received by the protocol reception unit 101. Specifically, a selection input from the above-described (1A), (1B), (1C), (2A), (2B), (2C), and (2D) is received via the input unit 30. Note that there may be a plurality of selected safety, and it is preferable to select the minimum safety required for operating the protocol.

  The verification item determination unit 109 uses the information set by the type setting unit 104, the role setting unit 105, and the data setting unit 107 to store the above-described verification items for each safety selected by the safety selection unit 108. 20 is read and verified.

  Further, the verification item determination unit 109 sets security parameters (for example, key size) required in the protocol. Check whether the size of the flow, cryptographic primitive, and argument satisfies the set security parameters, and if there is even one size that is not satisfied, the security determination unit 110 determines that the protocol is not secure Is done.

  The safety determination unit 110 determines that the protocol is safe when the verification item determination unit 109 determines that the verification items are satisfied for all the safety selected by the safety selection unit 108. . On the other hand, if there is even one safety that does not satisfy the verification item, the safety determination unit 110 determines that the protocol is not safe.

<Processing flow>
FIG. 2 is a flowchart showing the flow of the verification method executed by the control unit 10 of the verification apparatus 1 according to this embodiment.

  In step S1, the control unit 10 lists all cryptographic primitives used in the accepted authentication or key exchange protocol.

  In step S2, the control unit 10 determines whether or not compromise information is stored for the cryptographic primitives listed in step S1. If this determination is YES, the process proceeds to step S3, and if the determination is NO, the process proceeds to step S10.

  In step S3 (type setting step), the control unit 10 determines and sets the types of cryptographic primitives listed in step S1 by comparing with the information stored in the storage unit 20.

  In step S4 (role setting step), the control unit 10 determines and sets the role of the cryptographic primitive whose type is set in step S3 by comparing it with the information stored in the storage unit 20.

  In step S5, the control unit 10 lists all the flows in the accepted authentication or key exchange protocol.

  In step S6 (data setting step), the control unit 10 compares the flow data of the flow listed in step S5 and the arguments of the cryptographic primitive with the information stored in the storage unit 20 according to the protocol specifications. To determine and set the type and status.

  In step S <b> 7 (security selection step), the control unit 10 selects the security requested for the accepted authentication or key exchange protocol from the predetermined types stored in the storage unit 20. .

  In step S8 (verification item determination step), the control unit 10 uses the information set in step S3, step S4, and step S6 to store verification items for each safety selected in step S7 from the storage unit 20. Verify reading. And the control part 10 determines whether the verification item is satisfied regarding all the safety | security selected by step S7. If this determination is YES, the process proceeds to step S9, and if the determination is NO, the process proceeds to step S10.

  In step S9 (security determination step), the control unit 10 determines that this protocol is safe because the authentication or key exchange protocol to be verified satisfies all the required security.

  In step S10 (security determination step), the control unit 10 determines that the cryptographic primitive has been compromised in step S2 or the verification target protocol does not satisfy the required security. Determine that this protocol is not secure.

  This process can also be performed by software. When a series of processing is performed by software, a program constituting the software is installed in the computer. The program may be recorded on a removable medium such as a CD-ROM and distributed to the user, or may be distributed by being downloaded to the user's computer via a network.

  As described above, according to the present embodiment, it is possible to select the required security for the authentication or key exchange protocol and verify the security. That is, according to this embodiment, the authentication or key exchange protocol can be verified according to the level of security.

  As mentioned above, although embodiment of this invention was described, this invention is not restricted to embodiment mentioned above. The effects described in the embodiments of the present invention are only the most preferable effects resulting from the present invention, and the effects of the present invention are limited to those described in the embodiments of the present invention. is not.

DESCRIPTION OF SYMBOLS 1 Verification apparatus 10 Control part 20 Storage part 30 Input part 40 Display part 101 Protocol reception part 102 Cryptographic primitive enumeration part 103 Compromise information determination part 104 Type setting part 105 Role setting part 106 Flow enumeration part 107 Data setting part 108 Safety selection Part 109 Verification item judgment part 110 Safety judgment part

Claims (10)

A verification device for verifying the security of an authentication or key exchange protocol,
Verification items for satisfying the requirements for security against offline dictionary attacks in the authentication protocol, security against undetectable online dictionary attacks, and security against key leakage spoofing attacks, and detection failure in the key exchange protocol Security items for possible online dictionary attacks, security against unknown key agreement attacks, strong forward secrecy, weak backward secrecy, and verification items to satisfy the requirements of weak backward secrecy A storage unit
A type setting unit for setting the type of cryptographic primitive used in the protocol;
A role setting unit for setting the role of the cryptographic primitive whose type is set by the type setting unit;
A data setting unit for setting the type and state of flow data in the protocol or the type and state of arguments of cryptographic primitives;
A safety selection unit that selects the safety to be verified upon request;
The verification items relating to each of the safety selected by the safety selection unit are extracted from the storage unit, and the verification items are satisfied based on the type and role of the cryptographic primitive and the data set by the data setting unit A verification item determination unit for determining whether or not,
A verification apparatus comprising: a safety determination unit that determines that the protocol is safe when the verification item determination unit determines that all the selected verification items related to safety are satisfied. Security verification items against offline dictionary attacks in the authentication protocol are:
The cryptographic primitive that appears on the flow containing the long-term incomplete secret information that can be used repeatedly and secretly in another session is a symmetric key encryption or message authentication code scheme, or
A cryptographic primitive that appears on a flow containing long-term incomplete secret information that can be used repeatedly and secretly in another session is encryption using a password, public key cryptography, or hash function, and the cryptographic primitive The verification apparatus according to claim 1, wherein the argument includes temporary secret information that has first appeared in a secret state or temporary secret information that has previously appeared in a secret state in the same session. Security verification items against undetectable online dictionary attacks in the authentication protocol are:
Cryptographic primitives appearing on a flow containing long-term incomplete secret information that can be used repeatedly and secretly in another session are symmetric, public key or message authentication code schemes. The verification device according to claim 1 or 2. The security verification item against the key leakage spoofing attack in the authentication protocol is as follows:
The cryptographic primitive to be authenticated is a public key cryptography or digital signature scheme, and the temporary public information that the argument of the cryptographic primitive first appeared in the public state, the temporary that appeared in the public state before in the same session Public information, temporary secret information that first appeared in a secret state, or temporary secret information that appeared previously in a secret state in the same session, or
The cryptographic primitive to be authenticated is a Diffie-Hellman family or a hash function, and temporary secret information that the argument of the cryptographic primitive first appeared in a secret state, or a temporary that appeared in a secret state before in the same session The verification apparatus according to claim 1, wherein the secret information is included. Security verification items against undetectable online dictionary attacks in the key exchange protocol are:
Cryptographic primitives appearing on a flow containing long-term incomplete secret information that can be used repeatedly and secretly in another session are symmetric, public key or message authentication code schemes. The verification device according to claim 1. Verification items for security against unknown key sharing attacks in the key exchange protocol are:
The cryptographic primitive that is the key generation target in the protocol is a common key cryptography, encryption using a password, a digital signature scheme or a message authentication code scheme, and an argument of the cryptographic primitive can be repeatedly used in another session and is in a public state Specific public information that appeared in, temporary public information that first appeared in the public state, temporary public information that appeared in the public state before in the same session, temporary secret information that first appeared in the secret state or the same session Contains temporary secret information that appeared in a secret state in the past, or
Cryptographic primitives that are key generation targets in the protocol are public key cryptography or hash functions, and the arguments of the cryptographic primitives can be used repeatedly in different sessions and appear in public state for the first time in secret state. Contain temporary secret information that has been created or has been previously secretly revealed in the same session, or
The cryptographic primitive included in the argument of the cryptographic primitive that is the key generation target in the protocol is the common key encryption, the encryption using the password, the digital signature scheme or the message authentication code scheme, and the cryptographic primitive argument included in the argument Specific public information that can be used repeatedly in another session and appeared in public status, temporary public information that first appeared in public status, temporary public information that appeared in public status in the same session, in secret status Contains temporary confidential information that first appeared or temporary confidential information that appeared in a secret state in the same session, or
The cryptographic primitive included in the argument of the cryptographic primitive that is the key generation target in the protocol is a public key cryptography or hash function, and the cryptographic primitive argument included in the argument can be repeatedly used in another session and appears in a public state 6. Any one of claims 1 to 5, comprising: the specified public information and the temporary secret information first appearing in the secret state or the temporary secret information previously appearing in the secret state in the same session. The verification device according to the above. The verification items of strong forward secrecy in the key exchange protocol are as follows:
The cryptographic primitive that is the key generation target in the protocol is public key cryptography, Diffie-Hellman family, hash function, or message authentication code scheme, and the temporary primitive information or the same that the argument of the cryptographic primitive first appears in a secret state or the same Contains temporary secret information that appeared in a secret state before in the session, or
The cryptographic primitive that is the key generation target in the protocol is a hash function or a message authentication code scheme, and the cryptographic primitive included in the argument of the cryptographic primitive that is the key generation target in the protocol is the Diffie-Hellman family, and the argument The argument of the cryptographic primitive included in the information includes temporary secret information that first appeared in a secret state or temporary secret information that appeared previously in a secret state in the same session. The verification apparatus in any one of. The verification item of weak backward secrecy in the key exchange protocol is:
The cryptographic primitive that is the key generation target in the protocol is public key cryptography, Diffie-Hellman family, hash function, or message authentication code scheme, and the temporary primitive information or the same that the argument of the cryptographic primitive first appears in a secret state or the same Contains temporary secret information that appeared in a secret state before in the session, or
The cryptographic primitive that is the key generation target in the protocol is a common key encryption, encryption using a password, public key encryption, hash function, or message authentication code scheme, and the encryption primitive that is the key generation target in the protocol is an argument Temporary secret information that the cryptographic primitive included is the Diffie-Hellman family and the argument of the cryptographic primitive included in the argument first appeared in a secret state, or temporary secret information previously appeared in a secret state in the same session The verification apparatus according to claim 1, wherein the verification apparatus includes: A verification method in which a computer verifies the security of an authentication or key exchange protocol,
The computer includes verification items for satisfying the requirements of security against offline dictionary attacks in the authentication protocol, security against undetectable online dictionary attacks, and security against key leakage spoofing attacks, and the key exchange. Verification items to satisfy the requirements for security against undetectable online dictionary attacks in the protocol, security against unknown key sharing attacks, strong forward secrecy, and weak backward secrecy And a storage unit for storing
A type setting step for setting the type of cryptographic primitive used in the protocol;
A role setting step for setting the role of the cryptographic primitive whose type is set by the type setting step;
A data setting step for setting the type and state of flow data in the protocol or the type and state of arguments of cryptographic primitives;
A safety selection step for selecting the safety to be verified upon request;
The verification items related to the respective safety selected in the security selection step are extracted from the storage unit, and the verification items are satisfied based on the type and role of the cryptographic primitive and the data set in the data setting step. A verification item determination step for determining whether or not,
The computer executes a safety determination step for determining that the protocol is safe when it is determined in the verification item determination step that all the selected safety verification items are satisfied. Method of verification. A verification program for causing a computer to verify the security of an authentication or key exchange protocol,
The computer includes verification items for satisfying the requirements of security against offline dictionary attacks in the authentication protocol, security against undetectable online dictionary attacks, and security against key leakage spoofing attacks, and the key exchange. Verification items to satisfy the requirements for security against undetectable online dictionary attacks in the protocol, security against unknown key sharing attacks, strong forward secrecy, and weak backward secrecy And a storage unit for storing
A type setting step for setting the type of cryptographic primitive used in the protocol;
A role setting step for setting the role of the cryptographic primitive whose type is set by the type setting step;
A data setting step for setting the type and state of flow data in the protocol or the type and state of arguments of cryptographic primitives;
A safety selection step for selecting the safety to be verified upon request;
The verification items related to the respective safety selected in the security selection step are extracted from the storage unit, and the verification items are satisfied based on the type and role of the cryptographic primitive and the data set in the data setting step. A verification item determination step for determining whether or not,
In order to cause a computer to execute a safety determination step of determining that the protocol is safe when it is determined in the verification item determination step that all the selected safety verification items are satisfied. of the verification program.

Images