JP5188288B2 - 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) In the present invention, at least for an authentication protocol of a cryptographic protocol having an authentication security function, in order to verify the security of the authentication protocol, the cryptographic primitive to be authenticated has the property of being unforgeable, Either the argument of the cryptographic primitive appears for the first time in the protocol, previously appeared in the protocol in the same session, is temporarily public information that appears repeatedly in the protocol that cannot be used repeatedly in another session, or Contains temporary secrets that appear for the first time, appear in the protocol before in the same session, cannot be repeatedly used in another session and appear in the protocol, or the cryptographic primitives to be authenticated are one-way And the argument of the cryptographic primitive is Even if it includes a temporary secret information first appeared in the protocol, we propose a security verification system of the cryptographic protocol with a verification means for checking the verification item in active attack security of the authentication protocol.

(2) The present invention provides a cryptographic primitive enumeration unit, a compromise information determination unit, a role setting unit, a safety reason setting unit, a flow enumeration unit, an argument setting unit, a setting information determination unit, a safety A safety verification method for verifying the security of a cryptographic protocol in a cryptographic protocol security verification device comprising a selection unit and a verification item determination unit , wherein the cryptographic primitive enumeration unit is used in a cryptographic protocol A first step of enumerating encrypted primitives, and the compromised information determination unit verifies the presence or absence of compromised information for the enumerated cryptographic primitives, and if there is a compromised information, the encryption a second step of determining that the protocol is not safe, the role setting unit, in a cryptographic primitives enumerated above, if there is no one having a compromise information A third step of setting the role of the cryptographic primitives, said safety grounds setting unit, and a fourth step for setting a basis for security of the cryptographic primitives, the flow enumeration unit, an enumeration of the flow A fifth step of performing, a sixth step in which the argument setting unit sets the type and state of arguments of the flow data and the cryptographic primitive, and a setting information determination unit in which the set flow data and cryptographic primitive are A seventh step of determining whether or not the relationship between the type of argument and the state is correct, and including an incorrect one, and determining that the cryptographic protocol is not secure; Verification items in the active attack security of the authentication protocol when it is determined that the relationship between the flow data and the type and state of the arguments of the cryptographic primitive are all correct Thus, the target cryptographic primitive has the property of non-forgery, and any argument of the cryptographic primitive has first appeared in the protocol, has previously appeared in the protocol in the same session, or is not repeatedly used in another session. Possible temporary public information that appeared in the protocol, or that appeared in the protocol for the first time, appeared in the protocol before in the same session, or could not be used repeatedly in another session, and appeared temporarily in the protocol Check whether secret information is included, or whether the cryptographic primitives to be authenticated have a one-way property, and all the arguments of the cryptographic primitives contain temporary secret information that appears for the first time in the protocol And an eighth step of the verification item determination unit Ninth step for determining whether or not all verification items in active attack security are satisfied, and including those not satisfying, a ninth step for determining that the cryptographic protocol is not safe with respect to the selected security, and the verification items A security verification method comprising: a tenth step for determining that the cryptographic protocol is secure when the determination unit satisfies all verification items in active attack security of the authentication protocol; is suggesting.

(3) The present invention provides a cryptographic primitive enumeration unit, a compromise information determination unit, a role setting unit, a safety reason setting unit, a flow enumeration unit, an argument setting unit, a setting information determination unit, a safety A program for causing a computer to execute a security verification method for verifying the security of a cryptographic protocol in a cryptographic protocol security verification device comprising a selection unit and a verification item determination unit , the cryptographic primitive enumeration A first step of enumerating cryptographic primitives used in a cryptographic protocol, and the compromise information determining unit verifying the presence or absence of compromise information for the listed cryptographic primitives and having compromise information If there is one, the cryptographic protocol and a second step of determining unsafe, the role setting unit, the cryptographic primitives enumerated above During, when no one having a compromise information, a third step of setting the role of the cryptographic primitives, said safety grounds setting unit, first to set the basis for security of the cryptographic primitives 4 The flow enumeration unit for enumerating the flow, the argument setting unit for setting the flow data and the type and state of the cryptographic primitive arguments, and the setting. The information determining unit 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. 7 and steps, when the safety selection unit, the relationship between the type and state of the arguments of the flow data and the cryptographic primitives described above setting is determined that all correct, the authentication As a verification item in the active attack security of the protocol, whether the target cryptographic primitive has the property of non-forgery and whether any argument of the cryptographic primitive first appeared in the protocol or previously appeared in the protocol in the same session , Temporary public information that appears in the protocol that cannot be used repeatedly in another session, or that appeared for the first time in the protocol, previously appeared in the protocol in the same session, or cannot be used repeatedly in another session Contains temporary secret information that appears in the protocol, or the cryptographic primitive to be authenticated has a one-way nature, and all the arguments of the cryptographic primitive appear in the protocol for the first time An eighth step of checking whether information is included; When the verification item determination unit determines whether or not all verification items in the active attack security of the authentication protocol are satisfied, and includes those not satisfied, the cryptographic protocol is not secure with respect to the selected security A ninth step of determining, and a tenth step of determining that the cryptographic protocol is safe when the verification item determination unit satisfies all verification items in active attack security of the authentication protocol. Proposes a program to be executed by a computer.

According to the present invention, there is an effect that an authentication protocol among cryptographic protocols can be verified according to a security level.

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 above provable security, the authentication protocol matches
In conversion and key exchange protocol, there is a concept of security called semantic security. 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)
forward in the semantic security
The secrecy indicates that even if the attacker can obtain a long-term key such as a secret key or a password, the attacker cannot obtain a session key shared before that time.

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

