examples

Documentation

Index

• func ChangePIN(counter uint, pin Pin) bool
• func CheckContinouslyChangingPIN(pin Pin) bool
• func CheckPIN(attempt uint, pin Pin) bool
• func CheckPIN1(digits ...int) bool
• func CheckPIN2(digits [4]int) bool
• func CheckPIN3(attempt int, digits [4]int) bool
• func CheckPIN4(counter, attempt int, digits [4]int) bool
• func CheckUnknownPIN(attempt uint, pin Pin) bool
• func SlicesEqual[S1, S2 ~[]E, E comparable](s1 S1, s2 S2) bool
• func WithResetCheckPIN(attempt uint, pin Pin) bool
• type Pin
  • func (pin Pin) Valid() bool

Functions

func ChangePIN

func ChangePIN(counter uint, pin Pin) bool

assume: forall e. pin.Valid() // Valid PIN assume: forall e0. exists e1. e0.counter > 0; -> e1.counter == e0.counter - 1 // Continous Counter assume: forall e0 e1. e1.counter == e0.counter + 1; -> !SlicesEqual(e0.pin, e1.pin) // No Immediate Duplicate guarantee: forall e0. e0.counter == 0; -> SlicesEqual(e0.pin, []uint{0, 0, 0, 0}) // Inital PIN 0000 guarantee: forall e0 e1. math.Abs(e0._duration - e1._duration) <= 0.1 * time.Second // No Timing Side Channel guarantee: "TODO: No pin must be the reversal of another." // guarantee: forall e0. e0.ret0 -> forall e1. e1.ret0 && e1._time < e0._time;

-> e1._time + 15 * time.Minute <= e0._time			// Atleast 15 Minute Between Successful Changes

func CheckContinouslyChangingPIN

func CheckContinouslyChangingPIN(pin Pin) bool

assume: forall e. pin.Valid() // Valid PIN guarantee: forall e0 e1. math.Abs(e0._duration - e1._duration) <= 0.1 * time.Second // No Time Side Channel

func CheckPIN

func CheckPIN(attempt uint, pin Pin) bool

assume: forall e. pin.Valid() && e.attempt > 0 // Valid PIN and Attempt assume: forall e0. exists e1. e0.attempt > 1; -> e1.attempt == e0.attempt - 1 // Continous Attempts assume: forall e0 e1. e0._time < e1._time; <-> e0.attempt < e1.attempt // Attempts Increment on Consecutive Calls assume: forall e0 e1. e0._id != e1._id; <-> e0.attempt != e1.attempt // Unique Attempts guarantee: forall e. e.ret0; <-> e.attempt <= 3 && SlicesEqual(e.pin, []uint{3, 1, 4, 1}) // Successful Check guarantee: forall e0 e1. e0.ret0 && e1.ret0; -> SlicesEqual(e0.pin, e1.pin) // Exactly One Correct PIN guarantee: forall e0 e1. math.Abs(e0._duration - e1._duration) <= 0.1 * time.Second // No Timing Side Channel

func CheckPIN1

func CheckPIN1(digits ...int) bool

guarantee: forall e. e.ret == (len(digits) == 4 &&

digits[0] == 0 && digits[1] == 1 && digits[2] == 2 && digits[3] == 3)

guarantee: forall e0 e1. math.Abs(e0.time - e1.time) <= 0.1 * time.Second For all pairs if one is correct the other with different digits is incorrect. gurantee forall e0 e1. e0.ret && !slices.Equal(e0.digits, e1.digits); -> !e1.ret

func CheckPIN2

func CheckPIN2(digits [4]int) bool

guarantee: forall e.

e.ret == (digits[0] == 0 && digits[1] == 1 && digits[2] == 2 && digits[3] == 3)

guarantee: forall e0 e1. math.Abs(e0.time - e1.time) <= 0.1 * time.Second

func CheckPIN3

func CheckPIN3(attempt int, digits [4]int) bool

All pairs of executions which are not the same does not have the same attempt. Ergo, the attempt shoudl always be different between executions. assume: forall e0 e1. e0 != e1; -> e0.attempt != e1.attempt guarantee: forall e.

e.ret == (e.attempt <= 3 &&
	digits[0] == 0 && digits[1] == 1 && digits[2] == 2 && digits[3] == 3)

guarantee: forall e0 e1. math.Abs(e0.time - e1.time) <= 0.1 * time.Second

func CheckPIN4

func CheckPIN4(counter, attempt int, digits [4]int) bool

guarantee: forall e.

e.ret == (e.attempt <= 3 &&
	digits[0] == 0 && digits[1] == 1 && digits[2] == 2 && digits[3] == 3)

guarantee: forall e0 e1. math.Abs(e0.time - e1.time) <= 0.1 * time.Second guarantee: forall e0 e1. e0.counter >= e1.counter; -> e0.attempt >= e1.attempt

func CheckUnknownPIN

func CheckUnknownPIN(attempt uint, pin Pin) bool

assume: forall e. pin.Valid() && e.attempt > 0 // Valid PIN and Attempt assume: forall e0. exists e1. e0.attempt > 1; -> e1.attempt == e0.attempt - 1 // Continous Attempts assume: forall e0 e1. e0._time < e1._time; <-> e0.attempt < e1.attempt // Attempts Increment on Consecutive Calls assume: forall e0 e1. e0._id != e1._id; <-> e0.attempt != e1.attempt // Unique Attempts guarantee: forall e0 e1. e0.ret0 && e1.ret0; -> SlicesEqual(e0.pin, e1.pin) // Exactly One Correct PIN guarantee: forall e0 e1. math.Abs(e0._duration - e1._duration) <= 0.1 * time.Second // No Timing Side Channel

func SlicesEqual

func SlicesEqual[S1, S2 ~[]E, E comparable](s1 S1, s2 S2) bool

func WithResetCheckPIN

func WithResetCheckPIN(attempt uint, pin Pin) bool

assume: forall e. pin.Valid() && e.attempt > 0 // Valid PIN and Attempt assume: forall e0. exists e1. e0.attempt > 1; -> e1.attempt == e0.attempt - 1 // Continous Attempts assume: forall e0 e1. e0._time + time.Minute <= e1._time; -> e1.attempt == 1 // Reset After 1 Minute guarantee: forall e. e.ret0; <-> e.attempt <= 3 && SlicesEqual(e.pin, []uint{3, 1, 4, 1}) // Successful Check guarantee: forall e0 e1. e0.ret0 && e1.ret0; -> SlicesEqual(e0.pin, e1.pin) // Exactly One Correct PIN guarantee: forall e0 e1. math.Abs(e0._duration - e1._duration) <= 0.1 * time.Second // No Timing Side Channel

Types

type Pin

type Pin []uint

func (Pin) Valid

func (pin Pin) Valid() bool