Abstract: Automatic proof for internet voting protocols is a hotspot issue in security protocol world. To our best knowledge, until now analysis of coercion-resistance and internet voting protocols with automatic tool in computational model does not exist. So in this study, we initiatively proposed the automatic framework of coercion-resistance and internet voting protocols based on computational model with active adversary. In the proposed framework observational equivalence is used to formalize coercion-resistance. At the same time we propose a method to prove the observational equivalence between the two processes have the same structure and differ only by the terms and term evaluations with mechanized tool CryptoVerif. Based on the proposed method to prove with CryptoVerif the observational equivalence, the proposed mechanized framework can be used to automatically analyze coercion-resistance of internet voting protocols with CryptoVerif.