Formal and Precise Analysis of Soundness of Several Shuffling Schemes

Some of the most efficient shuffling schemes employ the same main idea to prove validity of shuffling. However, the principle behind the idea has not been explained in a completely formal and precise way. So formal guarantee of soundness of the shuffling schemes is not complete. Especially, it is unknown exactly how large the probability of failure of soundness is and exactly how strong soundness is. In this paper, why the proof mechanism guarantees validity of shuffling is formally proved to provide a formal guarantee of soundness of those shuffling schemes. Especially, the exact upper bound of the probability of failure of soundness is given to convincingly ensure soundness. Although we do not doubt soundness of most of the shuffling schemes, a formal and precise proof of their soundness is still valuable as it strengthens security guarantee of the schemes and removes a potential obstacle for their application to critical environments requiring formally guaranteed and measurable soundness. Moreover, the formal and precise proof shows that some shuffling scheme has serious problem in soundness.