JP5511926B2 - Cryptographic protocol security verification device, security verification method and program - Google Patents

Description

  The present invention relates to a cryptographic protocol having a security function such as authentication and key sharing, and relates to a cryptographic protocol safety verification device, a security verification method, and a program for verifying the security of such a cryptographic protocol.

  Conventionally, a secure cryptographic protocol has been proposed empirically based on a heuristic approach based on insight of security and cryptographic technology possessed by a protocol designer. However, there were some cases where security vulnerabilities were pointed out after the proposed cryptographic protocol specifications were made public. In fact, when vulnerabilities are discovered after standardized cryptographic protocols have been widely disseminated through products and the like, the cost associated with refurbishment becomes a major problem.

  In particular, when a fatal vulnerability is discovered, it is necessary to urgently deal with such issues as applying software patches and replacing hardware chips and components in order to avoid economic damage. Therefore, the more popular the proposed cryptographic protocol and related products, the greater the social impact, and in some cases, the entire system may fail.

  For this reason, the descriptions described in Patent Document 1 and Patent Document 2 disclose an apparatus, a method, and a program for verifying the security of a cryptographic protocol using a concept called “general-linkable security”. Here, “general-linkable security” means that a cryptographic protocol is safe if the cryptographic protocol safely realizes an ideal function related to the security function. For example, if a key exchange protocol securely implements the key exchange ideal function, the key exchange protocol has been shown to be secure.

JP 2007-28447 A JP 2008-35117 A

  The “general connectable safety” used in the above prior art documents 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 cryptographic protocol safely realizes its ideal function, this cryptographic protocol satisfies all the security required for the security function.

  However, the security and efficiency of the cryptographic protocol are in a trade-off relationship, and the efficiency decreases as the security of the cryptographic protocol increases. Therefore, when importance is attached to the efficiency of the cryptographic protocol, it is desired to reduce the security to an allowable range. However, in the above prior art, although it is possible to verify the strict security of the cryptographic protocol, it is not possible to perform verification according to the security level.

  Therefore, the present invention has been made in view of the above-described problems, and provides a cryptographic protocol safety verification device, a security verification method, and a program capable of verifying a cryptographic protocol according to a safety level. With the goal.

  The present invention proposes the following matters in order to solve the above problems.

(1) The present invention relates to a key exchange protocol of a cryptographic protocol having at least a key sharing security function, such as active attack safety, passive attack safety, offline dictionary attack safety, known key attack safety, forward secrecy of the key exchange protocol. the verification items in, e Bei verification means for checking a verification item to verify the safety of the key exchange protocol, as verification item in active attacks safety of the key exchange protocol, the argument of cryptographic primitives that the key generation target The included cryptographic primitives are indistinguishable or one-way in nature, and any arguments of the cryptographic primitives are temporary secret information that appears for the first time in the protocol, and can be used repeatedly in different sessions and appear in the protocol. Long-term complete confidential information or long-term incomplete confidential information Dolphins, proposes a security verification system of the cryptographic protocol, characterized in that to check.

(2) The present invention relates to a key exchange protocol of a cryptographic protocol having at least a key sharing security function, such as active attack safety, passive attack safety, offline dictionary attack safety, known key attack safety, forward secrecy of the key exchange protocol. in the verification items, comprising a verification means for checking a verification item to verify the safety of the key exchange protocol, as verification item in receiving dynamic attack safety of the key exchange protocol, encryption primitive Unidentified the key generation target The encryption primitive has temporary secret information that appears for the first time in the protocol , or the encryption primitive to be generated has a one-way property, The cryptographic primitive included in the argument of the cryptographic primitive has the property of being indistinguishable, and Primitive argument has proposed a safety verification device of the cryptographic protocol, characterized in that the check, it includes a temporary secret information for the first time appeared in the protocol.

