The AES-KW(P) proofs include SAW files related to AES-GCM in order to bring in the required definitions related to AES. The AES-GCM proof will need to be refactored a bit to allow other proofs to include only AES-GCM definitions. In order to support this refactoring, a similar refactoring will need to be performed in the cryptol-specs repository.
The AES-KW(P) proofs include SAW files related to AES-GCM in order to bring in the required definitions related to AES. The AES-GCM proof will need to be refactored a bit to allow other proofs to include only AES-GCM definitions. In order to support this refactoring, a similar refactoring will need to be performed in the cryptol-specs repository.