Communication systems in aviation tend to focus on safety rather than security. Protocols such as ADS-B are known to use plain-text, unauthenticated messages and thus are open to various attacks. Controller-Pilot Data Communication Link is no exception and was shown vulnerable also in practice. In this paper, we propose a cryptographic mechanism to provide secure mobility for CPDLC that can enable data encryption and authentication. The protocol is formally verified with the Proverif tool. We also estimate the byte overhead in CPDLC use.