(3) The present invention relates to a key exchange protocol of a cryptographic protocol having at least a key sharing security function, and an active attack safety, a passive attack safety, an offline dictionary attack safety, a known key attack safety, a forward secrecy of the key exchange protocol. A verification means for checking the verification item in the key exchange protocol as a verification item for verifying the security of the key exchange protocol, and encryption including long-term and incomplete secret information as a verification item in the off-line dictionary attack security of the key exchange protocol The primitive has a one-way nature and any of the cryptographic primitive arguments first appeared in the protocol, previously appeared in the protocol in the same session, or temporarily unavailable in another session and appeared in the protocol That it contains sensitive confidential information It proposes a security verification system of the cryptographic protocol, characterized.

(4) The present invention relates to a key exchange protocol that is a cryptographic protocol having at least a key sharing security function, such as active attack safety, passive attack safety, offline dictionary attack safety, known key attack safety, forward secrecy of the key exchange protocol. A verification means for checking the verification item in the key exchange protocol as a verification item for verifying the security of the key exchange protocol, and a cryptographic primitive that is a key generation target can not be identified as a verification item in the known key attack security of the key exchange protocol A temporary or unidirectional property in which any argument of the cryptographic primitive first appears in the protocol, previously appeared in the protocol in the same session, or repeatedly unavailable in another session and appeared in the protocol To check whether it contains sensitive confidential information It has proposed a safety verification device of the cryptographic protocols that.

(5) The present invention relates to a key exchange protocol of a cryptographic protocol having at least a key sharing security function, and an active attack safety, a passive attack safety, an offline dictionary attack safety, a known key attack safety, a forward secrecy of the key exchange protocol. A verification means for checking the verification item in the key exchange protocol as a verification item for verifying the security of the key exchange protocol, and as a verification item in the forward secrecy of the key exchange protocol, the cryptographic primitive that is the key generation target cannot be identified Or have a one-way nature, and any of the cryptographic primitive arguments appear in the protocol for the first time, appear in the protocol earlier in the same session, or are temporarily unavailable in another session and appear in the protocol Check to see if it contains confidential information It has proposed a safety verification device of the cryptographic protocols that butterflies.

(6) The present invention provides a definitive safety verification device security verification method for verifying the security of the cryptographic protocol, the security verification apparatus, a cryptographic primitives enumerated means, and compromise information determining means A role setting means, a safety ground setting means, a flow enumeration means, an argument setting means, a setting information determination means, a safety selection means, a verification item determination means, and a safety determination means, A first step in which the cryptographic primitive enumeration means enumerates cryptographic primitives used in a key exchange protocol; and the compromise information determination means verifies the presence or absence of compromise information for the enumerated cryptographic primitives; A second step of determining that the cryptographic protocol is not secure if there is compromise information, and the role setting means If there is no compromise that has compromise information, the third step of setting the role of the cryptographic primitive and the security rationale setting means set the security rationale of the cryptographic primitive A fourth step, a fifth step in which the flow enumeration means enumerates flows, and a sixth step in which the argument setting means sets the type and state of flow data and arguments of cryptographic primitives, The setting information determination means determines whether or not the relationship between the set flow data and the type and state of the argument of the cryptographic primitive is correct, and determines that the cryptographic protocol is not secure when it includes an incorrect one. And the security selecting means determines that all the relations between the set flow data and the types and states of the cryptographic primitive arguments are correct. In this case, an eighth step of selecting a verification item related to security from among verification items for active attack safety, passive attack security, offline dictionary attack security, known key attack security, and forward secrecy of the key exchange protocol. The verification item determination means determines whether or not all of the selected verification items are satisfied. And a tenth step of determining that the cryptographic protocol is safe when the security determination means satisfies all of the selected verification items;
A safety verification method characterized by having

