Security is considered one of the main challenges for software oriented architectures (SOA) [1,2]. For this reason, several standards have been developed around WS-Security. However, these security standards usually hinder interoperability, one of the main pillars of Web service technologies. Software adaptation  is a sound solution where an adaptor is deployed in the middle of the communication to overcome signature, behavioural and QoS incompatibilities between services. This is particularly important when dealing with stateful services (such as Windows Workflows or WS-BPEL processes) where any mismatch in the sequence of messages might lead the orchestration to a deadlock situation. We proposed security adaptation contracts  as concise and versatile specifications of how such incompatibilities must be solved. Nonetheless, synthesising an adaptor compliant with a given contract is not an easy task where concurrency issues must be kept in mind and security attacks must be analysed and prevented. In this paper, we present an adaptor synthesis, verification and refinement process based on security adaptation contracts which succeeds in overcoming incompatibilities among services and prevents secrecy attacks. We extended the ITACA toolbox  for synthesis and deadlock analysis and we integrated it with a variant of CCS , called Crypto-CCS , to verify and refine adaptors based on partial model checking and logical satisfiability techniques.