diff --git a/spec/README.md b/spec/README.md new file mode 100644 index 00000000..b5e83fdd --- /dev/null +++ b/spec/README.md @@ -0,0 +1,141 @@ +# TLA+ Specification for Registration Key Algorithm + +This directory contains the formal TLA+ specification for the registration key generation algorithm. + +## Files + +- **RegistrationKey.tla** - Main TLA+ specification module +- **RegistrationKey.cfg** - TLC model checker configuration +- **README.md** - This file + +## Overview + +The specification models the registration key generation as a state machine with the following phases: + +1. **Init** - Initial state with input parameters +2. **Concatenate** - Combine input strings in specific order +3. **Reverse** - Reverse the byte array +4. **Transform** - Apply mathematical transformation to each byte +5. **SpecialCharHandle** - Handle special characters +6. **HashInput** - Prepare input for MD5 hashing +7. **MD5Round1-3** - Multiple rounds of MD5 updates +8. **MD5Final** - Final MD5 digest +9. **Checksum** - Generate CRC checksum +10. **Combine** - Combine checksum and hash +11. **Encode** - Base-32 encode the result +12. **Complete** - Final state with generated key + +## State Variables + +### Input Variables +- `firstName` - User's first name +- `lastName` - User's last name +- `productName` - Product name +- `email` - User's email address +- `secret` - Secret seed value (optional) +- `additionalField1-3` - Additional fields (optional) + +### Algorithm State +- `phase` - Current phase of execution +- `byteArray` - Working byte array +- `position` - Current position in array processing +- `hashDigest` - MD5 hash result (16 bytes) +- `checksum` - CRC checksum (4 bytes) +- `registrationKey` - Final 20-character key + +## Invariants + +### Type Invariant +Ensures all variables maintain their correct types throughout execution. + +### Phase Order +Enforces correct sequencing of algorithm phases: +- Complete phase must have 20-character key +- MD5 phases only occur when secret is provided + +### Deterministic +Same inputs always produce the same registration key. + +### No Empty Key +Complete phase must produce a non-empty key. + +## Properties + +### Correctness +The specification always maintains type invariants. + +### Termination +The algorithm eventually reaches the Complete phase. + +### Uniqueness +Different inputs produce different keys (with high probability due to cryptographic hash). + +## Running the Model Checker + +To check the specification with TLC: + +```bash +tlc RegistrationKey.tla -config RegistrationKey.cfg +``` + +### State Space Constraints + +To make model checking feasible, the configuration limits: +- firstName: ≤ 10 characters +- lastName: ≤ 10 characters +- productName: ≤ 15 characters +- email: ≤ 20 characters + +## Key Insights from Formal Specification + +1. **Deterministic**: The algorithm is completely deterministic - same inputs always produce the same output. + +2. **Phase-Based**: The algorithm progresses through well-defined phases in a specific order. + +3. **Byte-Level Operations**: Most operations work at the byte level with mathematical transformations. + +4. **Multiple Hash Rounds**: MD5 is applied multiple times (update-update-digest-update-digest) for additional complexity. + +5. **Character Set Variations**: Two different base-32 character sets are used depending on whether additional fields are present. + +6. **Fixed Output Length**: Always produces exactly 20 characters regardless of input length. + +## Abstract vs Concrete + +This TLA+ specification is more abstract than the Java implementation: + +- **MD5 Hash**: Modeled abstractly as a non-deterministic choice from valid 16-byte sequences. In practice, it's the actual MD5 algorithm. + +- **Checksum**: Modeled abstractly as a 4-byte sequence. In practice, it's a CRC calculation on the hash. + +- **Byte Values**: Constrained to valid ranges but not modeling exact arithmetic overflow behavior. + +This abstraction level is appropriate for verifying the algorithm's structure, phase ordering, and key properties without getting lost in cryptographic implementation details. + +## Verification Goals + +The TLA+ specification can verify: + +- ✓ Algorithm always terminates +- ✓ All phases execute in correct order +- ✓ Output is always correct length (20 chars) +- ✓ Type safety throughout execution +- ✓ Deterministic behavior +- ✗ Cryptographic security (out of scope for TLA+) +- ✗ Key collision probability (requires statistical analysis) + +## Extensions + +Possible extensions to this specification: + +1. **Multi-Algorithm Support**: Model all 4 variants (4, 5, 7, 8 parameters) +2. **Validation**: Add registration key validation logic +3. **Concurrent Usage**: Model multiple users generating keys simultaneously +4. **Key Database**: Model storage and lookup of generated keys +5. **Expiration**: Add time-based key expiration logic + +## References + +- [TLA+ Home](https://lamport.azurewebsites.net/tla/tla.html) +- [Learn TLA+](https://learntla.com/) +- [TLA+ Hyperbook](https://learntla.com/tla/) diff --git a/spec/RegistrationKey.cfg b/spec/RegistrationKey.cfg new file mode 100644 index 00000000..06d2af22 --- /dev/null +++ b/spec/RegistrationKey.cfg @@ -0,0 +1,25 @@ +\* TLA+ Configuration file for RegistrationKey specification + +CONSTANTS + MAX_STRING_LENGTH = 50 + ASCII_MIN = 32 + ASCII_MAX = 122 + +SPECIFICATION Spec + +INVARIANTS + TypeInvariant + ValidInputs + PhaseOrder + FinalKeyLength + NoEmptyKey + +PROPERTIES + Termination + +\* Constraint to limit state space for model checking +CONSTRAINT + /\ Len(firstName) <= 10 + /\ Len(lastName) <= 10 + /\ Len(productName) <= 15 + /\ Len(email) <= 20 diff --git a/spec/RegistrationKey.tla b/spec/RegistrationKey.tla new file mode 100644 index 00000000..54cbfaed --- /dev/null +++ b/spec/RegistrationKey.tla @@ -0,0 +1,366 @@ +-------------------------- MODULE RegistrationKey -------------------------- +(* + TLA+ Specification for Registration Key Generation Algorithm + + This specification describes the registration key generation algorithm + used for product licensing, including obfuscation, hashing, and encoding. +*) + +EXTENDS Integers, Sequences, FiniteSets, TLC + +CONSTANTS + MAX_STRING_LENGTH, \* Maximum length of input strings + ASCII_MIN, \* Minimum ASCII value (32) + ASCII_MAX \* Maximum ASCII value (122) + +VARIABLES + firstName, \* User's first name + lastName, \* User's last name + productName, \* Name of the product + email, \* User's email address + secret, \* Secret seed value + additionalField1, \* Optional additional field 1 + additionalField2, \* Optional additional field 2 + additionalField3, \* Optional additional field 3 + + \* Algorithm state variables + phase, \* Current phase of algorithm + byteArray, \* Working byte array + position, \* Current position in array + hashDigest, \* MD5 hash result + checksum, \* CRC checksum bytes + registrationKey \* Final registration key + +vars == <> + +----------------------------------------------------------------------------- +(* Type Definitions *) + +Phases == { + "Init", + "Concatenate", + "Reverse", + "Transform", + "SpecialCharHandle", + "HashInput", + "MD5Round1", + "MD5Round2", + "MD5Discard", + "MD5Round3", + "MD5Final", + "Checksum", + "Combine", + "Encode", + "Complete" +} + +ValidString(s) == + /\ s \in Seq(ASCII_MIN..ASCII_MAX) + /\ Len(s) > 0 + /\ Len(s) <= MAX_STRING_LENGTH + +Base32Charset == "123456789ABCDEFGHIJKLMNPQRSTUVWXYZ" +Base32EnhancedCharset == "23456789ABCDEFGHJKLMNPQRSTUVWXYZ" + +SpecialCharacters == {96, 92, 91, 93, 59, 46} \* `, \, [, ], ;, . + +----------------------------------------------------------------------------- +(* Initial State *) + +Init == + /\ firstName \in Seq(ASCII_MIN..ASCII_MAX) + /\ lastName \in Seq(ASCII_MIN..ASCII_MAX) + /\ productName \in Seq(ASCII_MIN..ASCII_MAX) + /\ email \in Seq(ASCII_MIN..ASCII_MAX) + /\ secret \in Seq(ASCII_MIN..ASCII_MAX) \cup {<<>>} + /\ additionalField1 \in Seq(ASCII_MIN..ASCII_MAX) \cup {<<>>} + /\ additionalField2 \in Seq(ASCII_MIN..ASCII_MAX) \cup {<<>>} + /\ additionalField3 \in Seq(ASCII_MIN..ASCII_MAX) \cup {<<>>} + /\ ValidString(firstName) + /\ ValidString(lastName) + /\ ValidString(productName) + /\ ValidString(email) + /\ phase = "Init" + /\ byteArray = <<>> + /\ position = 1 + /\ hashDigest = <<>> + /\ checksum = <<>> + /\ registrationKey = <<>> + +----------------------------------------------------------------------------- +(* Algorithm Phase 1: Concatenation *) + +Concatenate == + /\ phase = "Init" + /\ byteArray' = lastName \o productName \o firstName \o lastName \o email + /\ phase' = "Reverse" + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +(* Algorithm Phase 2: Byte Reversal *) + +ReverseBytes == + /\ phase = "Reverse" + /\ position <= Len(byteArray) \div 2 + /\ LET idx1 == position + idx2 == Len(byteArray) - position + 1 + temp == byteArray[idx1] + IN + /\ byteArray' = [byteArray EXCEPT + ![idx1] = byteArray[idx2], + ![idx2] = temp] + /\ position' = position + 1 + /\ UNCHANGED <> + +CompleteReverse == + /\ phase = "Reverse" + /\ position > Len(byteArray) \div 2 + /\ phase' = "Transform" + /\ position' = 1 + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +(* Algorithm Phase 3: Character Transformation *) + +TransformByte(b, idx) == + LET base == (b + ((b - 32) % 7)) - (idx % 4) + IN IF base > 122 THEN base - 9 ELSE base + +TransformBytes == + /\ phase = "Transform" + /\ position <= Len(byteArray) + /\ LET b == byteArray[position] + transformed == TransformByte(b, position - 1) + IN + /\ byteArray' = [byteArray EXCEPT ![position] = transformed] + /\ position' = position + 1 + /\ UNCHANGED <> + +CompleteTransform == + /\ phase = "Transform" + /\ position > Len(byteArray) + /\ phase' = "SpecialCharHandle" + /\ position' = 1 + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +(* Algorithm Phase 4: Special Character Handling *) + +HandleSpecialChar(b, idx) == + IF b \in SpecialCharacters + THEN b + 6 + (idx % 10) + ELSE b + +HandleSpecialChars == + /\ phase = "SpecialCharHandle" + /\ position <= Len(byteArray) + /\ LET b == byteArray[position] + adjusted == HandleSpecialChar(b, position - 1) + IN + /\ byteArray' = [byteArray EXCEPT ![position] = adjusted] + /\ position' = position + 1 + /\ UNCHANGED <> + +CompleteSpecialChar == + /\ phase = "SpecialCharHandle" + /\ position > Len(byteArray) + /\ phase' = IF secret = <<>> THEN "Complete" ELSE "HashInput" + /\ position' = 1 + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +(* Algorithm Phase 5: MD5 Hashing (Abstract) *) + +PrepareHashInput == + /\ phase = "HashInput" + /\ byteArray' = byteArray \o secret + /\ phase' = "MD5Round1" + /\ UNCHANGED <> + +MD5Round1 == + /\ phase = "MD5Round1" + /\ phase' = "MD5Round2" + /\ UNCHANGED <> + +MD5Round2 == + /\ phase = "MD5Round2" + /\ phase' = "MD5Discard" + /\ UNCHANGED <> + +MD5Discard == + /\ phase = "MD5Discard" + /\ phase' = "MD5Round3" + /\ UNCHANGED <> + +MD5Round3 == + /\ phase = "MD5Round3" + /\ phase' = "MD5Final" + /\ UNCHANGED <> + +MD5Final == + /\ phase = "MD5Final" + /\ \E digest \in Seq(0..255): + /\ Len(digest) = 16 \* MD5 produces 16 bytes + /\ hashDigest' = digest + /\ phase' = "Checksum" + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +(* Algorithm Phase 6: Checksum Generation *) + +GenerateChecksum == + /\ phase = "Checksum" + /\ \E crc \in Seq(0..255): + /\ Len(crc) = 4 \* 4-byte checksum + /\ checksum' = crc + /\ phase' = "Combine" + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +(* Algorithm Phase 7: Combine Checksum and Hash *) + +CombineChecksumHash == + /\ phase = "Combine" + /\ byteArray' = checksum \o hashDigest \* 4 + 16 = 20 bytes + /\ phase' = "Encode" + /\ position' = 1 + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +(* Algorithm Phase 8: Base-32 Encoding *) + +Base32Encode(b, charset) == + LET charsetLen == Len(charset) + idx == (IF b < 0 THEN -b ELSE b) % charsetLen + IN charset[idx + 1] + +EncodeBytes == + /\ phase = "Encode" + /\ position <= Len(byteArray) + /\ LET charset == IF additionalField1 = <<>> /\ additionalField2 = <<>> + THEN Base32Charset + ELSE Base32EnhancedCharset + b == byteArray[position] + encoded == Base32Encode(b, charset) + IN + /\ registrationKey' = Append(registrationKey, encoded) + /\ position' = position + 1 + /\ UNCHANGED <> + +CompleteEncode == + /\ phase = "Encode" + /\ position > Len(byteArray) + /\ phase' = "Complete" + /\ Len(registrationKey) = 20 \* Final key is 20 characters + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +(* Next State Relation *) + +Next == + \/ Concatenate + \/ ReverseBytes + \/ CompleteReverse + \/ TransformBytes + \/ CompleteTransform + \/ HandleSpecialChars + \/ CompleteSpecialChar + \/ PrepareHashInput + \/ MD5Round1 + \/ MD5Round2 + \/ MD5Discard + \/ MD5Round3 + \/ MD5Final + \/ GenerateChecksum + \/ CombineChecksumHash + \/ EncodeBytes + \/ CompleteEncode + +Spec == Init /\ [][Next]_vars + +----------------------------------------------------------------------------- +(* Invariants *) + +TypeInvariant == + /\ phase \in Phases + /\ byteArray \in Seq(Int) + /\ position \in Nat + /\ hashDigest \in Seq(0..255) + /\ checksum \in Seq(0..255) + /\ registrationKey \in Seq(Int) + +ValidInputs == + /\ ValidString(firstName) + /\ ValidString(lastName) + /\ ValidString(productName) + /\ ValidString(email) + +PhaseOrder == + /\ phase = "Complete" => Len(registrationKey) = 20 + /\ phase \in {"MD5Round1", "MD5Round2", "MD5Discard", "MD5Round3", "MD5Final"} + => secret # <<>> + +FinalKeyLength == + phase = "Complete" => Len(registrationKey) = 20 + +Deterministic == + \* Same inputs always produce the same key + /\ phase = "Complete" + /\ phase' = "Complete" + => registrationKey = registrationKey' + +NoEmptyKey == + phase = "Complete" => registrationKey # <<>> + +----------------------------------------------------------------------------- +(* Properties *) + +THEOREM Correctness == Spec => []TypeInvariant + +THEOREM Termination == Spec => <>(phase = "Complete") + +THEOREM Uniqueness == + \* Different inputs produce different keys (with high probability) + /\ Spec + /\ firstName # firstName' + /\ phase = "Complete" + /\ phase' = "Complete" + => registrationKey # registrationKey' + +=============================================================================