feat: rename sensitive to encrypted and nonsensitive to signed (#175)

Author: ajewellamz

DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy

@@ -49,8 +49,8 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
  datatype CompoundBeacon = | CompoundBeacon (
  nameonly name: string ,
  nameonly split: Char ,
- nameonly sensitive: Option<SensitivePartsList> ,
- nameonly nonSensitive: Option<NonSensitivePartsList> ,
+ nameonly encrypted: Option<EncryptedPartsList> ,
+ nameonly signed: Option<SignedPartsList> ,
  nameonly constructors: Option<ConstructorList>
  )
  type CompoundBeaconList = x: seq<CompoundBeacon> | IsValid_CompoundBeaconList(x) witness *
@@ -222,6 +222,14 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
  datatype DynamoDbTablesEncryptionConfig = | DynamoDbTablesEncryptionConfig (
  nameonly tableEncryptionConfigs: DynamoDbTableEncryptionConfigList
  )
+ datatype EncryptedPart = | EncryptedPart (
+ nameonly name: string ,
+ nameonly prefix: Prefix
+ )
+ type EncryptedPartsList = x: seq<EncryptedPart> | IsValid_EncryptedPartsList(x) witness *
+ predicate method IsValid_EncryptedPartsList(x: seq<EncryptedPart>) {
+ ( 1 <= |x|  )
+}
  datatype GetBranchKeyIdFromDdbKeyInput = | GetBranchKeyIdFromDdbKeyInput (
  nameonly ddbKey: ComAmazonawsDynamodbTypes.Key
  )
@@ -303,15 +311,6 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
  nameonly cacheTTL: int32 ,
  nameonly maxCacheSize: int32
  )
- datatype NonSensitivePart = | NonSensitivePart (
- nameonly name: string ,
- nameonly prefix: Prefix ,
- nameonly loc: Option<TerminalLocation>
- )
- type NonSensitivePartsList = x: seq<NonSensitivePart> | IsValid_NonSensitivePartsList(x) witness *
- predicate method IsValid_NonSensitivePartsList(x: seq<NonSensitivePart>) {
- ( 1 <= |x|  )
-}
  datatype PlaintextPolicy =
 	| REQUIRE_WRITE_ALLOW_READ
 	| FORBID_WRITE_ALLOW_READ
@@ -324,12 +323,13 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
  nameonly versions: BeaconVersionList ,
  nameonly writeVersion: VersionNumber
  )
