JP6445474B2 - Pairing type conversion device, pairing type conversion method, program - Google Patents

Description

  The present invention relates to a pairing type conversion device, a pairing type conversion method, and a program for converting an algebraic structure of an algorithm.

A technique for converting the algebraic structure of an algorithm is known. For example, Non-Patent Document 1, the group G, the pairing on G _T e: an algorithm using G × G → G _T, the group G _1, G _2, pairing on G _T e: G ₁ × A technique for converting into an algorithm using G ₂ → G _T (where G ₁ ≠ G ₂ ) is disclosed. In Non-Patent Document 1, the group G ₁ or the group G ₂ is assigned to the node of the dependency graph of the group operation on the group G, the assignment situation is evaluated with an evaluation function, and the assignment with the best evaluation is selected.

<Preparation>
In cryptography, pairing is a probabilistic polynomial-time algorithm P that generates codes with the following algebraic structure.

Where λ is a safety variable, q is an integer q> 2 ^{Θ (λ)} , G ₁ , G ₂ , and G _T are finite abelian groups of the same type q (signs of each), and each is a polynomial time sample operation And with group operations. E: G ₁ × G ₂ → G _T is a polynomial time non-degenerate bimorphism. The CDH (Computational Diffie-Hellman) problem on G ₁ , G ₂ , and G _T is difficult.

G ₁ and G ₂ are referred to as a source group, and G _T is referred to as a target group. Unless otherwise specified, when calling simply a group or a group element, it means a source group or a group element of a source group. Galbraith et al. Roughly classified the pairing used in the encryption method into the following three types (Non-patent Document 2).
Type1: G ₁ = G ₂
There exists a polynomial time isomorphism of Type2: G ₁ ≠ G ₂ and φ: G ₂ → G ₁ .
Type3: There is no polynomial time isomorphism between G ₁ ≠ G ₂ , G ₁ and G ₂ .

In general, Type 1 is called symmetric pairing, and Type 2 and Type 3 are called asymmetric pairing. Since Type2 can be implemented using Type3, Type2 is not likely to appear except when actively using φ for methods and safety certification. In this specification, Type 3 is particularly assumed as asymmetric pairing. Regarding implementation problems such as calculation speed and group element size, the existence of asymmetric pairing that is much more efficient than symmetric pairing is known (see Non-Patent Document 3).
<Dependency Relationship Graph (Non-Patent Document 1)>
In contrast to a method, its dependency graph (dependency graph) is a directed graph that expresses a dependency relationship between group element variables describing the method. FIG. 1 shows a dependency graph in a simple example. The following is an algorithm corresponding to the dependency graph of FIG.

  The above algorithm is an example of an algorithm that receives group elements A, B, and D, calculates C and E using group operations, and outputs the pairing e (C, E). Each node represented by a round symbol in the dependency relationship graph shown in FIG. 1 represents a group element variable, and each edge (an arrow symbol in the figure) represents a dependency relationship by group operation. The input to pairing is expressed by the connection (arrow) to the pairing nodes 91 and 92 (rounded square symbols in the figure). In the dependency graph, only the relationship between group elements via group operations is described. Program structure such as "if-then-else" instruction and variables other than group elements such as a∈Z / pZ, Alternatively, all operations on the target group are discarded. Hereinafter, terms used to describe the dependency relationship graph are defined.

<Ancestral graph>
A subgraph of the dependency graph including all paths (edges) that can reach a specific node is called an ancestor graph of the specific node.

<Ancestor node>
A node that can reach a specific node is called an ancestor node of the specific node. For example, in the example of FIG. 1, node A is an ancestor node of node C.

<Descendant node>
A node that can be reached from a specific node is called a descendant node of the specific node. For example, in the example of FIG. 1, the node C is a descendant node of the node A.

<Input edge>
Represents the dependency by ancestor group operation. In the example of FIG. 1, the group element C is connected to the group element A by an input edge 81.

<Output edge>
Represents a dependency relationship by a group operation for descendant nodes. In the example of FIG. 1, the group element A is connected to the group element C at the output edge 81.

<Pairing node>
A node expressing an input to pairing in the dependency graph is called a pairing node. In the example of FIG. 1, pairing nodes 91 and 92 are illustrated.

