Symbolic protocol analysis in the union of disjoint intruder theories: Combining decision procedures
Identifieur interne :
000791 ( PascalFrancis/Curation );
précédent :
000790;
suivant :
000792
Symbolic protocol analysis in the union of disjoint intruder theories: Combining decision procedures
Auteurs : Yannick Chevalier [
France] ;
Michael Rusinowitch [
France]
Source :
-
Theoretical computer science [ 0304-3975 ] ; 2010.
RBID : Pascal:10-0147183
Descripteurs français
- Pascal (Inist)
- Théorie décision,
Analyse décision,
Analyse limite,
Multiplication,
Décryptage,
Algorithme,
Théorie ensemble,
Résolubilité,
Contrainte,
Trace,
Opérateur borné,
Informatique théorique,
Union disjointe,
Procédure décision,
68P25,
68Wxx,
03Exx,
Protocole sécurité,
Chiffrement,
Protocole cryptographique.
English descriptors
- KwdEn :
- Algorithm,
Bounded operator,
Computer theory,
Constraint,
Cryptographic protocol,
Decision analysis,
Decision theory,
Decryption,
Encryption,
Limit analysis,
Multiplication,
Security protocol,
Set theory,
Solvability,
Trace.
Abstract
Most of the decision procedures for symbolic analysis of protocols are limited to a fixed set of algebraic operators associated with a fixed intruder theory. Examples of such sets of operators comprise XOR, multiplication, abstract encryption/decryption. In this report we give an algorithm for combining decision procedures for arbitrary intruder theories with disjoint sets of operators, provided that solvability of ordered intruder constraints, a slight generalization of intruder constraints, can be decided in each theory. This is the case for most of the intruder theories for which a decision procedure has been given. In particular our result allows us to decide trace-based security properties of protocols that employ any combination of the above mentioned operators with a bounded number of sessions.
| pA |
| A01 | 01 | 1 | | @0 0304-3975 |
|---|
| A02 | 01 | | | @0 TCSCDI |
|---|
| A03 | | 1 | | @0 Theor. comput. sci. |
|---|
| A05 | | | | @2 411 |
|---|
| A06 | | | | @2 10 |
|---|
| A08 | 01 | 1 | ENG | @1 Symbolic protocol analysis in the union of disjoint intruder theories: Combining decision procedures |
|---|
| A09 | 01 | 1 | ENG | @1 Security and Cryptography Foundations |
|---|
| A11 | 01 | 1 | | @1 CHEVALIER (Yannick) |
|---|
| A11 | 02 | 1 | | @1 RUSINOWITCH (Michael) |
|---|
| A12 | 01 | 1 | | @1 YUNG (Moti) @9 ed. |
|---|
| A14 | 01 | | | @1 IRIT, Team LiLac, Université Paul Sabatier @2 Toulouse @3 FRA @Z 1 aut. |
|---|
| A14 | 02 | | | @1 Loria-INRIA Lorraine, Cassis Project @2 Nancy @3 FRA @Z 2 aut. |
|---|
| A15 | 01 | | | @1 Google Research and Computer Science, Columbia University @2 10027 New York, NY @3 USA @Z 1 aut. |
|---|
| A20 | | | | @1 1261-1282 |
|---|
| A21 | | | | @1 2010 |
|---|
| A23 | 01 | | | @0 ENG |
|---|
| A43 | 01 | | | @1 INIST @2 17243 @5 354000190124430030 |
|---|
| A44 | | | | @0 0000 @1 © 2010 INIST-CNRS. All rights reserved. |
|---|
| A45 | | | | @0 31 ref. |
|---|
| A47 | 01 | 1 | | @0 10-0147183 |
|---|
| A60 | | | | @1 P @2 C |
|---|
| A61 | | | | @0 A |
|---|
| A64 | 01 | 1 | | @0 Theoretical computer science |
|---|
| A66 | 01 | | | @0 GBR |
|---|
| C01 | 01 | | ENG | @0 Most of the decision procedures for symbolic analysis of protocols are limited to a fixed set of algebraic operators associated with a fixed intruder theory. Examples of such sets of operators comprise XOR, multiplication, abstract encryption/decryption. In this report we give an algorithm for combining decision procedures for arbitrary intruder theories with disjoint sets of operators, provided that solvability of ordered intruder constraints, a slight generalization of intruder constraints, can be decided in each theory. This is the case for most of the intruder theories for which a decision procedure has been given. In particular our result allows us to decide trace-based security properties of protocols that employ any combination of the above mentioned operators with a bounded number of sessions. |
|---|
| C02 | 01 | X | | @0 001D02A08 |
|---|
| C02 | 02 | X | | @0 001D02B07B |
|---|
| C02 | 03 | X | | @0 001D02A05 |
|---|
| C02 | 04 | X | | @0 001A02A01E |
|---|
| C03 | 01 | X | FRE | @0 Théorie décision @5 17 |
|---|
| C03 | 01 | X | ENG | @0 Decision theory @5 17 |
|---|
| C03 | 01 | X | SPA | @0 Teoría decisión @5 17 |
|---|
| C03 | 02 | X | FRE | @0 Analyse décision @5 18 |
|---|
| C03 | 02 | X | ENG | @0 Decision analysis @5 18 |
|---|
| C03 | 02 | X | SPA | @0 Análisis decisión @5 18 |
|---|
| C03 | 03 | X | FRE | @0 Analyse limite @5 19 |
|---|
| C03 | 03 | X | ENG | @0 Limit analysis @5 19 |
|---|
| C03 | 03 | X | SPA | @0 Análisis límite @5 19 |
|---|
| C03 | 04 | X | FRE | @0 Multiplication @5 20 |
|---|
| C03 | 04 | X | ENG | @0 Multiplication @5 20 |
|---|
| C03 | 04 | X | SPA | @0 Multiplicación @5 20 |
|---|
| C03 | 05 | X | FRE | @0 Décryptage @5 21 |
|---|
| C03 | 05 | X | ENG | @0 Decryption @5 21 |
|---|
| C03 | 05 | X | SPA | @0 Desciframiento @5 21 |
|---|
| C03 | 06 | X | FRE | @0 Algorithme @5 22 |
|---|
| C03 | 06 | X | ENG | @0 Algorithm @5 22 |
|---|
| C03 | 06 | X | SPA | @0 Algoritmo @5 22 |
|---|
| C03 | 07 | X | FRE | @0 Théorie ensemble @5 23 |
|---|
| C03 | 07 | X | ENG | @0 Set theory @5 23 |
|---|
| C03 | 07 | X | SPA | @0 Teoría conjunto @5 23 |
|---|
| C03 | 08 | X | FRE | @0 Résolubilité @5 24 |
|---|
| C03 | 08 | X | ENG | @0 Solvability @5 24 |
|---|
| C03 | 08 | X | SPA | @0 Resolubilidad @5 24 |
|---|
| C03 | 09 | X | FRE | @0 Contrainte @5 25 |
|---|
| C03 | 09 | X | ENG | @0 Constraint @5 25 |
|---|
| C03 | 09 | X | SPA | @0 Coacción @5 25 |
|---|
| C03 | 10 | X | FRE | @0 Trace @5 26 |
|---|
| C03 | 10 | X | ENG | @0 Trace @5 26 |
|---|
| C03 | 10 | X | SPA | @0 Traza @5 26 |
|---|
| C03 | 11 | X | FRE | @0 Opérateur borné @5 27 |
|---|
| C03 | 11 | X | ENG | @0 Bounded operator @5 27 |
|---|
| C03 | 11 | X | SPA | @0 Operador acotado @5 27 |
|---|
| C03 | 12 | X | FRE | @0 Informatique théorique @5 28 |
|---|
| C03 | 12 | X | ENG | @0 Computer theory @5 28 |
|---|
| C03 | 12 | X | SPA | @0 Informática teórica @5 28 |
|---|
| C03 | 13 | X | FRE | @0 Union disjointe @4 INC @5 70 |
|---|
| C03 | 14 | X | FRE | @0 Procédure décision @4 INC @5 71 |
|---|
| C03 | 15 | X | FRE | @0 68P25 @4 INC @5 72 |
|---|
| C03 | 16 | X | FRE | @0 68Wxx @4 INC @5 73 |
|---|
| C03 | 17 | X | FRE | @0 03Exx @4 INC @5 74 |
|---|
| C03 | 18 | X | FRE | @0 Protocole sécurité @4 CD @5 96 |
|---|
| C03 | 18 | X | ENG | @0 Security protocol @4 CD @5 96 |
|---|
| C03 | 19 | X | FRE | @0 Chiffrement @4 CD @5 97 |
|---|
| C03 | 19 | X | ENG | @0 Encryption @4 CD @5 97 |
|---|
| C03 | 20 | X | FRE | @0 Protocole cryptographique @4 CD @5 98 |
|---|
| C03 | 20 | X | ENG | @0 Cryptographic protocol @4 CD @5 98 |
|---|
| N21 | | | | @1 095 |
|---|
| N44 | 01 | | | @1 OTO |
|---|
| N82 | | | | @1 OTO |
|---|
|
|---|
| pR |
| A30 | 01 | 1 | ENG | @1 International Colloquium on Automata, Languages and Programming (ICALP 2005) @2 32 @3 Lisboa PRT @4 2005-07-11 |
|---|
|
|---|
Links toward previous steps (curation, corpus...)
- to stream PascalFrancis, to step Corpus: Pour aller vers cette notice dans l'étape Curation :000227
Links to Exploration step
Pascal:10-0147183
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">Symbolic protocol analysis in the union of disjoint intruder theories: Combining decision procedures</title>
<author><name sortKey="Chevalier, Yannick" sort="Chevalier, Yannick" uniqKey="Chevalier Y" first="Yannick" last="Chevalier">Yannick Chevalier</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>IRIT, Team LiLac, Université Paul Sabatier</s1>
<s2>Toulouse</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
</inist:fA14><country>France</country>
</affiliation><author><name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michael" last="Rusinowitch">Michael Rusinowitch</name>
<affiliation wicri:level="1"><inist:fA14 i1="02"><s1>Loria-INRIA Lorraine, Cassis Project</s1>
<s2>Nancy</s2>
<s3>FRA</s3>
<sZ>2 aut.</sZ>
</inist:fA14><country>France</country>
</affiliation><publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">10-0147183</idno>
<date when="2010">2010</date>
<idno type="stanalyst">PASCAL 10-0147183 INIST</idno>
<idno type="RBID">Pascal:10-0147183</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000227</idno>
<idno type="wicri:Area/PascalFrancis/Curation">000791</idno>
</publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">Symbolic protocol analysis in the union of disjoint intruder theories: Combining decision procedures</title>
<author><name sortKey="Chevalier, Yannick" sort="Chevalier, Yannick" uniqKey="Chevalier Y" first="Yannick" last="Chevalier">Yannick Chevalier</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>IRIT, Team LiLac, Université Paul Sabatier</s1>
<s2>Toulouse</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
</inist:fA14><country>France</country>
</affiliation><author><name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michael" last="Rusinowitch">Michael Rusinowitch</name>
<affiliation wicri:level="1"><inist:fA14 i1="02"><s1>Loria-INRIA Lorraine, Cassis Project</s1>
<s2>Nancy</s2>
<s3>FRA</s3>
<sZ>2 aut.</sZ>
</inist:fA14><country>France</country>
</affiliation><series><title level="j" type="main">Theoretical computer science</title>
<title level="j" type="abbreviated">Theor. comput. sci.</title>
<idno type="ISSN">0304-3975</idno>
<imprint><date when="2010">2010</date>
</imprint><seriesStmt><title level="j" type="main">Theoretical computer science</title>
<title level="j" type="abbreviated">Theor. comput. sci.</title>
<idno type="ISSN">0304-3975</idno>
</seriesStmt><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Algorithm</term>
<term>Bounded operator</term>
<term>Computer theory</term>
<term>Constraint</term>
<term>Cryptographic protocol</term>
<term>Decision analysis</term>
<term>Decision theory</term>
<term>Decryption</term>
<term>Encryption</term>
<term>Limit analysis</term>
<term>Multiplication</term>
<term>Security protocol</term>
<term>Set theory</term>
<term>Solvability</term>
<term>Trace</term>
</keywords><keywords scheme="Pascal" xml:lang="fr"><term>Théorie décision</term>
<term>Analyse décision</term>
<term>Analyse limite</term>
<term>Multiplication</term>
<term>Décryptage</term>
<term>Algorithme</term>
<term>Théorie ensemble</term>
<term>Résolubilité</term>
<term>Contrainte</term>
<term>Trace</term>
<term>Opérateur borné</term>
<term>Informatique théorique</term>
<term>Union disjointe</term>
<term>Procédure décision</term>
<term>68P25</term>
<term>68Wxx</term>
<term>03Exx</term>
<term>Protocole sécurité</term>
<term>Chiffrement</term>
<term>Protocole cryptographique</term>
</keywords><front><div type="abstract" xml:lang="en">Most of the decision procedures for symbolic analysis of protocols are limited to a fixed set of algebraic operators associated with a fixed intruder theory. Examples of such sets of operators comprise XOR, multiplication, abstract encryption/decryption. In this report we give an algorithm for combining decision procedures for arbitrary intruder theories with disjoint sets of operators, provided that solvability of ordered intruder constraints, a slight generalization of intruder constraints, can be decided in each theory. This is the case for most of the intruder theories for which a decision procedure has been given. In particular our result allows us to decide trace-based security properties of protocols that employ any combination of the above mentioned operators with a bounded number of sessions.</div>
</front><inist><standard h6="B"><pA><fA01 i1="01" i2="1"><s0>0304-3975</s0>
</fA01><fA02 i1="01"><s0>TCSCDI</s0>
</fA02><fA03 i2="1"><s0>Theor. comput. sci.</s0>
</fA03><fA05><s2>411</s2>
</fA05><fA08 i1="01" i2="1" l="ENG"><s1>Symbolic protocol analysis in the union of disjoint intruder theories: Combining decision procedures</s1>
</fA08><fA09 i1="01" i2="1" l="ENG"><s1>Security and Cryptography Foundations</s1>
</fA09><fA11 i1="01" i2="1"><s1>CHEVALIER (Yannick)</s1>
</fA11><fA11 i1="02" i2="1"><s1>RUSINOWITCH (Michael)</s1>
</fA11><fA12 i1="01" i2="1"><s1>YUNG (Moti)</s1>
<s9>ed.</s9>
</fA12><fA14 i1="01"><s1>IRIT, Team LiLac, Université Paul Sabatier</s1>
<s2>Toulouse</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
</fA14><fA14 i1="02"><s1>Loria-INRIA Lorraine, Cassis Project</s1>
<s2>Nancy</s2>
<s3>FRA</s3>
<sZ>2 aut.</sZ>
</fA14><fA15 i1="01"><s1>Google Research and Computer Science, Columbia University</s1>
<s2>10027 New York, NY</s2>
<s3>USA</s3>
<sZ>1 aut.</sZ>
</fA15><fA20><s1>1261-1282</s1>
</fA20><fA21><s1>2010</s1>
</fA21><fA23 i1="01"><s0>ENG</s0>
</fA23><fA43 i1="01"><s1>INIST</s1>
<s2>17243</s2>
<s5>354000190124430030</s5>
</fA43><fA44><s0>0000</s0>
<s1>© 2010 INIST-CNRS. All rights reserved.</s1>
</fA44><fA45><s0>31 ref.</s0>
</fA45><fA47 i1="01" i2="1"><s0>10-0147183</s0>
</fA47><fA60><s1>P</s1>
<s2>C</s2>
</fA60><fA64 i1="01" i2="1"><s0>Theoretical computer science</s0>
</fA64><fA66 i1="01"><s0>GBR</s0>
</fA66><fC01 i1="01" l="ENG"><s0>Most of the decision procedures for symbolic analysis of protocols are limited to a fixed set of algebraic operators associated with a fixed intruder theory. Examples of such sets of operators comprise XOR, multiplication, abstract encryption/decryption. In this report we give an algorithm for combining decision procedures for arbitrary intruder theories with disjoint sets of operators, provided that solvability of ordered intruder constraints, a slight generalization of intruder constraints, can be decided in each theory. This is the case for most of the intruder theories for which a decision procedure has been given. In particular our result allows us to decide trace-based security properties of protocols that employ any combination of the above mentioned operators with a bounded number of sessions.</s0>
</fC01><fC02 i1="01" i2="X"><s0>001D02A08</s0>
</fC02><fC02 i1="02" i2="X"><s0>001D02B07B</s0>
</fC02><fC02 i1="03" i2="X"><s0>001D02A05</s0>
</fC02><fC02 i1="04" i2="X"><s0>001A02A01E</s0>
</fC02><fC03 i1="01" i2="X" l="FRE"><s0>Théorie décision</s0>
<s5>17</s5>
</fC03><fC03 i1="01" i2="X" l="ENG"><s0>Decision theory</s0>
<s5>17</s5>
</fC03><fC03 i1="01" i2="X" l="SPA"><s0>Teoría decisión</s0>
<s5>17</s5>
</fC03><fC03 i1="02" i2="X" l="FRE"><s0>Analyse décision</s0>
<s5>18</s5>
</fC03><fC03 i1="02" i2="X" l="ENG"><s0>Decision analysis</s0>
<s5>18</s5>
</fC03><fC03 i1="02" i2="X" l="SPA"><s0>Análisis decisión</s0>
<s5>18</s5>
</fC03><fC03 i1="03" i2="X" l="FRE"><s0>Analyse limite</s0>
<s5>19</s5>
</fC03><fC03 i1="03" i2="X" l="ENG"><s0>Limit analysis</s0>
<s5>19</s5>
</fC03><fC03 i1="03" i2="X" l="SPA"><s0>Análisis límite</s0>
<s5>19</s5>
</fC03><fC03 i1="04" i2="X" l="FRE"><s0>Multiplication</s0>
<s5>20</s5>
</fC03><fC03 i1="04" i2="X" l="ENG"><s0>Multiplication</s0>
<s5>20</s5>
</fC03><fC03 i1="04" i2="X" l="SPA"><s0>Multiplicación</s0>
<s5>20</s5>
</fC03><fC03 i1="05" i2="X" l="FRE"><s0>Décryptage</s0>
<s5>21</s5>
</fC03><fC03 i1="05" i2="X" l="ENG"><s0>Decryption</s0>
<s5>21</s5>
</fC03><fC03 i1="05" i2="X" l="SPA"><s0>Desciframiento</s0>
<s5>21</s5>
</fC03><fC03 i1="06" i2="X" l="FRE"><s0>Algorithme</s0>
<s5>22</s5>
</fC03><fC03 i1="06" i2="X" l="ENG"><s0>Algorithm</s0>
<s5>22</s5>
</fC03><fC03 i1="06" i2="X" l="SPA"><s0>Algoritmo</s0>
<s5>22</s5>
</fC03><fC03 i1="07" i2="X" l="FRE"><s0>Théorie ensemble</s0>
<s5>23</s5>
</fC03><fC03 i1="07" i2="X" l="ENG"><s0>Set theory</s0>
<s5>23</s5>
</fC03><fC03 i1="07" i2="X" l="SPA"><s0>Teoría conjunto</s0>
<s5>23</s5>
</fC03><fC03 i1="08" i2="X" l="FRE"><s0>Résolubilité</s0>
<s5>24</s5>
</fC03><fC03 i1="08" i2="X" l="ENG"><s0>Solvability</s0>
<s5>24</s5>
</fC03><fC03 i1="08" i2="X" l="SPA"><s0>Resolubilidad</s0>
<s5>24</s5>
</fC03><fC03 i1="09" i2="X" l="FRE"><s0>Contrainte</s0>
<s5>25</s5>
</fC03><fC03 i1="09" i2="X" l="ENG"><s0>Constraint</s0>
<s5>25</s5>
</fC03><fC03 i1="09" i2="X" l="SPA"><s0>Coacción</s0>
<s5>25</s5>
</fC03><fC03 i1="10" i2="X" l="FRE"><s0>Trace</s0>
<s5>26</s5>
</fC03><fC03 i1="10" i2="X" l="ENG"><s0>Trace</s0>
<s5>26</s5>
</fC03><fC03 i1="10" i2="X" l="SPA"><s0>Traza</s0>
<s5>26</s5>
</fC03><fC03 i1="11" i2="X" l="FRE"><s0>Opérateur borné</s0>
<s5>27</s5>
</fC03><fC03 i1="11" i2="X" l="ENG"><s0>Bounded operator</s0>
<s5>27</s5>
</fC03><fC03 i1="11" i2="X" l="SPA"><s0>Operador acotado</s0>
<s5>27</s5>
</fC03><fC03 i1="12" i2="X" l="FRE"><s0>Informatique théorique</s0>
<s5>28</s5>
</fC03><fC03 i1="12" i2="X" l="ENG"><s0>Computer theory</s0>
<s5>28</s5>
</fC03><fC03 i1="12" i2="X" l="SPA"><s0>Informática teórica</s0>
<s5>28</s5>
</fC03><fC03 i1="13" i2="X" l="FRE"><s0>Union disjointe</s0>
<s4>INC</s4>
<s5>70</s5>
</fC03><fC03 i1="14" i2="X" l="FRE"><s0>Procédure décision</s0>
<s4>INC</s4>
<s5>71</s5>
</fC03><fC03 i1="15" i2="X" l="FRE"><s0>68P25</s0>
<s4>INC</s4>
<s5>72</s5>
</fC03><fC03 i1="16" i2="X" l="FRE"><s0>68Wxx</s0>
<s4>INC</s4>
<s5>73</s5>
</fC03><fC03 i1="17" i2="X" l="FRE"><s0>03Exx</s0>
<s4>INC</s4>
<s5>74</s5>
</fC03><fC03 i1="18" i2="X" l="FRE"><s0>Protocole sécurité</s0>
<s4>CD</s4>
<s5>96</s5>
</fC03><fC03 i1="18" i2="X" l="ENG"><s0>Security protocol</s0>
<s4>CD</s4>
<s5>96</s5>
</fC03><fC03 i1="19" i2="X" l="FRE"><s0>Chiffrement</s0>
<s4>CD</s4>
<s5>97</s5>
</fC03><fC03 i1="19" i2="X" l="ENG"><s0>Encryption</s0>
<s4>CD</s4>
<s5>97</s5>
</fC03><fC03 i1="20" i2="X" l="FRE"><s0>Protocole cryptographique</s0>
<s4>CD</s4>
<s5>98</s5>
</fC03><fC03 i1="20" i2="X" l="ENG"><s0>Cryptographic protocol</s0>
<s4>CD</s4>
<s5>98</s5>
</fC03><fN21><s1>095</s1>
</fN21><fN44 i1="01"><s1>OTO</s1>
</fN44><fN82><s1>OTO</s1>
</fN82><pR><fA30 i1="01" i2="1" l="ENG"><s1>International Colloquium on Automata, Languages and Programming (ICALP 2005)</s1>
<s2>32</s2>
<s3>Lisboa PRT</s3>
<s4>2005-07-11</s4>
</fA30>
Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/PascalFrancis/Curation
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000791 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Curation/biblio.hfd -nk 000791 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= PascalFrancis
|étape= Curation
|type= RBID
|clé= Pascal:10-0147183
|texte= Symbolic protocol analysis in the union of disjoint intruder theories: Combining decision procedures
}}
| This area was generated with Dilib version V0.6.33.
Data generation: Mon Jun 10 21:56:28 2019. Site generation: Fri Feb 25 15:29:27 2022 |  |