(7) The present invention is a program for causing a computer to execute a security verification method in a security verification apparatus for verifying the security of a cryptographic protocol, wherein the security verification apparatus includes cryptographic primitive enumeration means. Compromise information determination means, role setting means, safety ground setting means, flow enumeration means, argument setting means, setting information determination means, safety selection means, verification item determination means, safety A first step of enumerating the cryptographic primitives used in the key exchange protocol, and the compromise information determining means for the enumerated cryptographic primitives. The second step is to determine whether the cryptographic protocol is insecure if there is any information that has compromise information. When the role setting means, in a cryptographic primitives said listed, if there is no one having a compromise information, a third step of setting the role of the cryptographic primitives, said safety grounds setting means, A fourth step of setting the basis of security of the cryptographic primitive, a fifth step of enumerating the flow by the flow enumeration means, and a type of argument of the flow data and the cryptographic primitive by the argument setting means And the setting information determination means determines whether or not the relationship between the set flow data and the type of the argument of the cryptographic primitive and the state is correct, and includes an incorrect one. If the cryptographic protocol and seventh step of determining unsafe, the safety selection means, pull the flow data and cryptographic primitives the setting If it is determined that the relationship between the type and state is correct, the selection of verification items related to security can be made by selecting key attack protocol active attack safety, passive attack safety, offline dictionary attack safety, known key attack safety, forward The eighth step performed from among the verification items in confidentiality and the verification item determination means determine whether or not all of the selected verification items are satisfied. A ninth step for determining that the selected security is not safe, and a tenth step for determining that the cryptographic protocol is safe when the security determination means satisfies all of the selected verification items. And a program for causing a computer to execute .

  According to the present invention, it is possible to verify a key exchange protocol among cryptographic protocols according to the security level.

It is a figure which shows the structure of the security verification apparatus of the encryption protocol which concerns on this embodiment. It is a figure which shows the relationship between the kind and state of the flow data which concern on this embodiment, and the argument of a cryptographic primitive. It is a processing flow of the security verification apparatus of the encryption protocol which concerns on this embodiment.

Hereinafter, embodiments of the present invention will be described in detail with reference to the drawings.
Note that the constituent elements in the present embodiment can be appropriately replaced with existing constituent elements and the like, and various variations including combinations with other existing constituent elements are possible. Therefore, the description of the present embodiment does not limit the contents of the invention described in the claims.

<Existing security model for cryptographic protocol safety level>
Before going into the description of the embodiments of the present invention, the existing security model is shown with respect to the security level of the cryptographic protocol. The present invention uses a concept called “provable security” that proves the security of a cryptographic protocol based on the computational complexity theory. “Cryptographic protocol has provable security” means that it can be proved theoretically that the security of the cryptographic protocol results in the security of a certain cryptographic primitive.

  Assuming an attacker who breaks a cryptographic protocol, by proving that it is possible to construct a machine that breaks a cryptographic primitive in polynomial time, if this cryptographic primitive is not broken, the cryptographic protocol will not be broken. Prove it. In the present invention, an authentication protocol and a key exchange protocol are considered among cryptographic protocols.

  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, according to the security required for the authentication and key exchange protocol, an actual attack model was assumed and classified into the following security. However, the inside of () represents the attack corresponding to safety.

(1) matching conversion
In the authentication protocol, it indicates that the attacker can do nothing but send the message received from one party to the other party as it is. That is, the attacker cannot perform fraud such as message tampering, new message sending, message blocking, and message order switching.

(1A) Active attack safety (impersonated attack)
Active attack safety in matching conversions indicates that even if an attacker dominates communication between parties, the authentication protocol cannot be broken.

(2) semantic security
In the key exchange protocol, indicates that the 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) Active attack safety (spoofed attack)
Active attack security in semantic security indicates that even if an attacker dominates communication between parties, the key exchange protocol cannot be broken.

(2B) Passive attack safety (Eavesdropping attack)
Passive attack security in semantic security indicates that even if an attacker eavesdrops on communication between parties, the key exchange protocol cannot be broken.

(2C) Offline dictionary attack safety (offline dictionary attack)
The off-line dictionary attack safety in the semantic security indicates that the attacker cannot search the password of the party that matches the past history offline from the password guessing dictionary.

(2D) Known key attack safety (known key attack)
The known key attack security in the semantic security indicates that even if an attacker can obtain a session key, it cannot obtain another session key.