<Regular node>
A node that is not a pairing node is called a regular node. In the example of FIG. 1, regular nodes are represented by round symbols.

<Bottom node>
Of the regular nodes, a node representing no entire output edge or representing an entire loop having no output edge is called a bottom node.

<Duplex node>
A node in which both of the two source groups have been assigned is called a duplex node. The duplex node will be described later.

<Duplication prohibition node>
A node prohibited from becoming a duplex node for some reason is called a duplex prohibition node.

<Critical node>
The pairing node, the bottom node, and the duplication prohibition node are collectively referred to as a critical node.

<Normal node>
A node that is not a critical node is called a normal node.

<Terminology>
A predicate that x is included in the graph of G _i , i∈ {1,2} after partitioning for a certain node x is described as x∈G _i, and ¬ (x∈G _i )

Is described. And when those predicates are true, the value is defined as 1, and when the predicate is false, the value is defined as 0. That is, (x∈G _i ) ∈ {0, 1}. If a node x is a critical node, the predicate xεG ₁ and the predicate xεG ₂ are exclusive. That is, the exclusive rule x∈G ₁ ∧x∈G ₂ = 0 holds. On the other hand, if x is a normal node, the exclusion rule does not necessarily hold. In the present specification, the predicate x∈G ₂ relating to the critical node x is described again as a logical variable x. That is, for critical node x

である。

It is.

<The algorithm of Tango et al. (Non-Patent Documents 4 and 1)>
Since symmetric pairing has a simple algebraic structure, many cryptosystems are designed on the assumption of symmetric pairing. However, from the viewpoint of efficiency such as time complexity and area complexity, it is now considered desirable to use asymmetric pairing. Therefore, Tango et al. Proposed an algorithm for automatically converting an encryption system based on symmetric pairing into an encryption system based on asymmetric pairing while maintaining security (Non-Patent Documents 4 and 1). The transformation of Tango et al. Is roughly composed of the following algorithm.
Step1: Configure the dependency graphs (directed graphs) of the group operations in each algorithm constituting the encryption method and the reduction algorithm used in the security proof, and integrate them into one. FIG. 2 illustrates the integration of dependency graphs in the algorithm of Tango et al. For example, a dependency relationship graph (left of FIG. 2) representing an encryption algorithm including nodes P, Q, R, and the like, and a dependency graph (center of FIG. 2) representing a decryption algorithm including node P are represented by one dependency graph ( 2).
Step 2: Assign a pairing node corresponding to an input to pairing and a node called a bottom node corresponding to an input to a group element comparison operation to G ₁ or G ₂ . FIG. 3 illustrates allocation of source groups and decomposition of a graph for each source group in the algorithm of Tango et al. Of the bottom node 71 and 72 included in the dependency graph for example G ₁ is assigned 3, for example G ₂ is assigned to the bottom node 73, 74 (FIG. 3 top middle).
Step 3: In each pairing node and bottom node, a node (an ancestor node) tracing back one adjacent node of the input edge is assigned the same as the original pairing node or bottom node. If both G ₁ and G ₂ allocations occur at this time, it is interpreted as a node (duplex node) to which both are allocated. In the example of FIG. 3, G ₁ is assigned to the ancestor nodes of the bottom nodes 71 and 72, G ₂ is assigned to the ancestor nodes of the bottom nodes 73 and 74, and the node 61 to which both source groups are assigned. Etc. are interpreted as duplex nodes (upper right in FIG. 3).
Step4: When the duplication prohibition node corresponding to the HashToPoint () operation etc. appearing in the graph is a duplication node, the assignment is invalid. In other cases, the entire allocation state of the graph is input to the evaluation function for evaluation.
Step 5: For all assignments in Step 2, the graph with the best evaluation is decomposed into a graph composed of nodes to which G ₁ is allocated and a graph composed of nodes to which G ₂ is allocated (lower row in FIG. 3).

In the conversion of Tango et al., Step 3 and Step 4 must be executed in proportion to the number of source group assignment variations in Step 2. This requires 2 ⁿ operations, where n is the sum of the number of pairs of pairing nodes and the number of bottom nodes, and when n is large, the amount of computation becomes too large and difficult to execute.

