Suppose you are given two isomorphic graphs $G$ and $H$. Is there an efficient way of defining an isomorphism $\phi:V(G) \to V(H)$ if we already know they are isomorphic? Or is it just a guess and check process?

A metaanswer: knowing that the answer is yes, for any NP search problem (regardless of completeness), does not help much in finding the answer. The reason is that, if you had an algorithm A that found answers within some small known time bound T(n) for yesinstances of size n, but took much longer on noinstances, you could instead run a modified version of algorithm A that runs either until it finds the answer or until time T(n) has elapsed, and then gives up. The modified version is just as fast on yesinstances, but runs correctly within the same time bound on noinstances. So the "if we already know they are isomorphic" part of your question is close to meaningless. That said, there are a lot of things one can do other than naive guessing and checking. The known time bounds for arbitrary graphs are exponential in the square root of the number of vertices, much faster than the factorial time you would get for guessing all possible permutations, and there are many classes of graphs for which graph isomorphisms can be found in polynomial time — see Wikipedia on the graph isomorphism problem. For practical graph isomorphism checking, Victor's suggestion of just downloading and running nauty is a good one. 


The other answers have treated the case of finite graphs, but there is something interesting to say about infinite graphs as well. For example, we might consider the case of computable graphs. A graph is computable if it has a computable edge relation on the vertex set of natural numbers. It is quite natural to inquire of isomorphic computable graphs, whether they have a computable isomorphism. Question. If $G$ and $H$ are computable graphs and isomorphic, must there be a computable isomorphism? I hope you will find it interesting to learn that the answer is No. To see this, let me describe two isomorphic graphs, which will both be trees of height 2, having infinitely many leaves on level $1$ and infinitely many leaves on level $2$, but no splitting except at the root. On the one hand, we can easily build a computable such graph $G$, by using $0$ as the root, the remaining even numbers as the level $1$ nodes, and giving exactly the multiples of $4$ a successor on level $2$, using the odd numbers. Next, let me describe another computable presentation $H$ of this graph. We again use $0$ as the root and the remaining even numbers $2n$ as the level one nodes. But this time, we give $2n$ a successor, using the $k^{\rm th}$ odd number in the construction, only if program $n$ halts on input $0$ in less than time $k$. The graphs $G$ and $H$ are certainly isomorphic, because of their trivial form, but there can be no computable isomorphism between them, since any isomorphism would have to send the node $2n$ in $H$ either to a multiple of $4$ or not, and this would reveal whether it gets a successor in $G$, which would in turn tells us whether the program $n$ halts or not, solving the halting problem. So there can be no such computable isomorphism. QED The argument generalizes to oracles. That is, for any Turing degree $d$, there are isomorphic graphs that are computable from oracle $d$, but no isomorphism between them is computable from $d$. Thus, in the infinite case, one answer to your question is that you cannot compute the isomorphism of isomorphic graphs $G$ and $H$ just knowing $G$ and $H$. The isomorphism may simply have a greater Turing degree. More generally, this article by Csima, Khoussainov and Liu investigates the class of computably categorical graphs, the graphs $G$ that have the property that any two computable presentations of $G$ should be computably isomorphic. I discuss the issues of computable categoricity in this MO answer, which asked whether there could be equivalence without us being able to calculate it, a question for which the subject of computable model theory provides numerous answers. And there is more to say when one moves to uncountable graphs... 


It's still an open problem whether or not graph isomorphism is NP complete, though most cognoscenti in the computational complexity believe it is not. You might look at nauty, Brendan McKay's program which can do this (and more) fairly efficiently for even quite large graphs  http://cs.anu.edu.au/~bdm/nauty/ 


As David points out, just knowing that the two graphs are isomorphic can't help you produce an isomorphism, as you could have just assumed this in the first place for any input, and then checked whether your algorithm really produces an isomorphism. However, if you have an algorithm that always solves the decision problem "is G isomorphic to H?" then it can be used to produce an isomorphism between any two graphs that are isomorphic. This is similar to the fact that if you have some method of answering whether a given 3SAT instance is satisfiable, you can use that method to produce a certificate (an assignment of variables that makes the formula true). This property is known as selfreducibility, and is explained in these lecture notes. 