(2E) forward secrecy (long-term key destruction attack)
The forward security in the semantic security indicates that even if an attacker can obtain a long-term key such as a secret key or a password, it cannot obtain a previously shared session key.

  However, in the case of a key exchange protocol that does not use a password and a long-term key, the security of offline dictionary attack (2C) and the security of forward secrecy (2E) are not required.

<Information and symbols set in cryptographic primitives>
The information set in the cryptographic primitives used in the authentication / key exchange protocol is as follows.
(A) Cryptographic primitive (AGF) to be authenticated in the authentication protocol
(B) Cryptographic primitive (KGF) that is a key generation target in the key exchange protocol
(C) Cryptographic primitives (ACP) included in AGF and KGF arguments
(D) Other cryptographic primitives (OCP)

<Information that is the basis of security set for cryptographic primitives>
The information that is the basis of security set for the cryptographic primitive set above is as follows.
(A) Indistinguishability (IND): Indicates that two corresponding events cannot be identified in polynomial time without knowing secret information.
(B) Unidirectionality (OW): Indicates that an input value cannot be calculated in polynomial time from an output value without knowing secret information.
(C) Unforgeability (UF): Indicates that an authenticator of a required message cannot be generated in polynomial time without knowing secret information.

<Components set in all flow data and cryptographic primitives in the authentication / key exchange protocol>
The components set in all flow data and cryptographic primitives in the authentication / key exchange protocol are as follows.
(A) Types of arguments of flow data and cryptographic primitives a) Public information (PUB)
b) Specific public information (ID)
c) Temporary public information (TPK)
d) Long-term and complete confidential information (LLK)
e) Long-term and incomplete confidential information (PW)
f) Temporary confidential information (TSK)
(B) Flow data and cryptographic primitive argument status a) First appearance in public state (PFT)
b) Previously published in the same session (PSS)
c) It can be used repeatedly in other sessions and appears in public (PRS)
d) Appears in a public state that cannot be used repeatedly in another session (PNS)
e) First appearance in a secret state (SFT)
f) Appeared in secret before in the same session (SSS)
g) Can be used repeatedly in different sessions and appears in a secret state (SRS)
h) Cannot be used repeatedly in another session and appears in a secret state (SNS)

<Items to verify authentication and key exchange protocol according to security level>
The items for verifying the authentication and key exchange protocol according to the security level are as follows.

<Matching conversion for authentication protocol>
(A) Verification items and verification contents in active attack safety a) AGF is UF and arguments of AGF are all TPK-PFT, TPK-PSS, TPK-PNS, TSK-SFT, TSK-SSS, or TSK-SNS. Is included.
b) AGF is OW, and all arguments of AGF include TSK-SFT.

<Semantic security for key exchange protocol>
(B) Verification items and verification contents in active attack safety a) ACP is IND or OW, and all arguments of ACP include TSK-SFT and LLK-SRS or PW-SRS.

(C) Verification items and verification contents in passive attack safety a) KGF is IND, and all arguments of KGF include TSK-SFT.
b) KGF is OW, ACP is IND, and the argument of ACP includes TSK-SFT.

(D) Verification items and verification contents in off-line dictionary attack security a) OCP including PW is OW, and each argument of OCP includes TSK-SFT, TSK-SSS, or TSK-SNS.

(E) Verification items and verification contents in known key attack security a) KGF is IND or OW, and all arguments of KGF include TSK-SFT, TSK-SSS, or TSK-SNS.

(F) Verification items and verification contents in forward secrecy a) KGF is IND or OW, and any argument of KGF includes TSK-SFT, TSK-SSS, or TSK-SNS.

