-
Notifications
You must be signed in to change notification settings - Fork 12
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Shubham Chaturvedi
committed
Dec 7, 2024
1 parent
74b4972
commit 8066826
Showing
14 changed files
with
866 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
89 changes: 89 additions & 0 deletions
89
AwsCryptographyPrimitives/runtimes/go/ImplementationFromDafny-go/AESEncryption/externs.go
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,89 @@ | ||
package AESEncryption | ||
|
||
import ( | ||
"crypto/aes" | ||
"crypto/cipher" | ||
"fmt" | ||
|
||
"github.com/aws/aws-cryptographic-material-providers-library/primitives/AwsCryptographyPrimitivesTypes" | ||
"github.com/dafny-lang/DafnyRuntimeGo/v4/dafny" | ||
"github.com/dafny-lang/DafnyStandardLibGo/Wrappers" | ||
) | ||
|
||
var m_AESEncryption struct { | ||
AES_GCM CompanionStruct_Default___ | ||
} | ||
|
||
func (CompanionStruct_Default___) AESDecryptExtern(algo AwsCryptographyPrimitivesTypes.AES__GCM, key dafny.Sequence, cipherText dafny.Sequence, authTag dafny.Sequence, iv dafny.Sequence, aad dafny.Sequence) Wrappers.Result { | ||
keyBytes := dafny.ToByteArray(key) | ||
cipherTextBytes := dafny.ToByteArray(cipherText) | ||
authTagBytes := dafny.ToByteArray(authTag) | ||
ivBytes := dafny.ToByteArray(iv) | ||
aadBytes := dafny.ToByteArray(aad) | ||
|
||
if algo.Dtor_keyLength() != int32(len(keyBytes)) { | ||
return Wrappers.Companion_Result_.Create_Failure_(AwsCryptographyPrimitivesTypes.Companion_Error_.Create_AwsCryptographicPrimitivesError_(dafny.SeqOfChars([]dafny.Char(fmt.Errorf("algorithm key length %d doesn't match actual key length %d ", algo.Dtor_keyLength(), len(keyBytes)).Error())...))) | ||
|
||
} | ||
|
||
if algo.Dtor_ivLength() != int32(len(ivBytes)) { | ||
return Wrappers.Companion_Result_.Create_Failure_(AwsCryptographyPrimitivesTypes.Companion_Error_.Create_AwsCryptographicPrimitivesError_(dafny.SeqOfChars([]dafny.Char(fmt.Errorf("algorithm iv length %d doesn't match actual iv length %d ", algo.Dtor_ivLength(), len(ivBytes)).Error())...))) | ||
} | ||
|
||
if algo.Dtor_tagLength() != int32(len(authTagBytes)) { | ||
return Wrappers.Companion_Result_.Create_Failure_(AwsCryptographyPrimitivesTypes.Companion_Error_.Create_AwsCryptographicPrimitivesError_(dafny.SeqOfChars([]dafny.Char(fmt.Errorf("algorithm tag length %d doesn't match actual tag length %d ", algo.Dtor_tagLength(), len(authTagBytes)).Error())...))) | ||
} | ||
|
||
block, err := aes.NewCipher(keyBytes) | ||
if err != nil { | ||
return Wrappers.Companion_Result_.Create_Failure_(AwsCryptographyPrimitivesTypes.Companion_Error_.Create_AwsCryptographicPrimitivesError_(dafny.SeqOfChars([]dafny.Char(err.Error())...))) | ||
} | ||
|
||
if algo.Is_AES__GCM() { | ||
gcm, err := cipher.NewGCM(block) | ||
if err != nil { | ||
return Wrappers.Companion_Result_.Create_Failure_(AwsCryptographyPrimitivesTypes.Companion_Error_.Create_AwsCryptographicPrimitivesError_(dafny.SeqOfChars([]dafny.Char(err.Error())...))) | ||
} | ||
|
||
plaintext, err := gcm.Open(nil, ivBytes, append(cipherTextBytes, authTagBytes...), aadBytes) | ||
if err != nil { | ||
return Wrappers.Companion_Result_.Create_Failure_(AwsCryptographyPrimitivesTypes.Companion_Error_.Create_AwsCryptographicPrimitivesError_(dafny.SeqOfChars([]dafny.Char(err.Error())...))) | ||
} | ||
return Wrappers.Companion_Result_.Create_Success_(dafny.SeqOfBytes(plaintext)) | ||
} | ||
return Wrappers.Companion_Result_.Create_Failure_(false) | ||
} | ||
|
||
func (CompanionStruct_Default___) AESEncryptExtern(algo AwsCryptographyPrimitivesTypes.AES__GCM, iv dafny.Sequence, key dafny.Sequence, msg dafny.Sequence, aad dafny.Sequence) Wrappers.Result { | ||
keyBytes := dafny.ToByteArray(key) | ||
ivBytes := dafny.ToByteArray(iv) | ||
aadBytes := dafny.ToByteArray(aad) | ||
|
||
if algo.Dtor_keyLength() != int32(len(keyBytes)) { | ||
return Wrappers.Companion_Result_.Create_Failure_(AwsCryptographyPrimitivesTypes.Companion_Error_.Create_AwsCryptographicPrimitivesError_(dafny.SeqOfChars([]dafny.Char(fmt.Errorf("algorithm key length %d doesn't match actual key length %d ", algo.Dtor_keyLength(), len(keyBytes)).Error())...))) | ||
|
||
} | ||
|
||
if algo.Dtor_ivLength() != int32(len(ivBytes)) { | ||
return Wrappers.Companion_Result_.Create_Failure_(AwsCryptographyPrimitivesTypes.Companion_Error_.Create_AwsCryptographicPrimitivesError_(dafny.SeqOfChars([]dafny.Char(fmt.Errorf("algorithm iv length %d doesn't match actual iv length %d ", algo.Dtor_ivLength(), len(ivBytes)).Error())...))) | ||
} | ||
|
||
block, err := aes.NewCipher(keyBytes) | ||
if err != nil { | ||
return Wrappers.Companion_Result_.Create_Failure_(AwsCryptographyPrimitivesTypes.Companion_Error_.Create_AwsCryptographicPrimitivesError_(dafny.SeqOfChars([]dafny.Char(err.Error())...))) | ||
} | ||
|
||
if algo.Is_AES__GCM() { | ||
gcm, err := cipher.NewGCM(block) | ||
if err != nil { | ||
return Wrappers.Companion_Result_.Create_Failure_(AwsCryptographyPrimitivesTypes.Companion_Error_.Create_AwsCryptographicPrimitivesError_(dafny.SeqOfChars([]dafny.Char(err.Error())...))) | ||
} | ||
|
||
cipherText := gcm.Seal(nil, ivBytes, dafny.ToByteArray(msg), aadBytes) | ||
if cipherText == nil { | ||
return Wrappers.Companion_Result_.Create_Failure_(AwsCryptographyPrimitivesTypes.Companion_Error_.Create_AwsCryptographicPrimitivesError_(dafny.SeqOfChars([]dafny.Char(fmt.Errorf("failed to do AES_GCM Encrypt with the given parameters").Error())...))) | ||
} | ||
return Wrappers.Companion_Result_.Create_Success_(AwsCryptographyPrimitivesTypes.Companion_AESEncryptOutput_.Create_AESEncryptOutput_(dafny.SeqOfBytes(cipherText[:len(cipherText)-gcm.Overhead()]), dafny.SeqOfBytes(cipherText[len(cipherText)-gcm.Overhead():]))) | ||
} | ||
return Wrappers.Companion_Result_.Create_Failure_(false) | ||
} |
25 changes: 25 additions & 0 deletions
25
AwsCryptographyPrimitives/runtimes/go/ImplementationFromDafny-go/AesKdfCtr/externs.go
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,25 @@ | ||
package AesKdfCtr | ||
|
||
import ( | ||
"crypto/aes" | ||
"crypto/cipher" | ||
|
||
dafny "github.com/dafny-lang/DafnyRuntimeGo/v4/dafny" | ||
"github.com/dafny-lang/DafnyStandardLibGo/Wrappers" | ||
) | ||
|
||
func AesKdfCtrStream(nonce dafny.Sequence, key dafny.Sequence, length uint32) Wrappers.Result { | ||
|
||
block, err := aes.NewCipher(dafny.ToByteArray(key)) | ||
|
||
if err != nil { | ||
panic(err) | ||
} | ||
|
||
stream := cipher.NewCTR(block, dafny.ToByteArray(nonce)) | ||
|
||
result := make([]byte, length) | ||
|
||
stream.XORKeyStream(result, make([]byte, length)) | ||
return Wrappers.Companion_Result_.Create_Success_(dafny.SeqOfBytes(result)) | ||
} |
Oops, something went wrong.