Formalizing a Modal Logic for CCS in the HOL Theorem Prover