Kaman is security authentication scheme of mobile Ad Hoc networks. However, the author of Kaman didn’t verify security of the protocol by using formal method. Protocol Composition Logic (PCL) is formal verification logic of security protocol. This logic can simplify the process of protocol verification. This paper describes Kaman and analyzes its security properties in PCL. It is proved that Kaman can implement its security aim.