mirror of
https://github.com/johndoe6345789/tustu.git
synced 2026-04-24 13:45:00 +00:00
Add TLA+ specification and configuration for registration key generation algorithm
This commit is contained in:
141
spec/README.md
Normal file
141
spec/README.md
Normal file
@@ -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/)
|
||||
25
spec/RegistrationKey.cfg
Normal file
25
spec/RegistrationKey.cfg
Normal file
@@ -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
|
||||
366
spec/RegistrationKey.tla
Normal file
366
spec/RegistrationKey.tla
Normal file
@@ -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 == <<firstName, lastName, productName, email, secret,
|
||||
additionalField1, additionalField2, additionalField3,
|
||||
phase, byteArray, position, hashDigest, checksum, registrationKey>>
|
||||
|
||||
-----------------------------------------------------------------------------
|
||||
(* 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 <<firstName, lastName, productName, email, secret,
|
||||
additionalField1, additionalField2, additionalField3,
|
||||
position, hashDigest, checksum, registrationKey>>
|
||||
|
||||
-----------------------------------------------------------------------------
|
||||
(* 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 <<firstName, lastName, productName, email, secret,
|
||||
additionalField1, additionalField2, additionalField3,
|
||||
phase, hashDigest, checksum, registrationKey>>
|
||||
|
||||
CompleteReverse ==
|
||||
/\ phase = "Reverse"
|
||||
/\ position > Len(byteArray) \div 2
|
||||
/\ phase' = "Transform"
|
||||
/\ position' = 1
|
||||
/\ UNCHANGED <<firstName, lastName, productName, email, secret,
|
||||
additionalField1, additionalField2, additionalField3,
|
||||
byteArray, hashDigest, checksum, registrationKey>>
|
||||
|
||||
-----------------------------------------------------------------------------
|
||||
(* 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 <<firstName, lastName, productName, email, secret,
|
||||
additionalField1, additionalField2, additionalField3,
|
||||
phase, hashDigest, checksum, registrationKey>>
|
||||
|
||||
CompleteTransform ==
|
||||
/\ phase = "Transform"
|
||||
/\ position > Len(byteArray)
|
||||
/\ phase' = "SpecialCharHandle"
|
||||
/\ position' = 1
|
||||
/\ UNCHANGED <<firstName, lastName, productName, email, secret,
|
||||
additionalField1, additionalField2, additionalField3,
|
||||
byteArray, hashDigest, checksum, registrationKey>>
|
||||
|
||||
-----------------------------------------------------------------------------
|
||||
(* 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 <<firstName, lastName, productName, email, secret,
|
||||
additionalField1, additionalField2, additionalField3,
|
||||
phase, hashDigest, checksum, registrationKey>>
|
||||
|
||||
CompleteSpecialChar ==
|
||||
/\ phase = "SpecialCharHandle"
|
||||
/\ position > Len(byteArray)
|
||||
/\ phase' = IF secret = <<>> THEN "Complete" ELSE "HashInput"
|
||||
/\ position' = 1
|
||||
/\ UNCHANGED <<firstName, lastName, productName, email, secret,
|
||||
additionalField1, additionalField2, additionalField3,
|
||||
byteArray, hashDigest, checksum, registrationKey>>
|
||||
|
||||
-----------------------------------------------------------------------------
|
||||
(* Algorithm Phase 5: MD5 Hashing (Abstract) *)
|
||||
|
||||
PrepareHashInput ==
|
||||
/\ phase = "HashInput"
|
||||
/\ byteArray' = byteArray \o secret
|
||||
/\ phase' = "MD5Round1"
|
||||
/\ UNCHANGED <<firstName, lastName, productName, email, secret,
|
||||
additionalField1, additionalField2, additionalField3,
|
||||
position, hashDigest, checksum, registrationKey>>
|
||||
|
||||
MD5Round1 ==
|
||||
/\ phase = "MD5Round1"
|
||||
/\ phase' = "MD5Round2"
|
||||
/\ UNCHANGED <<firstName, lastName, productName, email, secret,
|
||||
additionalField1, additionalField2, additionalField3,
|
||||
byteArray, position, hashDigest, checksum, registrationKey>>
|
||||
|
||||
MD5Round2 ==
|
||||
/\ phase = "MD5Round2"
|
||||
/\ phase' = "MD5Discard"
|
||||
/\ UNCHANGED <<firstName, lastName, productName, email, secret,
|
||||
additionalField1, additionalField2, additionalField3,
|
||||
byteArray, position, hashDigest, checksum, registrationKey>>
|
||||
|
||||
MD5Discard ==
|
||||
/\ phase = "MD5Discard"
|
||||
/\ phase' = "MD5Round3"
|
||||
/\ UNCHANGED <<firstName, lastName, productName, email, secret,
|
||||
additionalField1, additionalField2, additionalField3,
|
||||
byteArray, position, hashDigest, checksum, registrationKey>>
|
||||
|
||||
MD5Round3 ==
|
||||
/\ phase = "MD5Round3"
|
||||
/\ phase' = "MD5Final"
|
||||
/\ UNCHANGED <<firstName, lastName, productName, email, secret,
|
||||
additionalField1, additionalField2, additionalField3,
|
||||
byteArray, position, hashDigest, checksum, registrationKey>>
|
||||
|
||||
MD5Final ==
|
||||
/\ phase = "MD5Final"
|
||||
/\ \E digest \in Seq(0..255):
|
||||
/\ Len(digest) = 16 \* MD5 produces 16 bytes
|
||||
/\ hashDigest' = digest
|
||||
/\ phase' = "Checksum"
|
||||
/\ UNCHANGED <<firstName, lastName, productName, email, secret,
|
||||
additionalField1, additionalField2, additionalField3,
|
||||
byteArray, position, checksum, registrationKey>>
|
||||
|
||||
-----------------------------------------------------------------------------
|
||||
(* 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 <<firstName, lastName, productName, email, secret,
|
||||
additionalField1, additionalField2, additionalField3,
|
||||
byteArray, position, hashDigest, registrationKey>>
|
||||
|
||||
-----------------------------------------------------------------------------
|
||||
(* Algorithm Phase 7: Combine Checksum and Hash *)
|
||||
|
||||
CombineChecksumHash ==
|
||||
/\ phase = "Combine"
|
||||
/\ byteArray' = checksum \o hashDigest \* 4 + 16 = 20 bytes
|
||||
/\ phase' = "Encode"
|
||||
/\ position' = 1
|
||||
/\ UNCHANGED <<firstName, lastName, productName, email, secret,
|
||||
additionalField1, additionalField2, additionalField3,
|
||||
hashDigest, checksum, registrationKey>>
|
||||
|
||||
-----------------------------------------------------------------------------
|
||||
(* 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 <<firstName, lastName, productName, email, secret,
|
||||
additionalField1, additionalField2, additionalField3,
|
||||
phase, byteArray, hashDigest, checksum>>
|
||||
|
||||
CompleteEncode ==
|
||||
/\ phase = "Encode"
|
||||
/\ position > Len(byteArray)
|
||||
/\ phase' = "Complete"
|
||||
/\ Len(registrationKey) = 20 \* Final key is 20 characters
|
||||
/\ UNCHANGED <<firstName, lastName, productName, email, secret,
|
||||
additionalField1, additionalField2, additionalField3,
|
||||
byteArray, position, hashDigest, checksum, registrationKey>>
|
||||
|
||||
-----------------------------------------------------------------------------
|
||||
(* 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'
|
||||
|
||||
=============================================================================
|
||||
Reference in New Issue
Block a user