diff --git a/examples/generate_2fa_token.adb b/examples/generate_2fa_token.adb index 750a616..6fac5c2 100644 --- a/examples/generate_2fa_token.adb +++ b/examples/generate_2fa_token.adb @@ -15,7 +15,6 @@ is Import, Convention => C, External_Name => "time"; - package TOTP is new OTP.T; begin pragma Assert (LSC.Byte_Arrays.Natural_Index'Last / 5 > 32); pragma Warnings (Off, "no Global contract"); @@ -26,7 +25,7 @@ begin (for all C of Ada.Command_Line.Argument (1) => Base32.Valid_Base32_Character (C))) then - Ada.Text_IO.Put_Line (OTP.Image (TOTP.TOTP ( + Ada.Text_IO.Put_Line (OTP.Image (OTP.T.TOTP ( Base32.Decode (Ada.Command_Line.Argument (1)), Time (System.Null_Address)), 6)); else diff --git a/src/base32.adb b/src/base32.adb index 106c3fc..c4ade46 100644 --- a/src/base32.adb +++ b/src/base32.adb @@ -123,12 +123,12 @@ is is N : Byte; begin - case Character'Pos (C) is - when 97 .. 122 => + case C is + when 'a' .. 'z' => N := Byte (Character'Pos (C) - 97); - when 65 .. 90 => + when 'A' .. 'Z' => N := Byte (Character'Pos (C) - 65); - when 50 .. 55 => + when '2' .. '7' => N := Byte (Character'Pos (C) - 24); when others => raise Constraint_Error; diff --git a/src/otp-h.ads b/src/otp-h.ads index 898af83..21b2391 100644 --- a/src/otp-h.ads +++ b/src/otp-h.ads @@ -24,6 +24,8 @@ is Depends => (HOTP'Result => (Key, Counter)), Pre => Key'Length <= 64; +private + -- @private Only used to generate the token function Extract (Mac : HMAC.HMAC_Type) diff --git a/src/otp-t.adb b/src/otp-t.adb index 5a6f555..05a4b95 100644 --- a/src/otp-t.adb +++ b/src/otp-t.adb @@ -1,8 +1,7 @@ -with Interfaces; with OTP.H; -use all type Interfaces.Unsigned_64; package body OTP.T +with SPARK_Mode is ---------- @@ -10,8 +9,10 @@ is ---------- function TOTP - (Key : LSC.Byte_Arrays.Byte_Array_Type; - Time : LSC.Types.Word64) + (Key : LSC.Byte_Arrays.Byte_Array_Type; + Time : LSC.Types.Word64; + X : LSC.Types.Word64 := 30; + T0 : LSC.Types.Word64 := 0) return OTP_Token is begin diff --git a/src/otp-t.ads b/src/otp-t.ads index bed052d..1d40bd3 100644 --- a/src/otp-t.ads +++ b/src/otp-t.ads @@ -1,30 +1,31 @@ with LSC.Types; with LSC.Byte_Arrays; +use all type LSC.Types.Word64; -- @summary -- Time based One-Time-Pad -- -- @description -- Calculates the Time based One-Time-Pad based on RFC 6238 --- --- @param X Time step size --- @param T0 Reference time -generic - X : LSC.Types.Word64 := 30; - T0 : LSC.Types.Word64 := 0; + package OTP.T +with SPARK_Mode is -- Calculates the TOTP Token from a given key and time offset -- @param HMAC key -- @param Current time + -- @param X Time step size + -- @param T0 Reference time -- @return TOTP Token as 31bit word function TOTP (Key : LSC.Byte_Arrays.Byte_Array_Type; - Time : LSC.Types.Word64) + Time : LSC.Types.Word64; + X : LSC.Types.Word64 := 30; + T0 : LSC.Types.Word64 := 0) return OTP_Token with - Depends => (TOTP'Result => (Key, Time)), - Pre => Key'Length <= 64; + Depends => (TOTP'Result => (Key, Time, X, T0)), + Pre => Key'Length <= 64 and X > 0; end OTP.T; diff --git a/src/otp.adb b/src/otp.adb index ecdec30..38d67ef 100644 --- a/src/otp.adb +++ b/src/otp.adb @@ -15,9 +15,7 @@ is Value : OTP_Value (1 .. D) := (others => '0'); begin for I in reverse Value'Range loop - pragma Loop_Invariant (for all C of Value => - Character'Pos (C) > 47 and - Character'Pos (C) < 58); + pragma Loop_Invariant (for all C of Value => C in '0' .. '9'); Value (I) := Character'Val ((Token mod 10) + 48); Token := Token / 10; end loop; diff --git a/src/otp.ads b/src/otp.ads index 061afc6..4de590d 100644 --- a/src/otp.ads +++ b/src/otp.ads @@ -9,8 +9,7 @@ is subtype OTP_Value is String with Dynamic_Predicate => - (for all C of OTP_Value => - Character'Pos (C) > 47 and Character'Pos (C) < 58); + (for all C of OTP_Value => C in '0' .. '9'); -- 31 bit OTP token subtype OTP_Token is Integer range 0 .. 2 ** 31 - 1; diff --git a/tests/totp_test.adb b/tests/otp-t-test.adb similarity index 82% rename from tests/totp_test.adb rename to tests/otp-t-test.adb index 75d9457..1f1bfc0 100644 --- a/tests/totp_test.adb +++ b/tests/otp-t-test.adb @@ -3,7 +3,7 @@ with OTP.T; with LSC.Types; with LSC.Byte_Arrays; -package body TOTP_Test +package body OTP.T.Test with SPARK_Mode is @@ -20,12 +20,11 @@ is 16#37#, 16#38#, 16#39#, 16#30#); Time : constant LSC.Types.Word64 := 59; Totp_Value : constant OTP.OTP_Value := "94287082"; - package TOTP is new OTP.T; begin - if OTP.Image (TOTP.TOTP (Key, Time), 8) /= Totp_Value then + if OTP.Image (OTP.T.TOTP (Key, Time), 8) /= Totp_Value then return "Calculating TOTP value failed"; end if; return "PASSED"; end Run; -end TOTP_Test; +end OTP.T.Test; diff --git a/tests/totp_test.ads b/tests/otp-t-test.ads similarity index 80% rename from tests/totp_test.ads rename to tests/otp-t-test.ads index 3ff6738..24a04b9 100644 --- a/tests/totp_test.ads +++ b/tests/otp-t-test.ads @@ -1,4 +1,4 @@ -package TOTP_Test +package OTP.T.Test with SPARK_Mode is @@ -8,4 +8,4 @@ is with Post => Run'Result'Length <= 128; -end TOTP_Test; +end OTP.T.Test; diff --git a/tests/test.adb b/tests/test.adb index 8516d82..4ddd05b 100644 --- a/tests/test.adb +++ b/tests/test.adb @@ -5,7 +5,7 @@ with Base32.Test; with HMAC.Test; with OTP.Test; with OTP.H.Test; -with TOTP_Test; +with OTP.T.Test; procedure Test with SPARK_Mode @@ -39,7 +39,7 @@ begin Eval (HMAC.Test.Name, HMAC.Test.Run, Passed); Eval (OTP.Test.Name, OTP.Test.Run, Passed); Eval (OTP.H.Test.Name, OTP.H.Test.Run, Passed); - Eval (TOTP_Test.Name, TOTP_Test.Run, Passed); + Eval (OTP.T.Test.Name, OTP.T.Test.Run, Passed); if not Passed then Ada.Command_Line.Set_Exit_Status (1); end if;