<Configuration of cryptographic protocol security verification device>
The configuration of the cryptographic protocol security verification apparatus according to the present embodiment will be described with reference to FIG. As shown in FIG. 1, the cryptographic protocol security verification device according to the present embodiment includes a cryptographic primitive enumeration unit 1, a compromise information determination unit 2, a role setting unit 3, a safety rationale setting unit 4, The flow enumeration unit 5, the argument setting unit 6, the setting information determination unit 7, the safety selection unit 8, the verification item determination unit 9, and the safety determination unit 10 are configured.

  The cryptographic primitive enumeration unit 1 lists all cryptographic primitives used in the authentication / key exchange protocol. The compromise information determination unit 2 confirms whether there is compromise information for the enumerated cryptographic primitives. If there is even one piece of compromise information, the security judgment unit 10 judges that the authentication / key exchange protocol is not secure.

  The role setting unit 3 sets information, for example, AGF, KGF, ACP, OCP, which is the role of the cryptographic primitive among the listed cryptographic primitives. The safety rationale setting unit 4 sets information that is a security rationale, for example, IND, OW, and UF, for cryptographic primitives for which roles are set.

  The flow enumeration unit 5 enumerates all the flows for the authentication / key exchange protocol. For the enumerated flow data and cryptographic primitives, the argument setting unit 6 specifies the types of arguments of the flow data and cryptographic primitives, such as PUB, ID, TPK, LLK, PW, TSK, and the arguments of the flow data and cryptographic primitives. The state, for example, PFT, PSS, PRS, PNS, SFT, SSS, SRS, SNS, and other components are set.

  Based on the data table showing the relationship between the type of flow data and the argument of the cryptographic primitive and the state shown in FIG. Determine if. If even one of the relationships is not correct, the security determination unit 10 determines that the authentication / key exchange protocol is not secure.

  The security selection unit 8 selects the required security in the authentication / key exchange protocol. A plurality of safety may be selected. The verification item determination unit 9 verifies the above-described verification items related to safety using the information set by the argument setting unit 6 for the safety selected by the safety selection unit 8.

However, before verifying the verification items, the following preparations are made according to each security in the authentication / key exchange protocol.
<Matching conversion for authentication protocol>
(A) Verification items in active attack safety Active attack safety is a response to spoofing attacks and generates information for the attacker to authenticate the other party from information obtained by controlling the communication between parties. Indicates that you can't. Note that the information set by the spoofing attack is all flows.

The following items are set for the set information in order of protocol flow. Here, it is assumed that the flow data and the argument state are updated. However, the public state has priority over the public state and the secret state.
a) Types of AGF, ACP, OCP and grounds for safety b) Types and states of arguments of AGF, ACP, OCP c) Types and states of flow data

  If cryptographic primitives are nested in the arguments of AGF and ACP, the state of the arguments of AGF and ACP is set to the final stage.

<Semantic security for key exchange protocol>
(A) Verification items in active attack safety Active attack safety is to distinguish a session key and a random number in polynomial time from information obtained by an attacker controlling communication between parties in response to a pretending attack. Indicates that you cannot. Note that the information set by the spoofing attack is all flows.

The following items are set for the set information in order of protocol flow. Here, it is assumed that the flow data and the argument state are updated. However, the public state has priority over the public state and the secret state.
a) KGF, ACP, OCP types and safety grounds b) KGF, ACP, OCP argument types and status c) Flow data types and status

  When cryptographic primitives are nested in the arguments of KGF and ACP, the state of the arguments of KGF and ACP is set to the final stage.

(B) Verification Items in Passive Attack Safety Passive attack safety corresponds to an eavesdropping attack, in which an attacker can distinguish session keys and random numbers in polynomial time from information obtained by eavesdropping on communication between parties. Indicates that it is not possible. Note that the information set by the wiretapping attack is all flows.

The following items are set for the set information in order of protocol flow. Here, it is assumed that the flow data and the argument state are updated. However, the public state has priority over the public state and the secret state.
a) KGF, ACP, OCP types and safety grounds b) KGF, ACP, OCP argument types and status c) Flow data types and status

  When cryptographic primitives are nested in the arguments of KGF and ACP, the state of the arguments of KGF and ACP is set to the final stage.