- datatype SensitivePart = | SensitivePart (
+ datatype SignedPart = | SignedPart (
  nameonly name: string ,
- nameonly prefix: Prefix
+ nameonly prefix: Prefix ,
+ nameonly loc: Option<TerminalLocation>
  )
- type SensitivePartsList = x: seq<SensitivePart> | IsValid_SensitivePartsList(x) witness *
- predicate method IsValid_SensitivePartsList(x: seq<SensitivePart>) {
+ type SignedPartsList = x: seq<SignedPart> | IsValid_SignedPartsList(x) witness *
+ predicate method IsValid_SignedPartsList(x: seq<SignedPart>) {
  ( 1 <= |x|  )
 }
  datatype SingleKeyStore = | SingleKeyStore (

DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy

@@ -244,13 +244,13 @@ list CompoundBeaconList {
 }
 
 @length(min: 1)
-list SensitivePartsList {
-  member: SensitivePart
+list EncryptedPartsList {
+  member: EncryptedPart
 }
 
 @length(min: 1)
-list NonSensitivePartsList {
-  member: NonSensitivePart
+list SignedPartsList {
+  member: SignedPart
 }
 
 @length(min: 1)
@@ -422,31 +422,31 @@ union VirtualTransform {
   segments : GetSegments
 }
 
-//= specification/searchable-encryption/beacons.md#sensitive-part-initialization
+//= specification/searchable-encryption/beacons.md#encrypted-part-initialization
 //= type=implication
-//# On initialization of a [sensitive part](#sensitive-part-initialization), the caller MUST provide:
+//# On initialization of a [encrypted part](#encrypted-part-initialization), the caller MUST provide:
 //#  * A name -- a string, the name of a standard beacon
 //#  * A prefix -- a string
 
-structure SensitivePart {
+structure EncryptedPart {
   @required
   name : String,
   @required
   prefix : Prefix
 }
 
-//= specification/searchable-encryption/beacons.md#non-sensitive-part-initialization
+//= specification/searchable-encryption/beacons.md#signed-part-initialization
 //= type=implication
-//# On initialization of a [non-sensitive part](#non-sensitive-part-initialization), the caller MUST provide:
+//# On initialization of a [signed part](#signed-part-initialization), the caller MUST provide:
 //#  * A name -- a string
 //#  * A prefix -- a string
 
-//= specification/searchable-encryption/beacons.md#non-sensitive-part-initialization
+//= specification/searchable-encryption/beacons.md#signed-part-initialization
 //= type=implication
-//# On initialization of a [non-sensitive parts](#non-sensitive-part-initialization), the caller MAY provide:
+//# On initialization of a [signed parts](#signed-part-initialization), the caller MAY provide:
 //# * A [terminal location](virtual.md#terminal-location) -- a string
 
-structure NonSensitivePart {
+structure SignedPart {
   @required
   name : String,
   @required
@@ -505,17 +505,17 @@ structure StandardBeacon {
 //= specification/searchable-encryption/beacons.md#compound-beacon-initialization
 //= type=implication
 //# On initialization of a Compound Beacon, the caller MAY provide:
-//#  * A list of [sensitive parts](#sensitive-part-initialization)
-//#  * A list of [non-sensitive parts](#non-sensitive-part-initialization)
+//#  * A list of [encrypted parts](#encrypted-part-initialization)
+//#  * A list of [signed parts](#signed-part-initialization)
 //#  * A list of constructors
 
 structure CompoundBeacon {
   @required
   name : String,
   @required
   split : Char,
-  sensitive : SensitivePartsList,
-  nonSensitive : NonSensitivePartsList,
+  encrypted : EncryptedPartsList,
+  signed : SignedPartsList,
   constructors : ConstructorList
 }
 

DynamoDbEncryption/dafny/DynamoDbEncryption/src/CompoundBeacon.dfy

@@ -24,39 +24,39 @@ module CompoundBeacon {
   type Prefix = x : string | 0 < |x| witness *
 
   datatype BeaconPart =
-    | Sensitive(prefix : Prefix, beacon : BaseBeacon.StandardBeacon)
-    | NonSensitive(prefix : Prefix, name : string, loc : TermLoc)
+    | Encrypted(prefix : Prefix, beacon : BaseBeacon.StandardBeacon)
+    | Signed(prefix : Prefix, name : string, loc : TermLoc)
   {
 
     function method getPrefix() : string
     {
       match this {
-        case Sensitive(p, b) => p
-        case NonSensitive(p, n, l) => p
+        case Encrypted(p, b) => p
+        case Signed(p, n, l) => p
       }
     }
 
     function method getName() : string
     {
       match this {
-        case Sensitive(p, b) => b.base.name
-        case NonSensitive(p, n, l) => n
+        case Encrypted(p, b) => b.base.name
+        case Signed(p, n, l) => n
       }
     }
 
     function method getString(item : DDB.AttributeMap, vf : VirtualFieldMap) : Result<Option<string>, Error>
     {
       match this {
-        case Sensitive(p, b) => VirtToString(b.loc, item, vf)
-        case NonSensitive(p, n, l) => VirtToString(l, item, vf)
+        case Encrypted(p, b) => VirtToString(b.loc, item, vf)
+        case Signed(p, n, l) => VirtToString(l, item, vf)
       }
     }
 
     function method GetFields(virtualFields : VirtualFieldMap) : seq<string>
     {
       match this {
-        case Sensitive(p, b) => b.GetFields(virtualFields)
-        case NonSensitive(p, n, l) =>
+        case Encrypted(p, b) => b.GetFields(virtualFields)
+        case Signed(p, n, l) =>
           if loc[0].key in virtualFields then
             virtualFields[loc[0].key].GetFields()
           else
@@ -88,47 +88,47 @@ module CompoundBeacon {
   function method MakeCompoundBeacon(
     base : BeaconBase,
     split : char,
-    parts : seq<BeaconPart>, // Non-Sensitive followed by Sensitive
-    numNonSensitive : nat,
+    parts : seq<BeaconPart>, // Signed followed by Encrypted
+    numSigned : nat,
     construct : ConstructorList
   )
     : (ret : Result<ValidCompoundBeacon, Error>)
-    requires numNonSensitive <= |parts|
-    requires OrderedParts(parts, numNonSensitive)
+    requires numSigned <= |parts|
+    requires OrderedParts(parts, numSigned)
 
     //= specification/searchable-encryption/beacons.md#initialization-failure
     //= type=implication
     //# Initialization MUST fail if any `prefix` in any [part](#part) is a prefix of
     //# the `prefix` of any other [part](#part).
     ensures ret.Success? ==> ret.value.ValidPrefixSet()
   {
-    var x := CompoundBeacon.CompoundBeacon(base, split, parts, numNonSensitive, construct);
+    var x := CompoundBeacon.CompoundBeacon(base, split, parts, numSigned, construct);
     var _ :- x.ValidPrefixSetResult();
     Success(x)
   }
 
   // are the parts properly ordered?
-  // that is, with the non-sensitive parts followed the sensitive parts
+  // that is, with the signed parts followed the encrypted parts
   predicate OrderedParts(p : seq<BeaconPart>, n : nat)
     requires n <= |p|
   {
-    && (forall x | 0 <= x < n :: p[x].NonSensitive?)
-    && (forall x | n <= x < |p| :: p[x].Sensitive?)
+    && (forall x | 0 <= x < n :: p[x].Signed?)
+    && (forall x | n <= x < |p| :: p[x].Encrypted?)
   }
 
   datatype CompoundBeacon = CompoundBeacon(
     base : BeaconBase,
     split : char,
     parts : seq<BeaconPart>,
-    numNonSensitive : nat,
+    numSigned : nat,
     construct : ConstructorList
   ) {
 
     predicate ValidState()
     {
       && ValidPrefixSet()
-      && numNonSensitive <= |parts|
-      && OrderedParts(parts, numNonSensitive)
+      && numSigned <= |parts|
+      && OrderedParts(parts, numSigned)
     }
 
     // no prefix is a prefix of another prefix
@@ -140,9 +140,9 @@ module CompoundBeacon {
         :: OkPrefixPair(x, y)
     }
 
-    // Does this beacon have any sensitive parts
+    // Does this beacon have any encrypted parts
     predicate method isEncrypted() {
-      numNonSensitive < |parts|
+      numSigned < |parts|
     }
 
     // find the part whose prefix matches this value
@@ -166,14 +166,14 @@ module CompoundBeacon {
         partFromPrefix(p[1..], value)
     }
 
-    // trim leading pieces that refer to nonsensitive parts
+    // trim leading pieces that refer to signed parts
     function method SkipSignedPieces(pieces : seq<string>) : Result<seq<string>, Error>
     {
       if |pieces| == 0 then
         Success(pieces)
       else
         var p :- partFromPrefix(parts, pieces[0]);
-        if p.Sensitive? then
+        if p.Encrypted? then
           Success(pieces)
         else
           SkipSignedPieces(pieces[1..])
@@ -477,9 +477,9 @@ module CompoundBeacon {
 
       //= specification/searchable-encryption/beacons.md#part-value-calculation
       //= type=implication
-      //# If the part is a [nonsensitive part](#non-sensitive-part-initialization),
+      //# If the part is a [signed part](#signed-part-initialization),
       //# the part value MUST be the concatenation of the part's prefix and the input string.
-      ensures part.NonSensitive? && ret.Success? ==>
+      ensures part.Signed? && ret.Success? ==>
                 && ret.value == part.prefix + data
                 && 0 < |ret.value|
                    //= specification/searchable-encryption/beacons.md#value-for-a-compound-beacon
@@ -489,10 +489,10 @@ module CompoundBeacon {
 
       //= specification/searchable-encryption/beacons.md#part-value-calculation
       //= type=implication
-      //# If the part is a [sensitive part](#sensitive-part-initialization),
+      //# If the part is a [encrypted part](#encrypted-part-initialization),
       //# the part value MUST be the concatenation of the part's prefix
       //# and the [string hash](#string-hash) of the input string.
-      ensures part.Sensitive? && ret.Success? ==>
+      ensures part.Encrypted? && ret.Success? ==>
                 && 0 < |ret.value|
                 && keys.Keys?
                 && part.beacon.hashStr(data, keys.value).Success?
@@ -504,11 +504,11 @@ module CompoundBeacon {
     {
       :- Need(split !in data, E("Value '" + data + "' for beacon part " + part.getName() + " contains the split character '" + [split] + "'."));
       match part {
-        case Sensitive(p, b) =>
+        case Encrypted(p, b) =>
           :- Need(keys.Keys?, E("Need KeyId for beacon " + b.base.name + " but no KeyId found in query."));
           var hash :- b.hashStr(data, keys.value);
           Success(part.prefix + hash)
-        case NonSensitive =>
+        case Signed =>
           Success(part.prefix + data)
       }
     }