The famous Square attacks against the Rijndael algorithm have taken advantage of the change of the balance of some bytes. Further study shows that the change of activity always happens before the change of balance, wh...The famous Square attacks against the Rijndael algorithm have taken advantage of the change of the balance of some bytes. Further study shows that the change of activity always happens before the change of balance, which builds the foundation for a new activity attack presented in this paper. In the activity attack, the round in which the activity changes is executed in an equivalent form to avoid the obstructive restriction of the subkeys of that round.The existence of the birthday paradox guarantees much fewer plaintexts necessary for activity attacks comparing with that for corresponding Square attacks. But no benefit may result from the new attacks performed independently because the activity attacks guess four instead of one key byte once. Only when both the balance property and the activity property are exploited at the same time can much better performance be obtained. The better performance in the simulation shows that the consuming time and chosen plaintexts necessary are both reduced to one tenth of those of the corresponding Square attacks. So the activity attacks could be viewed as an efficient supplement to the Square attacks.展开更多
Probabilistic techniques are widely used in the analysis of algorithms to estimate the computational complexity of algorithms or a computational problem.Traditionally,such analyses are performed using paper-and-pencil...Probabilistic techniques are widely used in the analysis of algorithms to estimate the computational complexity of algorithms or a computational problem.Traditionally,such analyses are performed using paper-and-pencil proofs and the results are sometimes validated using simulation techniques.These techniques are informal and thus may result in an inaccurate analysis.In this paper,we propose a formal technique for analyzing the expected time complexity of algorithms using higher-order-logic theorem proving.The approach calls for mathematically modeling the algorithm along with its inputs,using indicator random variables,in higher-order logic.This model is then used to formally reason about the expected time complexity of the underlying algorithm in a theorem prover.The paper includes the higher-order-logic formalization of indicator random variables,which are fundamental to the proposed infrastructure.In order to illustrate the practical effiectiveness and utilization of the proposed infrastructure,the paper also includes the analysis of algorithms for three well-known problems,i.e.,the hat-check problem,the birthday paradox and the hiring problem.展开更多
基金the National 973 Project(G1999035803)National 863 Grand Project(2002AA143021)and the National Cryptography Development Funds for the Tenth Five-year Project
文摘The famous Square attacks against the Rijndael algorithm have taken advantage of the change of the balance of some bytes. Further study shows that the change of activity always happens before the change of balance, which builds the foundation for a new activity attack presented in this paper. In the activity attack, the round in which the activity changes is executed in an equivalent form to avoid the obstructive restriction of the subkeys of that round.The existence of the birthday paradox guarantees much fewer plaintexts necessary for activity attacks comparing with that for corresponding Square attacks. But no benefit may result from the new attacks performed independently because the activity attacks guess four instead of one key byte once. Only when both the balance property and the activity property are exploited at the same time can much better performance be obtained. The better performance in the simulation shows that the consuming time and chosen plaintexts necessary are both reduced to one tenth of those of the corresponding Square attacks. So the activity attacks could be viewed as an efficient supplement to the Square attacks.
文摘Probabilistic techniques are widely used in the analysis of algorithms to estimate the computational complexity of algorithms or a computational problem.Traditionally,such analyses are performed using paper-and-pencil proofs and the results are sometimes validated using simulation techniques.These techniques are informal and thus may result in an inaccurate analysis.In this paper,we propose a formal technique for analyzing the expected time complexity of algorithms using higher-order-logic theorem proving.The approach calls for mathematically modeling the algorithm along with its inputs,using indicator random variables,in higher-order logic.This model is then used to formally reason about the expected time complexity of the underlying algorithm in a theorem prover.The paper includes the higher-order-logic formalization of indicator random variables,which are fundamental to the proposed infrastructure.In order to illustrate the practical effiectiveness and utilization of the proposed infrastructure,the paper also includes the analysis of algorithms for three well-known problems,i.e.,the hat-check problem,the birthday paradox and the hiring problem.