<Partition algorithm using integer programming>
In asymmetric pairing, the input G ₁ to one paired if the has attached node to the pairing is necessary to G ₂ is hitting split. Therefore, for the pair of nodes x, y∈ {0,1}
x + y = 1… (1)
Is established. Also, if there is a critical node (duplication prohibition node) y in an ancestor node of a certain critical node x, the allocation of those nodes is equal, that is,
xy = 0 ... (2)
Is established.

<Example>
FIG. 4 shows a dependency graph representing the group signature algorithm with local verifier of Boneh et al. (Non-patent Document 5). g ₁ , g ₂ , and ω correspond to the group public key of this scheme. See Non-Patent Document 5 for details. (p ₁ [0], p ₁ [1]),..., (p ₈ [0], p ₈ [1]) are a pair of pairing nodes. R ₁ , R ₃ ,

Is the bottom node. Moreover, u and v correspond to a duplication prohibition node (Non-patent Document 4). Therefore, this graph shows u, v, R ₁ , R ₃ ,

, p ₁ [0], p ₁ [1], ..., p ₈ [0], p ₈ [1], a total of 21 critical nodes exist. Consider the GF (2) overline relationship between these critical nodes. One linear relationship is expressed by sequentially arranging the coefficients and constant term values in accordance with the above variable order. For example, p ₁ [0], p ₁ [1] is a critical node that is a pairing pair.

Is established. In the above variable order, the coefficient of the sixth variable p ₁ [0] and the seventh variable p ₁ [1] is 1, the other coefficients are 0, and the constant term is 1. And only the value of the constant term
0,0,0,0,0,1,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1
It becomes. If "," is omitted
0000011000000000000001
Can be expressed as FIG. 5 illustrates the above process. When all the linear relationships in the graph of FIG. 4 are written down by this method, the linear relationship matrix illustrated in FIG. 6 is obtained. This matrix can be transformed into an echelon form using Gaussian elimination on GF (2). FIG. 7 illustrates a stepped matrix obtained by converting the linear relationship matrix of FIG. 6 into a stepped type.
If the bottom non-zero row of the staircase matrix is
0000000000000000000001
In this case, the coefficient of all variables is 0 and the constant term is 1, so the expression cannot be satisfied for any variable assignment. That is, the graph cannot be divided. In the group signature example above, the bottom non-zero line is
0000000000000000000111
(See FIG. 7), it can be seen that it can be divided. In the present specification, a variable that becomes the first term (corresponding to 1 with a solid underline in FIG. 7) in any step-type row (corresponding relational expression) is called a dependent variable. A variable that is not a dependent variable (corresponding to a column with a dashed underline in FIG. 7) is called an independent variable. Therefore, in the above example, p ₁ [1] and p ₈ [1] are independent variables, and the others are dependent variables. If you assign one appropriate value to all the independent variables, you can uniquely determine the value of the dependent variable sequentially from the lower relational expression.

In general, if there are n independent variables, there are 2 ⁿ value assignment methods (feasible solutions). Of these assignments, you want to find the optimal partition that meets some criteria. For example, in the case of the group signature in FIG. 4, g ₁ , g ₂ , and ω correspond to public keys. Therefore, if you want to find a partition with the smallest public key size, find a graph with the smallest total size of g ₁ , g ₂ , and ω. In this specification, such an evaluation criterion is expressed using a weight w _N for the node N. For example, in the case of FIG. 4, the nodes g ₁ , g ₂ , and ω are set to weight 1, the remaining nodes are set to weight 0 and the like.

| G _i |, i∈ {1,2} is defined as the number of bits necessary to represent an element of G _i , and defined as w _{N, i} = w _N · | G _i |. A set of vertices included in the graph g is defined as Vg. Using these notations, if the value of each predicate is regarded as an integer as it is, the problem of minimizing the size of the public key is as follows:

It can be regarded as a problem that minimizes the numerical value. If the set of critical nodes that node N has as descendants is defined as D _N

Can be. Therefore

Can be written. By the way, for variables x, x ₁ , x ₂ , y on {0,1}