(C) Verification Items in Offline Dictionary Attack Safety Offline dictionary attack safety is a response to offline dictionary attacks. From the past history for an attacker to search for a party password offline from a password guessing dictionary, the session key and It shows that random numbers cannot be distinguished by polynomial time. The information set by the off-line dictionary attack is all flows.

The following items are set for the set information in order of protocol flow. Here, it is assumed that the flow data and the argument state are updated. However, the public state has priority over the public state and the secret state.
a) OCP type and grounds for safety b) OCP argument type and status c) Flow data type and status

(D) Verification Items in Known Key Attack Safety Known key attack safety corresponds to a known key attack, and an attacker cannot distinguish a session key and a random number in polynomial time from a session key obtained in another session. It is shown that. Note that the information set by the known key attack is the session key of all other sessions.

The following items are set for the set information in order of protocol flow. Here, it is assumed that the flow data and the argument state are updated. However, the public state has priority over the public state and the secret state.
a) KGF, ACP, OCP types and safety grounds b) KGF, ACP, OCP argument types and status c) Flow data types and status

  When cryptographic primitives are nested in the arguments of KGF and ACP, the state of the arguments of KGF and ACP is set to the final stage.

(E) Verification item in forward secrecy forward secrecy corresponds to a long-term key destruction attack, and a session key and a random number are expressed in polynomial time from a long-term key such as a secret key or a password obtained by an attacker entering a party terminal. Indicates that they cannot be distinguished. The information set by the long-term key destruction attack is a long-term key.

The following items are set for the set information in order of protocol flow. Here, it is assumed that the flow data and the argument state are updated. However, the public state has priority over the public state and the secret state. In this case, the long-term key is handled as public information.
a) KGF, ACP, OCP types and safety grounds b) KGF, ACP, OCP argument types and status c) Flow data types and status

  When cryptographic primitives are nested in the arguments of KGF and ACP, the state of the arguments of KGF and ACP is set to the final stage.

<Processing of cryptographic protocol security verification device>
Processing of the cryptographic protocol security verification apparatus will be described with reference to FIG.
First, cryptographic primitives used in the authentication and key exchange protocol are listed (step S101). Next, for the enumerated cryptographic primitives, the presence / absence of compromise information is verified (step S102), and if there is any compromise information (“No” in step S102), it is determined that the cryptographic protocol is not secure. .

  On the other hand, if none of the listed cryptographic primitives has compromise information (“Yes” in step S102), the role of the cryptographic primitive is set (step S103). Further, the basis of security of the cryptographic primitive is set (step S104), the flow is enumerated (step S105), and the type and state of the argument of the flow data and the cryptographic primitive are set (step S106).

  Then, it is determined whether or not the relationship between the set flow data and the type and state of the argument of the cryptographic primitive is correct (step S107), and if it contains an incorrect one (“No” in step S107), the cryptographic protocol is Judge that it is not safe. On the other hand, when it is determined that the relationship between the set flow data and the type and state of the argument of the cryptographic primitive is all right (“Yes” in step S107), a verification item related to security is selected (step S108).

  Then, it is determined whether or not all of the selected verification items are satisfied (step S109), and if any are not satisfied (“No” in step S109), it is determined that the cryptographic protocol is not secure with respect to the selected security. If all the selected verification items are satisfied (“Yes” in step S109), it is determined that the cryptographic protocol is secure.

  Therefore, according to the present embodiment, the authentication protocol and the key exchange protocol among the cryptographic protocols can be verified according to the security level.

  The above-described series of processing is recorded as a program on a computer-readable recording medium, and the program recorded on the recording medium is read by the cryptographic protocol security verification device and executed, thereby executing the cryptographic protocol of the present invention. A safety verification device can be realized.

  In addition, if a WWW (World Wide Web) system is used, a homepage providing environment (or display environment) is also included. Further, the program may be transmitted from a computer storing the program in a storage device or the like to another computer via a transmission medium or by a transmission wave in the transmission medium. Here, the “transmission medium” for transmitting the program refers to a medium having a function of transmitting information, such as a network (communication network) such as the Internet or a communication line (communication line) such as a telephone line.

  The program may be for realizing a part of the functions described above. Furthermore, what can implement | achieve the function mentioned above in combination with the program already recorded on the computer, what is called a difference file (difference program) may be sufficient.

  The embodiments of the present invention have been described in detail with reference to the drawings. However, the specific configuration is not limited to the embodiments, and includes designs and the like that do not depart from the gist of the present invention.

