![](/common/images/spacer.gif) |
![](/common/images/spacer.gif) |
![](/common/images/spacer.gif) |
![](/common/images/spacer.gif) |
![](/common/images/spacer.gif) |
![](/images/database/grey-line.gif) |
![](/images/database/grey-line.gif) |
![](/common/images/spacer.gif) |
![](/common/images/spacer.gif) A Method of Formal Verification of Cryptographic Circuits
![](/common/images/spacer.gif) |
![](/common/images/spacer.gif) |
![](/common/images/spacer.gif) |
![](/images/database/grey-line.gif) |
![](/images/database/grey-line.gif) |
![](/common/images/spacer.gif) |
![](/common/images/spacer.gif)
Organization: | Toshiba Techno Center, Inc., Tokyo, Japan |
![](/common/images/spacer.gif) |
![](/common/images/spacer.gif) |
![](/common/images/spacer.gif) |
![](/images/database/grey-line.gif) |
![](/images/database/grey-line.gif) |
![](/common/images/spacer.gif) |
![](/common/images/spacer.gif)
Journal of Electronic Testing |
![](/common/images/spacer.gif) |
![](/common/images/spacer.gif) |
![](/common/images/spacer.gif) |
![](/images/database/grey-line.gif) |
![](/images/database/grey-line.gif) |
![](/common/images/spacer.gif) |
![](/common/images/spacer.gif) In this letter we report the formal verification of encryption and decryption circuits. After we describe algebraically a simple modular arithmetic circuit at both function and logic levels, we apply the symbolic manipulation of Mathematica.
![](/common/images/spacer.gif) |
![](/common/images/spacer.gif) |
![](/common/images/spacer.gif) |
![](/images/database/grey-line.gif) |
![](/images/database/grey-line.gif) |
![](/common/images/spacer.gif) |
![](/common/images/spacer.gif)
![](/common/images/spacer.gif) |
![](/common/images/spacer.gif) |