It is. That is, arbitrary conjunctions and negations of {0,1} variables can be replaced with variables under linear constraints, and the logical form of any propositional variable can be replaced by repeating this replacement. It is well known that it can be converted to a constrained linear form. Especially when x ₁ , ..., x _k , y∈ {0,1}

It is. Therefore, the value y _{1, N} on {0,1}

Defined as

Because

And can. As well

Defined as

It is. Therefore

The problem of minimizing

Regarding

Under the linear constraint

Can be reduced to the problem of minimizing the linear objective function.

If d ₁ and d ₂ are regarded as variables on {0, 1} for the critical nodes d ₁ and d ₂ that are paired, d ₁ + d ₂ = 1 holds. Similarly, d ₁ -d ₂ = 0 holds for critical nodes d ₁ and d ₂ having an ancestor-descendant relationship. Therefore, an exact solution or approximate solution can be obtained by writing down all of these linear relationships and inputting the above linear constraints and the above objective function into an arbitrary 0-1 integer programming algorithm.

In JA Garay and R. Gennaro, editors, Advances in Cryptology -CRYPTO 2014-34th Annual Cryptology Conference, Santa Barbara, CA, USA, August 17-21, 2014, Proceedings, Part I, volume 8616 of Lecture Notes in Computer Science, pages 241 {260. Springer, 2014. S. D. Galbraith, K. G. Paterson, and N. P. Smart. Pairings for cryptographers.Discrete Applied Mathematics, 156 (16): 3113 {3121, 2008. PSLM Barreto and M. Naehrig.Pairing-friendly elliptic curves of prime order.In B. Preneel and SE Tavares, editors, Selected Areas in Cryptography, 12th International Workshop, SAC 2005, Kingston, ON, Canada, August 11-12, 2005 , Revised Selected Papers, volume 3897 of Lecture Notes in Computer Science, pages 319 {331. Springer, 2005. T. Tango, M. Abe, and T. Okamoto.Implementation of Automated Translation for Schemes on Symmetric Bilinear Groups.In Proc. Of SCIS 2014, 2014. D. Boneh and H. Shacham.Group signatures with verier-local revocation.In V. Atluri, B. Ptz-mann, and PD McDaniel, editors, Proceedings of the 11th ACM Conference on Computer and Communications Security, CCS 2004, Washington, DC, USA, October 25-29, 2004, pages 168 {177. ACM, 2004. J. Groth and A. Sahai. Efficient noninteractive proof systems for bilinear groups.SIAM J. Comput., 41 (5): 1193 {1232, 2012.

  When designing a large-scale scheme, a concept having a higher abstraction level than a concept such as pairing or power may be used as a cryptographic primitive (for example, Groth-Sahai proof, Non-Patent Document 6). When such primitives with a high degree of abstraction (upper primitives) are mounted with specific primitives such as pairing and power, the mounting method is not necessarily unique. Furthermore, the optimal implementation can vary depending on the design designed using it, not the high-order primitive itself. In such cases, the dependency graph in the strict sense is not uniquely determined. For example, in Groth-Sahai certification

The non-interactive zero-knowledge proofs (NIZK)

There is a case where a non-interactive witness-indistinguishable proof (NIWI) of the following equation is used (Non-Patent Document 6). However, [X] is a group element variable committed for the group element X. At this time, e (C _i ^-1 , [B _i ]) may be used instead of e (B _i ^-1 , [C _i ]) when the pairing used is symmetric pairing. . In other words, when implementing the above upper primitive Groth-Sahai proof with symmetric pairing, if the number of constant pairings is n, there are N = 2 ⁿ degrees of freedom, and the dependency graph is not uniquely determined . Therefore, if there are m such upper primitives in the scheme, it is necessary to call an algorithm using integer programming N ^m times in order to obtain the optimum scheme among all implementations. It was impossible to calculate.

  Therefore, an object of the present invention is to provide a pairing type conversion device that can reduce the number of times an algorithm is called using integer programming to one.

  The pairing type conversion apparatus of the present invention includes a virtual dependency relationship graph generation unit, an identifier allocation unit, a logical expression incorporation unit, and an evaluation function linearization unit.

  The virtual dependency graph generation unit generates a virtual dependency graph that enumerates and incorporates all the upper primitives for a cryptographic protocol including a plurality of selectable upper primitives during implementation. The identifier assigning unit assigns an identifier to each of the upper primitives. The logical expression incorporation unit incorporates the logical expression so that the node corresponding to the identifier is counted in the evaluation function only when the identifier matches the value of the appropriate implementation. The evaluation function linearization unit linearizes the evaluation function and converts the evaluation function and the search space into an integer programming problem instance.

  According to the pairing type conversion apparatus of the present invention, the number of calls of an algorithm using integer programming can be reduced to one.

The figure which shows the dependence relationship graph in a simple example. The figure which illustrates integration of the dependence graph in the algorithm of Tango et al. The figure which illustrates allocation of the source group in Tango's algorithm, and decomposition | disassembly of the graph for every source group. The figure which shows the dependence graph expressing the verifier local revocation group signature algorithm of Boneh et al. The figure which illustrates the process of converting the linear relationship between critical nodes into a matrix form. The figure which illustrates a linear relationship matrix. The figure which illustrates the staircase type matrix which converted the linear relationship matrix into the staircase type. 1 is a block diagram showing a configuration of a pairing conversion device according to Embodiment 1. FIG. 3 is a flowchart showing the operation of the pairing conversion device according to the first embodiment. The figure which illustrates the virtual dependency relationship graph which enumerated the high-order primitive. The figure which illustrates the state in which only the node of the high-order primitive corresponding to a specific identifier is counted in an evaluation function in a virtual dependency relationship graph.

  Hereinafter, embodiments of the present invention will be described in detail. In addition, the same number is attached | subjected to the structure part which has the same function, and duplication description is abbreviate | omitted.

  Hereinafter, the configuration and operation of the pairing conversion device according to the first embodiment will be described with reference to FIGS. 8, 9, 10, and 11. FIG. 8 is a block diagram showing the configuration of the pairing type conversion apparatus 1 of the present embodiment. FIG. 9 is a flowchart showing the operation of the pairing type conversion apparatus 1 of the present embodiment. FIG. 10 is a diagram illustrating a virtual dependency graph listing the upper primitives. FIG. 11 is a diagram exemplifying a state in which only the node of the upper primitive corresponding to a specific identifier is counted in the evaluation function in the virtual dependency relationship graph.

  As shown in FIG. 8, the pairing conversion device 1 according to the present exemplary embodiment includes a virtual dependency graph generation unit 11, an identifier assignment unit 12, a logical expression incorporation unit 13, and an evaluation function linearization unit 14.

  The virtual dependency graph generation unit 11 enumerates all upper primitives (illustrated as upper primitives 51-1, 51-2, 51-3, etc. in FIG. 10) for a cryptographic protocol including a plurality of selectable upper primitives during implementation. ) To generate a virtual dependency relationship graph (illustrated as the virtual dependency relationship graph 4 in FIG. 10) (S11). The identifier assigning unit 12 assigns identifiers (illustrated as identifiers v = 1, 2, 3,... In FIG. 10) to each higher primitive (S12). The logical expression incorporating unit 13 determines that the node corresponding to the identifier is an evaluation function only when the identifier matches the value of the appropriate implementation (in FIG. 11 exemplifies the case where the identifier v = 2 matches the value of the appropriate implementation). A logical expression is incorporated so as to be counted (S13). The evaluation function linearization unit 14 linearizes the evaluation function and converts the evaluation function and the search space into an integer programming problem instance (S14).

Below, the detail of operation | movement of the pairing type conversion apparatus 1 of a present Example is demonstrated. Assuming that the parameter representing the scale of the scheme is s, upper primitives whose implementation freedom N is a polynomial (i.e., n = O (log (s))) with respect to s are polynomial units (m = O ( Consider a situation where s ^c )) exists. However, O is a big-o notation. Under such circumstances, even if the dependency graph is not uniquely determined, a single integer programming problem instance can be constructed by considering a virtual dependency graph as follows.
Step.1: Define an integer variable (identifier) for each higher primitive.
Step 2: All possible implementations of the upper primitive are virtually implemented (step S11 above), and the integer variable (identifier) value is assigned to each virtual implementation one by one (above step S12). At this time, the virtual dependency graph generation unit 11 implements only one (virtual) group element variables that are not explicitly included in the original method and that are collectively referred to from a plurality of virtual implementations. .
Step.3: When the group element variable included in the virtual implementation to which the value is assigned is included in the evaluation function, the integer variable is included in the coefficient so that it is evaluated only when the integer variable (identifier) matches the value. Set the nomenclature (equation). As for the virtual group element variables that are referred to from a plurality of virtual implementations, those obtained by connecting the above terms with scissors are set as coefficients (step S13).
Step.4: The evaluation function linearization unit 14 converts an integer variable (identifier) into a binary variable, if necessary. At this time, the term (equal expression) of the integer variable (identifier) is converted into an expression obtained by connecting the term (equal expression) of the binary variable with ∧. In addition, binary variable terminology (equalities) is converted to literals (binary variables themselves or their negations). Finally, the evaluation function is linearized using equation (3) (step S14).

  For example, consider the following NIZK (NonInteractive Zero-Knowledge proofs) sequence.

  Here, crs, [X], [B], proof, etc. are a list of a finite number of group element variables generated by a specific group operation within the function on each right side. Hereinafter, the bit length of these lists is described as | [X] | In general, NIZK.Verify corresponding to NIZK.Prove is used in different algorithms that make up the scheme, but since the dependency graph is finally integrated into one, it is described here as one sequence. It is assumed that commit [B] is referenced in the part of. In accordance with Step 1. above, a variable vε {0, 1} is prepared for the upper primitive NIZK in the above sequence. Then, according to Step.2, list the implementations as follows and assign variable values (see the comment section below).

  Here, the commit [C] that is not explicitly included in the original method is referenced only from the virtual implementation with v = 0. Even if the commit [C] is referenced from another virtual implementation, only one is implemented. In order to construct NIZK (NonInteractive Zero-Knowledge proofs) using NIWI (NonInteractive Witness-Indistinguishable proofs) in Groth-Sahai certification, in practice, some additional NIWI is required. It is omitted by describing. If the objective function is a function that minimizes the size of the commit, for example, according to Step 3.

And so on. Commits [X] and [B] are defined in the original method and are therefore unconditionally incorporated into the objective function. On the other hand, the commit [C] is a conditional term because it is a commit newly generated by the expansion of the upper primitive. According to Step.4, | [X] |, | [B] |, | [C] | are expanded into logical expressions of critical nodes according to the method described above.

And finally the formulas (1), (2) and

Under the linear constraint

なる目的関数を最小化する１つの0-1整数線形計画問題インスタンスに帰着される。

Which results in one 0-1 integer linear programming problem instance that minimizes the objective function

<Supplementary note>
The apparatus of the present invention includes, for example, a single hardware entity as an input unit to which a keyboard or the like can be connected, an output unit to which a liquid crystal display or the like can be connected, and a communication device (for example, a communication cable) capable of communicating outside the hardware entity. Can be connected to a communication unit, CPU (Central Processing Unit, may include a cache memory or a register), RAM or ROM as a memory, an external storage device as a hard disk, and their input unit, output unit, communication unit, CPU , RAM, ROM, and a bus connected so that data can be exchanged between the external storage devices. If necessary, the hardware entity may be provided with a device (drive) that can read and write a recording medium such as a CD-ROM. A physical entity having such hardware resources includes a general-purpose computer.

  The external storage device of the hardware entity stores a program necessary for realizing the above functions and data necessary for processing the program (not limited to the external storage device, for example, reading a program) It may be stored in a ROM that is a dedicated storage device). Data obtained by the processing of these programs is appropriately stored in a RAM or an external storage device.

  In the hardware entity, each program stored in an external storage device (or ROM or the like) and data necessary for processing each program are read into a memory as necessary, and are interpreted and executed by a CPU as appropriate. . As a result, the CPU realizes a predetermined function (respective component requirements expressed as the above-described unit, unit, etc.).

  The present invention is not limited to the above-described embodiment, and can be appropriately changed without departing from the spirit of the present invention. In addition, the processing described in the above embodiment may be executed not only in time series according to the order of description but also in parallel or individually as required by the processing capability of the apparatus that executes the processing. .

  As described above, when the processing functions in the hardware entity (the apparatus of the present invention) described in the above embodiments are realized by a computer, the processing contents of the functions that the hardware entity should have are described by a program. Then, by executing this program on a computer, the processing functions in the hardware entity are realized on the computer.

  The program describing the processing contents can be recorded on a computer-readable recording medium. As the computer-readable recording medium, for example, any recording medium such as a magnetic recording device, an optical disk, a magneto-optical recording medium, and a semiconductor memory may be used. Specifically, for example, as a magnetic recording device, a hard disk device, a flexible disk, a magnetic tape, etc., and an optical disk, a DVD (Digital Versatile Disc), a DVD-RAM (Random Access Memory), a CD-ROM (Compact Disc Read Only Memory), a CD-R (Recordable). ) / RW (ReWritable) or the like can be used as a magneto-optical recording medium, MO (Magneto-Optical disc) or the like can be used, and EEP-ROM (Electronically Erasable and Programmable-Read Only Memory) or the like can be used as a semiconductor memory.

  The program is distributed by selling, transferring, or lending a portable recording medium such as a DVD or CD-ROM in which the program is recorded. Furthermore, the program may be distributed by storing the program in a storage device of the server computer and transferring the program from the server computer to another computer via a network.

  A computer that executes such a program first stores, for example, a program recorded on a portable recording medium or a program transferred from a server computer in its own storage device. When executing the process, the computer reads a program stored in its own recording medium and executes a process according to the read program. As another execution form of the program, the computer may directly read the program from a portable recording medium and execute processing according to the program, and the program is transferred from the server computer to the computer. Each time, the processing according to the received program may be executed sequentially. Further, the above-described processing may be executed by a so-called ASP (Application Service Provider) type service that realizes a processing function only by an execution instruction and result acquisition without transferring a program from the server computer to the computer. Good. Note that the program in this embodiment includes information that is used for processing by an electronic computer and that conforms to the program (data that is not a direct command to the computer but has a property that defines the processing of the computer).

  In this embodiment, a hardware entity is configured by executing a predetermined program on a computer. However, at least a part of these processing contents may be realized by hardware.

Claims (7)

A virtual dependency graph generation unit that generates a virtual dependency graph that enumerates and incorporates all the high-order primitives for a cryptographic protocol including a plurality of selectable high-order primitives during implementation;
An identifier assigning unit for assigning an identifier to each of the upper primitives;
A formula incorporation unit that incorporates a formula so that nodes corresponding to the identifier are counted in the evaluation function only if the identifier matches an appropriate implementation value;
An evaluation function linearization unit that linearizes the evaluation function and converts the evaluation function and the search space into an integer programming problem instance;
A pairing type conversion device. The pairing type conversion device according to claim 1,
The virtual dependency graph generation unit
A pairing conversion device that incorporates only one group element variable referenced from a plurality of virtual implementations into the virtual dependency graph. The pairing type conversion device according to claim 1 or 2,
The evaluation function linearization unit includes:
A pairing conversion device that converts the identifier into a binary variable. Virtual dependency graph generator pairing type converter, upon implementation, the cryptographic protocol including a plurality of upper primitive selectable, Luz Te' to generate a virtual dependency graph incorporating enumerating all the upper primitive Run
Identifier assignment of the pairing type conversion device, to each of the upper primitive, and executes the assignment away Te' flop identifiers,
Logical expression incorporating part of the pairing type conversion device, only when the identifier matches the value of the appropriate implementation, Luz Te' flop incorporating a formula so that the node corresponding to the identifier is counted in the evaluation function Run
Evaluation function linearizer pairing type conversion device, the evaluation function linearizes executes away step to convert the evaluation function and the search space integer programming problem instance
Pairing type conversion method. The pairing type conversion method according to claim 4,
The virtual dependency graph producing formation unit,
A pairing conversion method that incorporates only one group element variable referenced from a plurality of virtual implementations into the virtual dependency graph. The pairing type conversion method according to claim 4 or 5,
The evaluation function linearization unit includes:
A pairing conversion method for converting the identifier into a binary variable.   The program for functioning a computer as a pairing type conversion apparatus in any one of Claim 1 to 3.

Images