DESCRIPTION OF SYMBOLS 1 ... Cryptographic primitive enumeration part 2 ... Compromise information determination part 3 ... Role setting part 4 ... Safety ground setting part 5 ... Flow enumeration part 6 ... Argument setting part 7 ... Setting information determination unit 8 ... Safety selection unit 9 ... Verification item determination unit 10 ... Safety determination unit

Claims (7)

For the key exchange protocol of the cryptographic protocol having at least a key sharing security function, the verification items in the key exchange protocol active attack safety, passive attack safety, offline dictionary attack safety, known key attack safety, forward secrecy are for example Bei the verification means for checking as verification item to verify the safety of the exchange protocol,
As a verification item in active attack security of the key exchange protocol, a cryptographic primitive included in an argument of a cryptographic primitive that is a key generation target has an indistinguishability property or a one-way property. Check whether it contains temporary secret information that first appeared in the protocol and long-term complete secret information or long-term incomplete secret information that can be used repeatedly in another session and appears in the protocol A cryptographic protocol security verification device characterized by the above . For the key exchange protocol of the cryptographic protocol having at least a key sharing security function, the verification items in the key exchange protocol active attack safety, passive attack safety, offline dictionary attack safety, known key attack safety, forward secrecy are It has a verification means to check as a verification item to verify the safety of the exchange protocol,
As verification item in receiving dynamic attack safety of the key exchange protocol, it has the property of cryptographic primitives indistinguishability of the key generation target, first appeared temporary secret any cryptographic primitives argument protocol The cryptographic primitives that contain information or the key generation target have a one-way property, and the cryptographic primitives included in the cryptographic primitive argument have the unidentifiable property, and the cryptographic primitive argument A cryptographic protocol security verification device characterized by checking whether or not includes temporary secret information first appearing in the protocol. For the key exchange protocol of the cryptographic protocol having at least a key sharing security function, the verification items in the key exchange protocol active attack safety, passive attack safety, offline dictionary attack safety, known key attack safety, forward secrecy are It has a verification means to check as a verification item to verify the safety of the exchange protocol,
As a verification item in the off-line dictionary attack security of the key exchange protocol, a cryptographic primitive including long-term and incomplete secret information has a one-way property, and all the arguments of the cryptographic primitive first appeared in the protocol . An apparatus for verifying the security of a cryptographic protocol, characterized in that it checks whether it has previously appeared in the protocol in the same session or contains temporary secret information that has been repeatedly unavailable in another session and has appeared in the protocol . For the key exchange protocol of the cryptographic protocol having at least a key sharing security function, the verification items in the key exchange protocol active attack safety, passive attack safety, offline dictionary attack safety, known key attack safety, forward secrecy are It has a verification means to check as a verification item to verify the safety of the exchange protocol,
As a verification item in the known key attack security of the key exchange protocol, the cryptographic primitives that are key generation targets have indistinguishability or one-way properties, and all the arguments of the cryptographic primitives appear for the first time in the protocol, An apparatus for verifying the security of a cryptographic protocol, characterized by checking whether it has appeared in the protocol before in the same session, or contains temporary secret information that cannot be repeatedly used in another session and appears in the protocol. For the key exchange protocol of the cryptographic protocol having at least a key sharing security function, the verification items in the key exchange protocol active attack safety, passive attack safety, offline dictionary attack safety, known key attack safety, forward secrecy are It has a verification means to check as a verification item to verify the safety of the exchange protocol,
As a verification item in the forward secrecy of the key exchange protocol, the cryptographic primitive that is the key generation target has an indistinguishability property or a one-way property, and all the arguments of the cryptographic primitive appear in the protocol for the first time, or the same An apparatus for verifying the security of a cryptographic protocol, comprising: checking whether a session has previously appeared in a protocol or whether temporary secret information that has been repeatedly used in another session and has appeared in the protocol is included. A security verification method in a security verification device for verifying the security of a cryptographic protocol,
The safety verification device includes a cryptographic primitive enumeration unit, a compromise information determination unit, a role setting unit, a safety basis setting unit, a flow enumeration unit, an argument setting unit, a setting information determination unit, a safety A selection unit, a verification item determination unit, and a safety determination unit,
A first step in which the cryptographic primitive enumeration means enumerates cryptographic primitives used in a key exchange protocol;
A second step in which the compromise information determination means verifies the presence or absence of the compromise information for the enumerated cryptographic primitives, and determines that the cryptographic protocol is not secure if there is one having the compromise information; ,
A third step in which the role setting means sets the role of the cryptographic primitive when none of the enumerated cryptographic primitives has compromise information;
A fourth step in which the security basis setting means sets a security basis for the cryptographic primitive;
A fifth step in which the flow enumeration means enumerates flows;
A sixth step in which the argument setting means sets the type and state of arguments of flow data and cryptographic primitives;
The setting information determination means determines whether or not the relationship between the set flow data and the type and state of the argument of the cryptographic primitive is correct, and determines that the cryptographic protocol is not secure when it includes an incorrect one. A seventh step to:
When the security selection unit determines that the relationship between the set flow data and the type and state of the cryptographic primitive arguments are all correct, the selection of the verification items related to the security is performed, and the active attack safety of the key exchange protocol is selected. 8th step to be performed from the verification items in passive attack safety, offline dictionary attack security, known key attack safety, forward secrecy,
A ninth step in which the verification item determination means determines whether or not all of the selected verification items are satisfied, and determines that the cryptographic protocol is not secure with respect to the selected security if it includes items that do not satisfy When,
A tenth step for determining that the cryptographic protocol is safe when the security determination means satisfies all the selected verification items;
Safety verification method characterized by having a. A program for causing a computer to execute a security verification method in a security verification device for verifying the security of a cryptographic protocol,
The safety verification device includes a cryptographic primitive enumeration unit, a compromise information determination unit, a role setting unit, a safety basis setting unit, a flow enumeration unit, an argument setting unit, a setting information determination unit, a safety A selection unit, a verification item determination unit, and a safety determination unit,
A first step in which the cryptographic primitive enumeration means enumerates cryptographic primitives used in a key exchange protocol;
A second step in which the compromise information determination means verifies the presence or absence of the compromise information for the enumerated cryptographic primitives, and determines that the cryptographic protocol is not secure if there is one having the compromise information; ,
A third step in which the role setting means sets the role of the cryptographic primitive when none of the enumerated cryptographic primitives has compromise information;
A fourth step in which the security basis setting means sets a security basis for the cryptographic primitive;
A fifth step in which the flow enumeration means enumerates flows;
A sixth step in which the argument setting means sets the type and state of arguments of flow data and cryptographic primitives;
The setting information determination means determines whether or not the relationship between the set flow data and the type and state of the argument of the cryptographic primitive is correct, and determines that the cryptographic protocol is not secure when it includes an incorrect one. A seventh step to:
When the security selection unit determines that the relationship between the set flow data and the type and state of the cryptographic primitive arguments are all correct, the selection of the verification items related to the security is performed, and the active attack safety of the key exchange protocol is selected. 8th step to be performed from the verification items in passive attack safety, offline dictionary attack security, known key attack safety, forward secrecy,
A ninth step in which the verification item determination means determines whether or not all of the selected verification items are satisfied, and determines that the cryptographic protocol is not secure with respect to the selected security if it includes items that do not satisfy When,
A tenth step for determining that the cryptographic protocol is safe when the security determination means satisfies all the selected verification items;
A program that causes a computer to execute.

Images