<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 the authenticator of the required message cannot be generated in polynomial time without knowing the 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 states c) Flow data types and states

  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 states c) Flow data types and states

  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 states c) Flow data types and states

  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 states c) Flow data types and states

  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). 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.

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.

Explanation of symbols

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 (3)

    At least for an authentication protocol of a cryptographic protocol having an authentication security function, in order to verify the security of the authentication protocol, the cryptographic primitive to be authenticated has the property of non-forgery, and the argument of the cryptographic primitive Are either first appearing in the protocol, previously appearing in the same session in the same session, are temporarily unavailable in other sessions and are temporary public information appearing in the protocol, or first appearing in the protocol, Either it appears in the protocol before in the same session, cannot be used repeatedly in another session, contains temporary secret information that appears in the protocol, or the cryptographic primitives to be authenticated have a one-way nature. However, all the arguments of the cryptographic primitive are Or it contains a first appeared temporary secret information Col security verification device of the cryptographic protocol with a verification means for checking the verification item in active attack security of the authentication protocol. Cryptographic primitive enumeration unit, compromise information determination unit, role setting unit, safety reason setting unit, flow enumeration unit, argument setting unit, setting information determination unit, security selection unit, and verification item determination A security verification method for verifying the security of a cryptographic protocol in a cryptographic protocol security verification device comprising: a cryptographic primitive enumeration unit enumerating cryptographic primitives used in the cryptographic protocol In the first step, the compromise information determination unit verifies the presence or absence of compromise information for the enumerated cryptographic primitives, and determines that the cryptographic protocol is not safe if there is any compromise information. a second step of, the role setting unit, in a cryptographic primitives enumerated above, if there is no one having a compromise information, the cryptographic primitives Performing a third step of setting the role of I blanking, the safety grounds setting unit, and a fourth step for setting a basis for security of the cryptographic primitives, the flow enumeration unit, an enumeration of the flow A fifth step, a sixth step in which the argument setting unit sets the type and state of the flow data and the argument of the cryptographic primitive, and the setting information determination unit sets the flow data and the argument of the cryptographic primitive. The relationship between the type and the state of whether or not the relationship between the type and the state is correct, and when it includes an incorrect one, a seventh step for determining that the cryptographic protocol is not secure, and the security selector sets the set When it is determined that the relationship between the flow data and the type and state of the cryptographic primitive arguments are all correct, the verification protocol in the active attack security of the authentication protocol is subject to verification. A cryptographic primitive has the property of non-forgery and any of the cryptographic primitive arguments first appeared in the protocol, previously appeared in the protocol in the same session, or appeared in the protocol repeatedly unusable in another session Whether it is temporary public information, or it appears for the first time in the protocol, previously appeared in the protocol in the same session, or cannot be used repeatedly in another session and contains temporary confidential information that appears in the protocol Or an eighth step of checking whether the cryptographic primitive to be authenticated has a one-way property, and any of the arguments of the cryptographic primitive includes temporary secret information first appearing in the protocol; The verification item determination unit makes the active attack safety of the authentication protocol safe. Determining whether or not all the verification items are satisfied, and including a non-satisfied one, the ninth step of determining that the cryptographic protocol is not secure with respect to the selected security, and the verification item determination unit, And a tenth step of determining that the cryptographic protocol is secure when all of the verification items in the active attack security of the authentication protocol are satisfied. Cryptographic primitive enumeration unit, compromise information determination unit, role setting unit, safety reason setting unit, flow enumeration unit, argument setting unit, setting information determination unit, security selection unit, and verification item determination A program for causing a computer to execute a security verification method for verifying the security of a cryptographic protocol in a cryptographic protocol security verification device comprising: a cryptographic protocol enumeration unit used in the cryptographic protocol The first step of enumerating the cryptographic primitives that have been performed, and the compromise information determination unit verifies the presence or absence of the compromise information for the enumerated cryptographic primitives, and if there is one having the compromise information, a second step of determining that the cryptographic protocol is not safe, the role setting unit, in a cryptographic primitives enumerated above, compromise Kajo If there is no one having, a third step of setting the role of the cryptographic primitives, said safety grounds setting unit, and a fourth step for setting a basis for security of the cryptographic primitives, the flow A fifth step in which the enumeration unit enumerates flows; a sixth step in which the argument setting unit sets the type and state of arguments of flow data and cryptographic primitives; and the setting information determination unit includes: it is determined whether the relationship is correct arguments type and state of the flow data and cryptographic primitives that the set, if it contains not correct, the encryption protocol and the seventh step of determining unsafe, the when the safety selection unit, the relationship between the type and state of the arguments of the flow data and the cryptographic primitives described above setting is determined that all correct, active of the authentication protocol As a verification item in attack security, the target cryptographic primitive has the property of non-forgery, and all the arguments of the cryptographic primitive appear in the protocol for the first time, appear in the protocol in the same session before, another session Is temporary public information that appears in the protocol that cannot be used repeatedly in the protocol, or appears in the protocol that appeared in the protocol for the first time, appeared in the protocol before in the same session, or cannot be used repeatedly in another session The encryption primitive to be authenticated has a one-way nature, and any argument of the encryption primitive contains temporary secret information that appears for the first time in the protocol. An eighth step of checking whether or not the verification item is determined Part is, first the determines whether or not to satisfy all the verification items in active attacks secure authentication protocol, when including those not satisfied, the encryption protocol is determined to be unsafe for safety selected 9 And a tenth step in which the verification item determination unit determines that the cryptographic protocol is secure when all verification items in the active attack security of the authentication protocol are satisfied. Program for.

Images